[TYPES] Types theories with first-class definitional extensions

[Herman Geuvers]

We define and treat a system lambda-D in our book (Calculus of 
Constructions with definitions):

Rob Nederpelt and Herman Geuvers
Type Theory and Formal Proof, An Introduction, Cambridge University 
Press, December 2014.

See also
http://www.win.tue.nl/~wsinrpn/book_type_theory.htm


Another source is

Fairouz Kamareddine, Twan Laan and Rob Nederpelt: A Modern Perspective 
on Type Theory, From its Origins until Today, Kluwer Academic 
Publishers, Applied Logic Series, Vol. 29, 2004 – Chapter 10: Pure Type 
Systems with parameters and definitions.

Best

Herman Geuvers

On 11/03/2016 08:17 AM, Frédéric Blanqui wrote:
> [ 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
>>
>