Stuart F. Allen. “A Non-Type-Theoretic Definition of Martin-Löf’s Types”. In: LICS. IEEE Computer Society, 1987, pp. 215–221.
Stuart F. Allen. “A Non-Type-Theoretic Semantics for Type-Theoretic Language”. PhD thesis. Cornell University, 1987.
Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, and Lori Lorigo. FDL: A Prototype Formal Digital Library. Tech. rep. 2004-1941. Cornell University, 2002.
Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, and Evan Moran. “Innovations in computational type theory using Nuprl”. In: J. Applied Logic 4.4 (2006). http://www.nuprl.org/, pp. 428–469.
Abhishek Anand, Mark Bickford, Robert L. Constable, and Vincent Rahli. “A Type Theory with Partial Equivalence Relations as Types”. Presented at TYPES 2014. 2014.
Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, and Nicolas Tabareau. “To-wards Certified Meta-Programming with Typed Template-Coq”. In: ITP 2018. Vol. 10895. LNCS. Springer, 2018, pp. 20–39.
Abhishek Anand and Vincent Rahli. Towards a Formal ly Verified Proof Assistant. Tech. rep. http://www.nuprl.org/html/Nuprl2Coq/. Cornell University, 2014.
Abhishek Anand and Vincent Rahli. “Towards a Formally Verified Proof Assistant”. In: ITP 2014. Vol. 8558. LNCS. Springer, 2014, pp. 27–44.
Bruno Barras. “Sets in Coq, Coq in Sets”. In: Journal of Formalized Reasoning 3.1 (2010), pp. 29–48.
Bruno Barras and Benjamin Werner. Coq in Coq. Tech. rep. INRIA Rocquencourt, 1997.
Yves Bertot and Pierre Casteran. Interactive Theorem Proving and Program Development. http://www.labri.fr/perso/casteran/CoqArt. SpringerVerlag, 2004.
Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, and André Platzer. “Formally verified differential dynamic logic”. In: CPP 2017. ACM, 2017, pp. 208–221.
Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen, and André Platzer. “VeriPhy: verified controller executables from verified cyber-physical system models”. In: PLDI 2018. ACM, 2018, pp. 617–630.
Ana Bove, Peter Dybjer, and Ulf Norell. “A Brief Overview of Agda-A Functional Language with Dependent Types”. In: TPHOLs 2009. Vol. 5674. LNCS. http://wiki. portal.chalmers.se/agda/pmwiki.php. Springer, 2009, pp. 73–78.
Edwin Brady. “IDRIS —: systems programming meets full dependent types”. In: PLPV 2011. ACM, 2011, pp. 43–54.
Alexandre Buisse and Peter Dybjer. “Towards Formalizing Categorical Models of Type Theory in Type Theory”. In: Electr. Notes Theor. Comput. Sci. 196 (2008), pp. 137–151.
Robert L. Constable. “Constructive Mathematics as a Programming Logic I: Some Principles of Theory”. In: Fundamentals of Computation Theory. Vol. 158. LNCS. Springer, 1983, pp. 64–77.
Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith. Implementing mathematics with the Nuprl proof development system. Upper Saddle River, NJ, USA: Prentice-Hall, Inc., 1986.
Robert L. Constable and Scott F. Smith. “Computational Foundations of Basic Recursive Function Theory”. In: Theoretical Computer Science 121.1&2 (1993), pp. 89–112.
William Cook and Jens Palsberg. “A Denotational Semantics of Inheritance and Its Correctness”. In: SIGPLAN Not. 24.10 (Sept. 1989), pp. 433–443.
The Coq Proof Assistant. http://coq.inria.fr/.
Karl Crary. “Type-Theoretic Methodology for Practical Programming Languages”. PhD thesis. Ithaca, NY: Cornell University, Aug. 1998.
Stuart F. Allen, Robert L. Constable, and Douglas J. Howe. “Reflecting the Open-Ended Computation System of Constructive Type Theory”. In: Logic, Algebra and Computation. Vol. F79. NATO ASI Series. Springer-Verlag, 1990, pp. 265–280.
Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, and André Platzer. “KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems”. In: CADE-25. Vol. 9195. LNCS. Springer, 2015, pp. 527–538.
Murdoch Gabbay and Andrew M. Pitts. “A New Approach to Abstract Syntax Involving Binders”. In: LICS 1999. IEEE Computer Society, 1999, pp. 214–224.
John Harrison. “Towards Self-verification of HOL Light”. In: IJCAR 2006. Vol. 4130. LNCS. Springer, 2006, pp. 177–191.
Martin Hofmann. “Extensional concepts in intensional type theory”. PhD thesis. University of Edinburgh, 1995.
Douglas J. Howe. “Equality in Lazy Computation Systems”. In: LICS 1989. IEEE Computer Society, 1989, pp. 198–203.
Douglas J. Howe. “On Computational Open-Endedness in Martin-Löf’s Type Theory”. In: LICS ’91. IEEE Computer Society, 1991, pp. 162–172.
Douglas J. Howe. “Semantic Foundations for Embedding HOL in Nuprl”. In: Algebraic Methodology and Software Technology. Vol. 1101. LNCS. Berlin: Springer-Verlag, 1996, pp. 85–101.
Idris. http://www.idris-lang.org/.
Alexei Kopylov. “Type Theoretical Foundations for Data Structures, Classes, and Objects”. PhD thesis. Ithaca, NY: Cornell University, 2004.
Saul A. Kripke. “Semantical Considerations on Modal Logic”. In: Acta Philosophica Fennica 16.1963 (1963), pp. 83–94.
Ramana Kumar, Rob Arthan, Magnus O. Myreen, and Scott Owens. “HOL with Definitions: Semantics, Soundness, and a Verified Implementation”. In: ITP 2014. Vol. 8558. LNCS. Springer, 2014, pp. 308–324.
Ramana Kumar, Rob Arthan, Magnus O. Myreen, and Scott Owens. “Self-Formalisation of Higher-Order Logic-Semantics, Soundness, and a Verified Implementation”. In: J. Autom. Reasoning 56.3 (2016), pp. 221–259.
Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. “CakeML: a verified implementation of ML”. In: POPL’14. ACM, 2014, pp. 179–192.
Ondrej Kuncar and Andrei Popescu. “A Consistent Foundation for Isabelle/HOL”. In: ITP 2015. Vol. 9236. LNCS. Springer, 2015, pp. 234–252.
Ondrej Kuncar and Andrei Popescu. “Comprehending Isabelle/HOL’s Consistency”. In: ESOP 2017. Vol. 10201. LNCS. Springer, 2017, pp. 724–749.
Ondrej Kuncar and Andrei Popescu. “Safety and conservativity of definitions in HOL and Isabelle/HOL”. In: vol. 2. POPL. 2018, 24:1–24:26.
Rustan Leino. “Dafny: An Automatic Program Verifier for Functional Correctness”. In: Logic for Programming, Artificial Intel ligence, and Reasoning. Springer Berlin Heidelberg, Apr. 2010, pp. 348–370.
Lori Lorigo. “Information Management in the Service of Knowledge and Discovery”. PhD thesis. Cornell University, 2006.
Martin-Löf. “Constructive Mathematics and Computer Programming”. In: 6th International Congress for Logic, Methodology and Philosophy of Science. Noth-Holland, Amsterdam, 1982, pp. 153–175.
Bertrand Meyer. “Applying "Design by Contract"”. In: IEEE Computer 25.10 (1992), pp. 40–51.
Bertrand Meyer. Eiffel: the language. Prentice-Hall, Inc., 1992.
Magnus O. Myreen and Jared Davis. “A Verified Runtime for a Verified Theorem Prover”. In: ITP 2011. Vol. 6898. LNCS. Springer, 2011, pp. 265–280.
Magnus O. Myreen and Jared Davis. “The Reflective Milawa Theorem Prover Is Sound-(Down to the Machine Code That Runs It)”. In: ITP 2014. Vol. 8558. LNCS. Springer, 2014, pp. 421–436.
Magnus O. Myreen, Scott Owens, and Ramana Kumar. “Steps towards Verified Implementations of HOL Light”. In: ITP’13. Vol. 7998. LNCS. Springer, 2013, pp. 490–495.
Aleksey Nogin and Alexei Kopylov. “Formalizing Type Operations Using the "Image" Type Constructor”. In: Electr. Notes Theor. Comput. Sci. 165 (2006), pp. 121–132.
Nuprl in Coq. https://github.com/vrahli/NuprlInCoq.
Andrew M Pitts. Nominal Sets: Names and Symmetry in Computer Science, volume 57 of Cambridge Tracts in Theoretical Computer Science. 2013.
Andrew M. Pitts. “Nominal Logic: A First Order Theory of Names and Binding”. In: TACS 2001. Vol. 2215. LNCS. Springer, 2001, pp. 219–242.
Vincent Rahli and Mark Bickford. “A nominal exploration of intuitionism”. In: CPP 2016. Extended version: http://www.nuprl.org/html/Nuprl2Coq/continuity-long.pdf. ACM, 2016, pp. 130–141.
Vincent Rahli and Mark Bickford. “Validating Brouwer’s continuity principle for numbers using named exceptions”. In: Mathematical Structures in Computer Science (2017), pp. 1– 49.
Vincent Rahli, Mark Bickford, and Abhishek Anand. “Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types”. In: ITP’13. Vol. 7998. LNCS. Springer, 2013, pp. 261–278.
John C. Reynolds. “Types, Abstraction and Parametric Polymorphism”. In: IFIP Congress. 1983, pp. 513–523.
Tom Ridge and James Margetson. “A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic”. In: TPHOLs 2005. Vol. 3603. LNCS. Springer, 2005, pp. 294– 309.
Scott F. Smith. “Partial Objects in Type Theory”. PhD thesis. Ithaca, NY: Cornell University, 1989.
The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study: http://homotopytypetheory.org/book, 2013.
Benjamin Werner. “Sets in Types, Types in Sets”. In: TACS. Vol. 1281. LNCS. Springer, 1997, pp. 530–546.
