The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

Brigitte's and my ICFP 2013 paper includes both an intuitive account and 
a formal termination proof for sized types in the "inflationary style".  See

  http://www2.tcs.ifi.lmu.de/~abel/publications.html#icfp13

for conference and long version (with complete proof).

Also, there are papers of Jorge Sacchini on integrating sized types into 
the CIC.

Cheers,
Andreas

On 09.01.2014 19:10, Cody Roux wrote:
> On 01/09/2014 12:49 PM, Nikhil Swamy wrote:
> > This is a very interesting discussion ... thanks! Although it's a bit hard to 
> > keep up with it all! : )
> >
> > I wonder if someone here would be able to provide a suitable reading list on 
> > sized types. I have read Andreas Abel's MiniAgda paper, which provides nice 
> > examples and good intuition, but not much on the metatheory side. Is there 
> > something more comprehensive that you would recommend to study? Abel's LMCS 
> > 2008 paper? Something even more recent (or older)?
>      In addition to Andreas' excellent paper, you might want to look at
> his PhD dissertation, which is a nice read with a wealth of very nice
> examples and counter-examples. You might want to look at the MiniAgda
> paper as well. The other paper I enjoyed the most was Barthe /et. al./
>
> Typed based termination of recursive definitions
> http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.12.4933
>
> That explains the situation for simple types, which I think is a good start.
>
> Hope this helps!
>
> Best,
> Cody
>
>
> > Thanks!
> > -Nik
> >
> > > -----Original Message-----
> > > From:coq-club-request AT inria.fr
> > >   
> > > [mailto:coq-club-request AT inria.fr]
> > >  On
> > > Behalf Of Bruno Barras
> > > Sent: Thursday, January 9, 2014 3:45 AM
> > > To: Altenkirch Thorsten; Cody Roux; Jean Goubault-Larrecq; coq-
> > > club AT inria.fr
> > > Subject: Re: [Coq-Club] [Agda] Re: [HoTT] newbie questions about
> > > homotopy theory & advantage of UF/Coq
> > >
> > > On 09/01/2014 11:42, Altenkirch Thorsten wrote:
> > > > > About K: Coq has managed to describe a pattern-match whI wonder if someone 
> > > > > here would be able to provide a suitable reading list on sized types. I have 
> > > > > read Andreas Abel's MiniAgda paper, which provides nice examples and good 
> > > > > intuition, but not much on the metatheory side. Is there something more 
> > > > > comprehensive that you would recommend to study? Abel's LMCS 2008 paper? 
> > > > > Something even more recent (or older)?
> > > > >
> > > > > Thanks!
> > > > > -Nik
> > > > > ich does not
> > > > > allow it (by making less unification information available in the
> > > > > branches), and I don't think it's that relevant to the problem at
> > > > > hand, which is mostly concerned about when a term is a subterm of
> > > another.
> > > > I don't agree!
> > > >
> > > > If the only proof of equality is refl then it is clear that subst
> > > > should preserve the structural ordering.
> > > It's not clear to me. Proof-irrelevance does not mean that any equality
> > > admits refl as a proof!
> > > If you apply subst with a proof of 0=1 (or, less controversially
> > > (False->True) = True), I see a priori no reason why it should preserve the
> > > structural ordering. This ordering should remain well-founded even in
> > > inconsistent contexts.
> > >
> > > This reasoning is sound only when you do that for proofs of x=x, and then
> > > yes this is obviously related to K.
> > >
> > > Bruno.


--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/