Abhishek Anand and Vincent Rahli. CFGV Online Reference. url: http://nuprl.org/html/CFGVLFMTP2014/.
The Agda Wiki. http://wiki.portal.chalmers.se/agda/pmwiki.php.
T. Altenkirch. "A formalization of the strong normalization proof for System F in LEGO". In: TLCA. Springer, 1993, pp. 13-28.
A. Anand and V. Rahli. "Towards a Formally Verified Proof Assistant". Accepted to ITP 2014. 2014.
A. Anand and V. Rahli. Towards a Formally Verified Proof Assistant. Tech. rep. http://www.nuprl.org/html/Nuprl2Coq/. Cornell University, 2014.
B. Aydemir, A. Charguéraud, B. C. Pierce, R. Pollack, and S. Weirich. "Engineering Formal Metatheory". In: POPL. 2008, pp. 3-15.
B. Aydemir and S. Weirich. "LNgen: Tool support for locally nameless representations". 2010.
B. Barras. "Sets in Coq, Coq in Sets". In: Journal of Fromalized Reasoning 3.1 (2010), pp. 29-48.
A. Chlipala. "A certified type-preserving compiler from lambda calculus to assembly language". In: PLDI. 2007.
A. Chlipala. Certified programming with dependent types. MIT Press, 2011.
R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing mathematics with the Nuprl proof development system. Prentice-Hall, Inc., 1986.
François Pottier. dblib. Dec. 3, 2013. url: http://gallium.inria. fr/blog/announcing-dblib/.
J.-Y. Girard, P. Taylor, and Y. Lafont. Proofs and Types. Cambridge University Press, 1989.
D. J. Howe. "Equality in Lazy Computation Systems". In: LICS. 1989, pp. 198-203.
S. C. Kleene. "Disjunction and Existence Under Implication in Elementary Intuitionistic Formalisms". In: JSL 27.1 (Mar. 1, 1962), pp. 11-18.
A. Koprowski and H. Binsztok. "TRX: A formally verified parser interpreter". In: LMCS 7.2 (2011), pp. 345-365.
R. Kumar, M. O. Myreen, M. Norrish, and S. Owens. "CakeML: a verified implementation ofML". In: POPL. ACM Press, 2014, pp. 179-191.
F. Pfenning and C. Elliott. "Higher-Order Abstract Syntax". In: PLDI. 1988, pp. 199-208.
B. Pientka and J. Dunfield. "Beluga: A framework for programming and reasoning with deductive systems (system description)". In: Automated Reasoning. Springer, 2010, pp. 15-21.
A. M. Pitts. "Nominal logic: A first order theory of names and binding". In: TACS. Springer, 2001, pp. 219-242.
E. Polonowski. "Automatically generated infrastructure for De Bruijn syntaxes". In: ITP. Springer, 2013, pp. 402-417.
P. Sewell, F. Z. Nardelli, S. Owens, G. Peskine, T. Ridge, S. Sarkar, and R. StrnišA. "Ott: Effective tool support for the working semanticist". In: JFP 20.01 (2010), p. 71.
I. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. 2013.
C. Urban and C. Kaliszyk. "General Bindings and Alpha-Equivalence in Nominal Isabelle". In: LMCS 8.2 (2012).
S. Weirich, B. A. Yorgey, and T. Sheard. "Binders unbound". In: ICFP. 2011, pp. 333-345.
