Thorsten Altenkirch, Nils Anders Danielsson, Andres Löh & Nicholas Oury (2010):
ΠΣ:Dependent Types without the Sugar.
In: Functional and Logic Programming,
Lecture Notes in Computer Science 6009.
Springer,
pp. 40–55,
doi:10.1007/978-3-642-12251-4_5.
Thierry Coquand (1996):
An algorithm for type-checking dependent types.
Science of Computer Programming 26(1-3),
pp. 167–177,
doi:10.1016/0167-6423(95)00021-6.
Jean-Yves Girard (1972):
Interprétation fonctionelle et élimination des coupures dans l'arithmétique d'ordre supérieur.
Thèse de doctorat d'état.
Université Paris 7.
Andres Löh, Conor McBride & Wouter Swierstra (2010):
A tutorial implementation of a dependently typed lambda calculus.
Fundamenta Informaticae 102(2),
pp. 1001–1031,
doi:10.3233/FI-2010-304.
M.H. Sørensen & P. Urzyczyn (2006):
Lectures on the Curry-Howard Isomorphism.
Studies in Logic and the Foundations of Mathematics 149.
Elsevier,
doi:10.1016/S0049-237X(06)80003-0.