T. Altenkirch, C. McBride & W. Swierstra (2007):
Observational Equality, Now!.
In: A. Stump & H. Xi: PLPV '07: Proceedings of the 2007 Workshop on Programming Languages meets Program Verification,
pp. 57–68.
B. Barras & B. Bernardo (2008):
The Implicit Calculus of Constructions as a Programming Language with Dependent Types.
In: Roberto M. Amadio: Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008,
Lecture Notes in Computer Science 4962.
Springer,
pp. 365–379.
R. Constable & the PRL group (1986):
Implementing Mathematics with the Nuprl Proof Development System.
Prentice-Hall.
M. Coppo1 & M. Dezani-Ciancaglini (1978):
A New Type Assignment for λ-terms.
Archiv. Math. Logik 19(1),
pp. 139–156.
R. Harper, F. Honsell & G. Plotkin (1993):
A Framework for Defining Logics.
Journal of the Association for Computing Machinery 40(1),
pp. 143–184.
P. Martin-Löf (1984):
Intuitionistic Type Theory.
Bibliopolis.
C. McBride (1999):
Dependently Typed Functional Programs and Their Proofs.
Ph.D. thesis.
University of Edinburgh.
A. Miquel (2001):
The Implicit Calculus of Constructions.
In: Typed Lambda Calculi and Applications,
Lecture Notes in Computer Science 2044.
Springer,
pp. 344–359.
N. Mishra-Linger & T. Sheard (2008):
Erasure and Polymorphism in Pure Type Systems.
In: Roberto M. Amadio: Foundations of Software Science and Computational Structures, 11th International Conference (FOSSACS),
Lecture Notes in Computer Science 4962.
Springer,
pp. 350–364.
A. Stump, M. Deters, A. Petcher, T. Schiller & T. Simpson (2009):
Verified Programming in Guru.
In: T. Altenkirch & T. Millstein: Programming Languges meets Program Verification (PLPV),
pp. 49–58.