[ 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
