Re: [TYPES] Types theories with first-class definitional extensions

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hello.

For pure type systems with definitions, see the LFCS'94 paper of Poll & 
Severi: http://dx.doi.org/10.1007/3-540-58140-5_30.

For a module calculus for PTSs, see the TLCA'97 paper of Courant, 
http://dx.doi.org/10.1007/3-540-62688-3_32, and its journal version in 
JFP'07: http://dx.doi.org/10.1017/S0956796806005867.

Best regards,

Frédéric.


Le 02/11/2016 à 17:26, William J. Bowman a écrit :
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> On Tue, Nov 01, 2016 at 10:43:44PM -0400, Jacques Carette wrote:
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>>
>> I am looking for literature on (higher-order, potentially dependent) type
>> theories where a context (telescope) can contain not just declarations, but
>> also definitions.
> I may misunderstand your question, but doesn't CIC have this (and other languages with dependent let)?
>
> The typing rule for dependent let adds a definition to the context:
>
> Δ;Γ ⊢ e : t
> Δ;Γ,x = e :t ⊢ e' : t
> ----------------------
> Δ;Γ ⊢ let x = e in e' : t[e/x]
>
> https://coq.inria.fr/refman/Reference-Manual006.html
>
> This also reminds me of translucency.
> A translucent type add a definition to the type declaration:
>
> (x = e : t) -> t'
> ∃ (x = e : t). t
>
> The original work on translucent sums:
> https://www.cs.cmu.edu/~rwh/theses/lillibridge.pdf
>
> I've also seen translucent functions here, which has a good explanation of translucency and more
> citations to chase:
> http://dl.acm.org/citation.cfm?id=237791
>