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, 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 and Vincent Rahli. "Towards a Formally Verified Proof Assistant". In: ITP 2014. Vol. 8558. LNCS. Springer, 2014, pp. 27-44.
Mark van Atten. On Brouwer. Wadsworth Philosophers. Cengage Learning, 2004.
Mark van Atten and Dirk van Dalen. "Arguments for the continuity principle". In: Bulletin of Symbolic Logic 8.3 (2002), pp. 329-347.
Stefano Berardi, Marc Bezem, and Thierry Coquand. "On the Computational Content of the Axiom of Choice". In: J. Symb. Log. 63.2 (1998), pp. 600-622.
Mark Bickford, Liron Cohen, Robert L. Constable, and Vincent Rahli. "Computability Beyond Church-Turing via Choice Sequences". Extended version avaible at https://vrahli.gith ub.io/articles/FCS-long.pdf. 2018.
Douglas Bridges and Fred Richman. Varieties of Constructive Mathematics. London Mathematical Society Lecture Notes Series. Cambridge University Press, 1987.
L. E. J Brouwer. "Begründung der mengenlehre unabhängig vom logischen satz vom ausgeschlossen dritten. zweiter teil: Theorie der punkmengen". In: Koninklijke Nederlandse Akademie van Wetenschappen te Amsterdam 12.7 (1919).
L. E. J. Brouwer. Brouwer's Cambridge Lectures on Intuitionism. Edited by D. Van Dalen. Cambridge University Press, 1981, pp. 214-215.
L. E. J. Brouwer. "Historical Background, Principles and Methods of Intuitionism". In: Journal of Symbolic Logic 19.2 (1954), pp. 125-125.
Venanzio Capretta and Jonathan Fowler. "The continuity of monadic stream functions". In: 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). June 2017, pp. 1-12.
Paul J. Cohen. "The independence of the continuum hypothesis". In: the National Academy of Sciences of the United States of America 50.6 (Dec. 1963), pp. 1143-1148.
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.
Thierry Coquand and Bassel Mannaa. "The Independence of Markov's Principle in Type Theory". In: FSCD 2016. Vol. 52. LIPIcs. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2016, 17:1-17:18.
Thierry Coquand, Bassel Mannaa, and Fabian Ruch. "Stack semantics of type theory". In: LICS 2017. IEEE Computer Society, 2017, pp. 1-11.
Karl Crary. "Type-Theoretic Methodology for Practical Programming Languages". PhD thesis. Ithaca, NY: Cornell University, Aug. 1998.
Dirk van Dalen. "An interpretation of intuitionistic analysis". In: Annals of mathematical logic 13.1 (1978), pp. 1-43.
Michael A. E. Dummett. Elements of Intuitionism. Second. Clarendon Press, 2000.
VH Dyson and Georg Kreisel. Analysis of Beth's semantic construction of intuitionistic logic. Stanford University. Applied Mathematics and Statistics Laboratories, 1961.
Martín H. Escardó and Chuangjie Xu. "The Inconsistency of a Brouwerian Continuity Principle with the Curry-Howard Interpretation". In: TLCA 2015. Vol. 38. LIPIcs. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015, pp. 153-164.
Hugo Herbelin. "A Constructive Proof of Dependent Choice, Compatible with Classical Logic". In: LICS 2012. IEEE, 2012, pp. 365-374.
Douglas J. Howe. "Equality in Lazy Computation Systems". In: LICS 1989. IEEE Computer Society, 1989, pp. 198-203.
Hajime Ishihara and Peter Schuster. "A continuity principle, a version of Baire's theorem and a boundedness principle". In: J. Symb. Log. 73.4 (2008), pp. 1354-1360.
Stephen C. Kleene and Richard E. Vesley. The Foundations of Intuitionistic Mathematics, especially in relation to recursive functions. North-Holland Publishing Company, 1965.
Georg Kreisel. "Lawless sequences of natural numbers". In: Compositio Mathematica 20 (1968), pp. 222-248.
Georg Kreisel. "On weak completeness of intuitionistic predicate logic". In: J. Symb. Log. 27.2 (1962), pp. 139-158.
Georg Kreisel and Anne S. Troelstra. "Formal systems for some branches of intuitionistic analysis". In: Annals of Mathematical Logic 1.3 (1970), pp. 229-387.
Saul A. Kripke. "Semantical Considerations on Modal Logic". In: Acta Philosophica Fennica 16.1963 (1963), pp. 83-94.
John Longley. "When is a Functional ProgramNot a Functional Program?" In: ICFP'99. ACM, 1999, pp. 1-7.
Per Martin-Löf. Intuitionistic Type Theory. Studies in Proof Theory, Lecture Notes 1. Napoli: Bibliopolis, 1984.
Etienne Miquey. "A sequent calculus with dependent types for classical arithmetic". In: LICS 2018. 2018.
Joan R. Moschovakis. "An intuitionistic theory of lawlike, choice and lawless sequences". In: Logic Colloquium'90: ASL Summer Meeting in Helsinki. Association for Symbolic Logic. 1993, pp. 191-209.
Nuprl in Coq. https://github.com/vrahli/NuprlInCoq.
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, Mark Bickford, and Robert L. Constable. "Bar induction: The good, the bad, and the ugly". In: LICS 2017. Extended version avaible at https://vrahli.github.io/articles/ba r-induction-lics-long.pdf. IEEE Computer Society, 2017, pp. 1-12.
Vincent Rahli, Liron Cohen, and Mark Bickford. "A Verified Theorem Prover Backend Supported by a Monotonic Library". Submitted. 2018.
Michael Rathjen. "A note on Bar Induction in Constructive Set Theory". In: Math. Log. Q. 52.3 (2006), pp. 253-258.
Anne S. Troelstra. Choice sequences: a chapter of intuitionistic mathematics. Clarendon Press Oxford, 1977.
Anne S. Troelstra. "Choice Sequences and Informal Rigour". In: Synthese 62.2 (1985), pp. 217-227.
Anne S. Troelstra andDirk vanDalen. Constructivismin MathematicsAn Introduction. Vol. 121. Studies in Logic and the Foundations of Mathematics. Elsevier, 1988.
The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study: http://homotopytypetheory.org/book, 2013.
Wim Veldman. "Understanding and Using Brouwer's Continuity Principle". In: Reuniting the Antipodes - Constructive and Nonstandard Views of the Continuum. Vol. 306. Synthese Library. Springer Netherlands, 2001, pp. 285-302.
Beth E.W. "Semantic Construction of Intuitionistic Logic". In: Journal of Symbolic Logic 22.4 (1957), pp. 363-365.
