The Agda Wiki. http://wiki.portal.chalmers.se/agda/pmwiki.php
Allen, S.F.: A non-type-theoretic semantics for type-theoretic language. Ph.D. thesis, Cornell University, (1987)
Allen, S.F., Bickford, M., Constable, R.L., Eaton, R., Kreitz, C., Lorigo, L., Moran, E.: Innovations in computational type theory using Nuprl. J. Appl. Logic 4(4), 428-469 (2006). http://www.nuprl.org/
Anand, A., Bickford, M., Constable, R.L., Rahli, V.: A type theory with partial equivalence relations as types. Presented at TYPES 2014 (2014)
Anand, A., Rahli, V.: Towards a formally verified proof assistant. Technical report, Cornell University (2014). http://www.nuprl.org/html/Nuprl2Coq/
Anand, A., Rahli, V.: Towards a formally verified proof assistant. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 27-44. Springer, Heidelberg (2014)
Berardi, S., Bezem, M., Coquand, T.: On the computational content of the axiom of choice. J. Symb. Log. 63(2), 600-622 (1998)
Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004). http://www.labri.fr/perso/casteran/CoqArt
Bickford, M., Constable, R.: Inductive construction in Nuprl type theory using bar induction. Presented at TYPES 2014 (2014). http://nuprl.org/KB/show.php? ID=723
Bove, A., Dybjer, P., Norell, U.: A brief overview of Agda - a functional language with dependent types. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 73-78. Springer, Heidelberg (2009)
Brady, E.: IDRIS: systems programming meets full dependent types. In: PLPV 2011, pp. 43-54. ACM (2011)
Bridges, D., Richman, F.: Varieties of Constructive Mathematics. London Mathematical Society Lecture Notes Series. Cambridge University Press, Cambridge (1987)
Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall Inc, Upper Saddle River (1986)
Constable, R.L.: Constructive mathematics as a programming logic I: some principles of theory. In: Karpinski, M. (ed.) Fundamentals of Computation Theory. LNCS, vol. 158, pp. 64-77. Springer, London (1983)
The Coq Proof Assistant. http://coq.inria.fr/
Crary, K.: Type-theoretic methodology for practical programming languages. Ph.D. thesis, Cornell University, Ithaca, NY, August 1998
Dummett, M.A.E.: Elements of Intuitionism, 2nd edn. Clarendon Press, Oxford (2000)
Escardó, M.H., Chuangjie, X.: The Inconsistency of a Brouwerian Continuity principle with the curry-howard interpretation. In: TLCA 2015, vol. 38, pp. 153-164. LIPIcs. Schloss Dagstuhl - Leibniz- Zentrum fuer Informatik (2015)
Allen, S.F., Constable, R.L., Howe, D.J.: Reflecting the open-ended computation system of constructive type theory. In: Bauer, F.L. (ed.) Logic, Algebra and Computation. NATO ASI Series, vol. 79, pp. 265-280. Springer, Heidelberg (1990)
Hofmann, M.: Extensional concepts in intensional type theory. Ph.D. thesis, University of Edinburgh (1995)
Howard, W.A., Kreisel, G.: Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis. J. Symb. Log. 31(3), 325-358 (1966)
Howe, D.J.: Equality in lazy computation systems. In: LICS 1989, pp. 198-203. IEEE Computer Society (1989)
Howe, D.J.: Importing mathematics from HOL into Nuprl. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 267-282. Springer, Heidelberg (1996)
Howe, D.J.: On computational open-endedness in Martin-Löf’s type theory. In: LICS 1991, pp. 162-172. IEEE Computer Society (1991)
Howe, D.J.: Semantic foundations for embedding HOL in Nuprl. In: Nivat, M., Wirsing, M. (eds.) AMAST 1996. LNCS, vol. 1101, pp. 85-101. Springer, Heidelberg (1996)
Idris. http://www.idris-lang.org/
Kleene, S.C., Vesley, R.E.: The Foundations of Intuitionistic Mathematics, Especially in Relation to Recursive Functions. North-Holland Publishing Company, Amsterdam (1965)
Kopylov, A.: Type theoretical foundations for data structures, classes, and objects. Ph.D. thesis, Cornell University, Ithaca, NY (2004)
Kreisel, G.: On weak completeness of intuitionistic predicate logic. J. Symb. Logic 27(2), 139-158 (1962)
Kumar, R., Arthan, R., Myreen, M.O., Owens, S.: Self-formalisation of higherorder logic - semantics, soundness, and a verified implementation. J. Autom. Reason. 56(3), 221-259 (2016)
Longley, J.: When is a functional program not a functional program? In: ICFP 1999, pp. 1-7. ACM (1999)
Nogin, A., Kopylov, A.: Formalizing type operations using the "Image" type constructor. Electr. Notes Theor. Comput. Sci. 165, 121-132 (2006)
Rahli, V., Bickford, M.: A nominal exploration of intuitionism. Extended version of our CPP. 2016 paper (2015). http://www.nuprl.org/html/Nuprl2Coq/ continuity-long.pdf
Rahli, V., Bickford, M.: A nominal exploration of intuitionism. In: CPP, pp. 130-141. ACM (2016)
Rahli, V., Bickford, M., Anand, A.: Formal program optimization in Nuprl using computational equivalence and partial types. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 261-278. Springer, Heidelberg (2013)
Rahli, V., Bickford, M., Constable, R.L.: A story of bar induction in Nuprl (2015). Extended version http://www.nuprl.org/html/Nuprl2Coq/bar-induction-long.pdf
Rathjen, M.: Constructive set theory and brouwerian principles. J. UCS 11(12), 2008-2033 (2005)
Smith, S.F.: Partial objects in type theory. Ph.D. thesis, Cornell University, Ithaca, NY (1989)
Troelstra, A.S.: A note on non-extensional operations in connection with continuity and recursiveness. Indagationes Mathematicae 39(5), 455-462 (1977)
Troelstra, A.S.: Aspects of constructive mathematics. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp. 973-1052. North-Holland Publishing Company, Amsterdam (1977)
Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics an Introduction. Studies in Logic and the Foundations of Mathematics, vol. 121. Elsevier, North Holland (1988)
The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study (2013). http:// homotopytypetheory.org/book
Veldman, W.: Brouwer’s real thesis on bars. Philosophia Scientiæ CS6, 21-42 (2006)
Veldman, W.: Understanding and using Brouwer’s Continuity principle. In: Schuster, P., Berger, U., Osswald, H. (eds.) Reuniting the Antipodes Constructive and Nonstandard Views of the Continuum. Synthese Library, vol. 306, pp. 285-302. Springer, Netherlands (2001)
