coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Similarities between forall and fun

From: Dominic Mulligan <dominic.p.mulligan AT googlemail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Similarities between forall and fun
Date: Sun, 15 Nov 2015 15:53:06 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=dominic.p.mulligan AT googlemail.com; spf=Pass smtp.mailfrom=dominic.p.mulligan AT googlemail.com; spf=None smtp.helo=postmaster AT mail-ig0-f175.google.com
Ironport-phdr: 9a23:FE2XwBy2ucOXY4rXCy+O+j09IxM/srCxBDY+r6Qd0e8VIJqq85mqBkHD//Il1AaPBtWGra8ZwLqP+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStOU0pn8h7n60qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mosVHSODxe7kyZb1eFjUvdW4vt+PxshyWYQyK530dWS0zjx5MAgfM6lmuUpD0sy37vaxlniyHOcn3QrkycTul6KhvRRrhiSNBPDk8pjKEwvdshb5W9Ury7yd0xJTZNdmY

> Here is an example of such type system:
>
> Pure Subtype Systems, DeLesley S. Hutchins
> http://www.diku.dk/hjemmesider/ansatte/henglein/papers/hutchins2010.pdf

And here is another with a small bibliography pointing to similar work:

http://www.macs.hw.ac.uk/~fairouz/forest/papers/journals-publications/jfp05.pdf

Ironically, according to that paper Coquand first presented the Calculus of Constructions with a single, unified binder, following a convention established by De Bruijn in AutoMath.

Thanks,
Dominic

[Coq-Club] Similarities between forall and fun, Yasuaki Kudo, 11/15/2015
- <Possible follow-up(s)>
- Re: [Coq-Club] Similarities between forall and fun, Kyle Stemen, 11/15/2015
- Re: [Coq-Club] Similarities between forall and fun, Gabriel Scherer, 11/15/2015
  - Re: [Coq-Club] Similarities between forall and fun, effectfully, 11/15/2015
    - Re: [Coq-Club] Similarities between forall and fun, Dominic Mulligan, 11/15/2015
      - Re: [Coq-Club] Similarities between forall and fun, Andreas Abel, 11/19/2015
  - RE: [Coq-Club] Similarities between forall and fun, Yasuaki Kudo, 11/17/2015
- Re: [Coq-Club] Similarities between forall and fun, Yves Bertot, 11/16/2015
  - Re: [Coq-Club] Similarities between forall and fun, Freek Wiedijk, 11/16/2015
    - Re: [Coq-Club] Similarities between forall and fun, Thorsten Altenkirch, 11/16/2015
      - Re: [Coq-Club] Similarities between forall and fun, Freek Wiedijk, 11/16/2015
        
        Re: [Coq-Club] Similarities between forall and fun, Thorsten Altenkirch, 11/16/2015
        
        Re: [Coq-Club] Similarities between forall and fun, Randy Pollack, 11/16/2015
        
        Re: [Coq-Club] Similarities between forall and fun, Freek Wiedijk, 11/16/2015
- RE: [Coq-Club] Similarities between forall and fun, Soegtrop, Michael, 11/16/2015