coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: effectfully <effectfully AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Similarities between forall and fun
Date: Sun, 15 Nov 2015 18:37:41 +0300
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=effectfully AT gmail.com; spf=Pass smtp.mailfrom=effectfully AT gmail.com; spf=None smtp.helo=postmaster AT mail-yk0-f170.google.com
Ironport-phdr: 9a23:iO4Qih+etZtJ9v9uRHKM819IXTAuvvDOBiVQ1KB90OwcTK2v8tzYMVDF4r011RmSDdidtq8P1LqempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lR8iP0o/oh6ibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwu3cYh/V0/MlZFK7+Yq4QTLpCDT1gPXpmytfssEzOQwWC7WcST2ESg1IcDgbL4RrmUIr1tjrSue902S3cNsrzG+NnEQ++5rtmHUe7wBwMMCQ0pTna

Gabriel Scherer,
>I don't remember a precise reference

Here is an example of such type system:

Pure Subtype Systems, DeLesley S. Hutchins
http://www.diku.dk/hjemmesider/ansatte/henglein/papers/hutchins2010.pdf

[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