[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
