@misc(Agda,
 year         = {2016},
 title        = {The Agda wiki},
 url          = {http://wiki.portal.chalmers.se/agda/pmwiki.php},
)
@inproceedings(ADLO,
 author       = {Thorsten Altenkirch and Nils Anders Danielsson and Andres L{\"o}h and Nicholas Oury},
 year         = {2010},
 title        = {{$\Pi\Sigma $}:Dependent Types without the Sugar},
 booktitle    = {Functional and Logic Programming},
 series       = {Lecture Notes in Computer Science},
 volume       = {6009},
 publisher    = {Springer},
 pages        = {40--55},
 doi          = {10.1007/978-3-642-12251-4\_5},
)
@misc(August,
 author       = {Lennart Augustsson},
 year         = {2007},
 title        = {Simpler, Easier!},
 url          = {http://augustss.blogspot.ru/2007/10/simpler-easier-in-recent-paper-simply.html},
)
@misc(Bauer,
 author       = {Andrej Bauer},
 year         = {2012},
 title        = {How to Implement Dependent Type Theory},
 url          = {http://math.andrej.com/2012/11/08/how-to-implement-dependent-type-theory-i/},
)
@misc(Coq,
 year         = {2016},
 title        = {The Coq proof assistant},
 url          = {https://coq.inria.fr},
)
@article(TCoq,
 author       = {Thierry Coquand},
 year         = {1996},
 title        = {An algorithm for type-checking dependent types},
 journal      = {Science of Computer Programming},
 volume       = {26},
 number       = {1-3},
 pages        = {167--177},
 doi          = {10.1016/0167-6423(95)00021-6},
)
@phdthesis(Gir,
 author       = {Jean-Yves Girard},
 year         = {1972},
 title        = {Interpr{\'e}tation fonctionelle et {\'e}limination des coupures dans l'arithm{\'e}tique d'ordre sup{\'e}rieur},
 type         = {Th{\`e}se de doctorat d'{\'e}tat},
 school       = {Universit{\'e} Paris 7},
)
@article(LMS,
 author       = {Andres L{\"o}h and Conor McBride and Wouter Swierstra},
 year         = {2010},
 title        = {A tutorial implementation of a dependently typed lambda calculus},
 journal      = {Fundamenta Informaticae},
 volume       = {102},
 number       = {2},
 pages        = {1001--1031},
 doi          = {10.3233/FI-2010-304},
)
@misc(Racket,
 year         = {2012},
 title        = {Racket},
 url          = {http://www.racket-lang.org},
)
@book(SU,
 author       = {S{\o}rensen, M.H. and P. Urzyczyn},
 year         = {2006},
 title        = {Lectures on the Curry-Howard Isomorphism},
 series       = {Studies in Logic and the Foundations of Mathematics},
 volume       = {149},
 publisher    = {Elsevier},
 doi          = {10.1016/S0049-237X(06)80003-0},
)
@misc(Weir,
 author       = {Stephanie Weirich},
 year         = {2014},
 title        = {Lectures at the Oregon Programming Languages Summer School: Types, Logic, Semantics, and Verification},
 url          = {https://www.cs.uoregon.edu/research/summerschool/summer14/index.html},
)