The Coq mailing list

[Jorge Luis Sacchini <sacchini AT qatar.cmu.edu>]

You may also want to look at the following papers:

  Gilles Barthe, Benjamin Grégoire, and Fernando Pastawski.
  Practical inference for type-based termination in a polymorphic
  setting.
  TLCA 2005.

  Gilles Barthe, Benjamin Grégoire, and Fernando Pastawski.
  CIC^ : Type-based termination of recursive definitions in the
  Calculus of Inductive Constructions.
  LPAR 2006.

They describe type systems with sized types for system F and CIC, 
including a size-inference algorithm. My work on sized types builds 
directly on top of these systems.

There is also this tutorial:

   Gilles Barthe, Benjamin Grégoire, and Colin Riba.
   A Tutorial on Type-Based Termination.
   LERNET 2008 summer school.

which may have more examples and metatheory (I don't remember the 
details very well).


-- Jorge



On 09/01/14 21:54, Andreas Abel wrote:
> 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.