H. Barendregt (1992):
Lambda calculi with types.
In: S. Abramsky, D.M. Gabbay & T.S.E. Maibaum: Handbook of Logic in Computer Science 2.
Oxford University Press,
pp. 117–309.
F. Blanqui (2001):
Definitions by Rewriting in the Calculus of Constructions.
In: Logic in Computer Science.
IEEE Computer Society,
pp. 9–18,
doi:10.1109/LICS.2001.932478.
C. Sacerdoti Coen (2004):
Mathematical Libraries as Proof Assistant Environments.
In: A. Asperti, G. Bancerek & A. Trybulec: Mathematical Knowledge Management,
Lecture Notes in Computer Science 3119.
Springer,
pp. 332–346,
doi:10.1007/978-3-540-27818-4_24.
T. Coquand & G. Huet (1988):
The Calculus of Constructions.
Information and Computation 76(2/3),
pp. 95–120,
doi:10.1016/0890-5401(88)90005-3.
D. Cousineau & G. Dowek (2007):
Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo.
In: S. Ronchi Della Rocca: Typed Lambda Calculi and Applications,
Lecture Notes in Computer Science 4583.
Springer,
pp. 102–117,
doi:10.1007/978-3-540-73228-0_9.
H. Geuvers, R. Krebbers, J. McKinna & F. Wiedijk (2010):
Pure Type Systems without Explicit Contexts.
In: K. Crary & M. Miculan: Logical Frameworks and Meta-languages: Theory and Practice,
Electronic Proceedings in Theoretical Computer Science 34.
Open Publishing Association,
pp. 53–67,
doi:10.4204/EPTCS.34.6.
H. Geuvers & M.-J. Nederhof (1991):
Modular proof of strong normalization for the calculus of constructions.
Journal of Functional Programming 1(2),
pp. 155–189,
doi:10.1017/S0956796800020037.
eptcs@eptcs.org