Harley D. Eades III & Aaron Stump (2010):
Hereditary Substitution for Stratified System F.
In: International Workshop on Proof-Search in Type Theories.
A FLoC workshop,
Edinburgh, Scotland.
Available at http://homepage.divms.uiowa.edu/~astump/papers/pstt-2010.pdf.
Gregory Malecha, Adam Chlipala & Thomas Braibant (2014):
Compositional Computational Reflection.
In: Gerwin Klein & Ruben Gamboa: ITP'14,
Lecture Notes in Computer Science 8558.
Springer,
pp. 374–389,
doi:10.1007/978-3-319-08970-6_24.
Conor McBride (2005):
Epigram: Practical Programming with Dependent Types.
Advanced Functional Programming,
pp. 130–170,
doi:10.1007/11546382_3.
Ulf Norell (2007):
Towards a practical programming language based on dependent type theory.
Department of Computer Science and Engineering, Chalmers University of Technology,
SE-412 96 Göteborg, Sweden.
Available at http://www.cs.chalmers.se/~ulfn/papers/thesis.html.
Matthieu Sozeau (2010):
Equations: A Dependent Pattern-Matching Compiler.
In: First International Conference on Interactive Theorem Proving.
Springer,
doi:10.1007/978-3-642-14052-5_29.