coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Andreas Abel <andreas.abel AT ifi.lmu.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Similarities between forall and fun
Date: Thu, 19 Nov 2015 15:06:23 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=andreas.abel AT ifi.lmu.de; spf=None smtp.mailfrom=andreas.abel AT ifi.lmu.de; spf=None smtp.helo=postmaster AT acheron.ifi.lmu.de
Ironport-phdr: 9a23:90dBhRYaipVrIaZ4JHB00ln/LSx+4OfEezUN459isYplN5qZpc+zbnLW6fgltlLVR4KTs6sC0LqL9f67EjFRqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh730pcaYPlQArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8/VPlTCCksG2Ez/szi8xfZHiWV4X5Je2MaiBdBGEDs5hz+FsP4tCfgu+NmniCQMMneTL41HzCn8uFnRUm72288Kzcl/TSP2YRLh6VBrUf5qg==

My student Matthias Benkard also worked on such a system, see "Type Checking without Types"

http://www.cse.chalmers.se/~abela/benkardThesis.pdf

On 15.11.2015 16:53, Dominic Mulligan wrote:

> 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

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

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

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

[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