References

1. (2016): The Agda wiki. Available at http://wiki.portal.chalmers.se/agda/pmwiki.php.
2. 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.
3. Lennart Augustsson (2007): Simpler, Easier!. Available at http://augustss.blogspot.ru/2007/10/simpler-easier-in-recent-paper-simply.html.
4. Andrej Bauer (2012): How to Implement Dependent Type Theory. Available at http://math.andrej.com/2012/11/08/how-to-implement-dependent-type-theory-i/.
5. (2016): The Coq proof assistant. Available at https://coq.inria.fr.
6. 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.
7. 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.
8. 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.
9. (2012): Racket. Available at http://www.racket-lang.org.
10. 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.
11. Stephanie Weirich (2014): Lectures at the Oregon Programming Languages Summer School: Types, Logic, Semantics, and Verification. Available at https://www.cs.uoregon.edu/research/summerschool/summer14/index.html.

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org