The Coq mailing list

[Cody Roux <cody.roux AT andrew.cmu.edu>]

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.