Stuart Allen. An Abstract Semantics for Atoms in Nuprl. Tech. rep. Cornell University, 2006.
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, Mark Bickford, Robert L. Constable, and Vincent Rahli. "A Type Theory with Partial Equivalence Relations as Types". Presented at TYPES 2014. 2014.
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.
Michael J. Beeson. Foundations of Constructive Mathematics. Springer, 1985.
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.
Ulrich Berger and Paulo Oliva. "Modified bar recursion". In: Mathematical Structures in Computer Science 16.2 (2006), pp. 163-183.
Yves Bertot and Pierre Casteran. Interactive Theorem Proving and Program Development. http://www.labri.fr/perso/casteran/CoqA rt. SpringerVerlag, 2004.
Marc Bezem. "Equivalence of Bar Recursors in the Theory of Functionals of Finite Type". In: Archive for Mathematical Logic 27.2 (1988), pp. 149-160.
Mark Bickford. "Unguessable Atoms: A Logical Foundation for Security". In: Verified Software: Theories, Tools, Experiments, Second Int'l Conf. Vol. 5295. LNCS. Springer, 2008, pp. 30-53.
Mark Bickford and Robert Constable. "Inductive Construction in Nuprl Type Theory Using Bar Induction". Presented at TYPES 2014 http://nuprl.org/KB/show.phpID=723. 2014.
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/pmw iki.php. Springer, 2009, pp. 73-78.
Edwin Brady. "IDRIS-: systems programming meets full dependent types". In: PLPV 2011. ACM, 2011, pp. 43-54.
Douglas Bridges and Fred Richman. Varieties of Constructive Mathematics. London Mathematical Society Lecture Notes Series. Cambridge University Press, 1987.
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. "From frege to Gödel: A Source Book in Mathematical Logic, 1879-1931". In: Harvard University Press, 1927. Chap. On the Domains of Definition of Functions.
L.E.J. Brouwer. "Historical background, principles and methods of intuitionism". In: South African journal of science 49.3,4 (1952).
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.
Paul J. Cohen. "The independence of the continuum hypothesis II". In: The National Academy of Sciences of the United States of America 51.1 (Jan. 1964), pp. 105-110.
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. Upper Saddle River, NJ, USA: Prentice-Hall, Inc., 1986.
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 and Scott F. Smith. "Computational Foundations of Basic Recursive Function Theory". In: Theoretical Computer Science 121.1&2 (1993), pp. 89-112.
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.
Gerrit van Der Hoeven and Ieke Moerdijk. "Sheaf models for choice sequences". In: Ann. Pure Appl. Logic 27.1 (1984), pp. 63-107.
Michael A. E. Dummett. Elements of Intuitionism. Second. Clarendon Press, 2000.
Martín Hötzel 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.
Martín Escardó and Paulo Oliva. "Bar Recursion and Products of Selection Functions". In: J. Symb. Log. 80.1 (2015), pp. 1-28.
Martin Hofmann. "Extensional concepts in intensional type theory". PhD thesis. University of Edinburgh, 1995.
William A. Howard. "Functional interpretation of bar induction by bar recursion". eng. In: Compositio Mathematica 20 (1968), pp. 107-124.
William A. Howard and Georg Kreisel. "Transfinite Induction and Bar Induction of Types Zero and One, and the Role of Continuity in Intuitionistic Analysis". In: J. Symb. Log. 31.3 (1966), pp. 325-358.
Douglas J. Howe. "Equality in Lazy Computation Systems". In: LICS 1989. IEEE Computer Society, 1989, pp. 198-203.
Douglas J. Howe. "Importing Mathematics from HOL into Nuprl". In: Theorem Proving in Higher Order Logics. Vol. 1125. LNCS. Berlin: Springer-Verlag, 1996, pp. 267-282.
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/.
S.C. Kleene and R.E. Vesley. The Foundations of Intuitionistic Mathematics, especially in relation to recursive functions. North-Holland Publishing Company, 1965.
Alexei Kopylov. "Type Theoretical Foundations for Data Structures, Classes, and Objects". PhD thesis. Ithaca, NY: Cornell University, 2004.
G. Kreisel and A.S. Troelstra. "Formal systems for some branches of intuitionistic analysis". In: Annals of Mathematical Logic 1.3 (1970), pp. 229-387.
Georg Kreisel. "A Remark on Free Choice Sequences and the Topological Completeness Proofs". In: J. Symb. Log. 23.4 (1958), pp. 369-388.
Georg Kreisel. "Lawless sequences of natural numbers". eng. 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.
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.
Paul F. Mendler. "Inductive Definition in Type Theory". PhD thesis. Ithaca, NY: Cornell University, 1988.
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.
Paulo Oliva. "Understanding and Using Spector's Bar Recursive Interpretation of Classical Analysis". In: CiE 2006. Vol. 3988. LNCS. Springer, 2006, pp. 423-434.
Paulo Oliva and T.Powell. "On Spector's bar recursion". In: Math. Log. Q. 58.4-5 (2012), pp. 356-265.
Christine Paulin-Mohring. "Inductive Definitions in the system Coq-Rules and Properties". In: TLCA'93. Vol. 664. LNCS. Springer, 1993, pp. 328-345.
Andrew M. Pitts. "Nominal Logic: A First Order Theory of Names and Binding". In: TACS 2001. Vol. 2215. LNCS. Springer, 2001, pp. 219-242.
T.Powell. "On Bar Recursive Interpretations of Analysis". PhD thesis. Queen Mary University of London, Aug. 2013.
Vincent Rahli. "Exercising Nuprl's Open-Endedness". In: ICMS 2016. Vol. 9725. LNCS. Springer, 2016, pp. 18-27.
Vincent Rahli and Mark Bickford. "A Nominal Exploration of Intuitionism". Extended version of CPP 2016 paper: http://www. nuprl.org/html/Nuprl2Coq/continuity-long.pdf. 2015.
Vincent Rahli and Mark Bickford. "A nominal exploration of intuitionism". In: CPP 2016. ACM, 2016, pp. 130-141.
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.
Vincent Rahli, Mark Bickford, and Robert L. Constable. "Bar Induction: The Good, the Bad, and the Ugly". Extended version avaible at http://www.nuprl.org/html/Nuprl2Coq/bar-inductionlics-long.pdf. Apr. 2017.
Michael Rathjen. "A note on Bar Induction in Constructive Set Theory". In: Math. Log. Q. 52.3 (2006), pp. 253-258.
Michael Rathjen. "Constructive Set Theory and Brouwerian Principles". In: J. UCS 11.12 (2005), pp. 2008-2033.
Michael Rathjen. "The Role of Parameters in Bar Rule and Bar Induction". In: J. Symb. Log. 56.2 (1991), pp. 715-730.
Helmut Schwichtenberg. "On Bar Recursion of Types 0 and 1". In: J. Symb. Log. 44.3 (1979), pp. 325-329.
Scott F. Smith. "Partial Objects in Type Theory". PhD thesis. Ithaca, NY: Cornell University, 1989.
Clifford Spector. "Provably recursive functionals of analysis: A consistency proof of analysis by an extension of principles in current intuitionistic mathematics". In: Recursive Function Theory: Proc. Symposia in Pure Mathematics. Vol. 5. American Mathematical Society, 1962, pp. 1-27.
A.S. Troelstra. "A Note on Non-Extensional Operations in Connection With Continuity and Recursiveness". In: Indagationes Mathematicae 39.5 (1977), pp. 455-462.
A.S. Troelstra. Choice Sequences: A Chapter of Intuitionistic Mathematics. Clarendon Press, 1977.
A.S. Troelstra. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. New York, Springer, 1973.
A.S. Troelstra and D. van Dalen. Constructivism in Mathematics An 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. "Brouwer's Fan Theorem as an axiom and as a contrast to Kleene's alternative". In: Arch. Math. Log. 53.5-6 (2014), pp. 621-693.
Wim Veldman. "Brouwer's real thesis on bars". In: Philosophia Scientiæ CS6 (2006), pp. 21-42.
Wim Veldman. "Some Applications of Brouwer's thesis on Bars". In: One Hundred Years of Intuitionism. Birkhäuser, 2008, pp. 326-340.
Wim Veldman. "Understanding and Using Brouwer's Continuity Principle". English. In: Reuniting the Antipodes-Constructive and Nonstandard Views of the Continuum. Vol. 306. Synthese Library. Springer Netherlands, 2001, pp. 285-302.
Wim Veldman and Mark Bezem. "Ramsey's theorem and the pigeonhole principle in intuitionistic mathematics". In: J. of the London Mathematical Society s2-47 (2 1993), pp. 193-211.
Richard Vesley. "Realizing Brouwer's Sequences". In: Ann. Pure Appl. Logic 81.1-3 (1996), pp. 25-74.
Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt. "Stop When You Are Almost-Full-Adventures in Constructive Termination". In: ITP 2012. Vol. 7406. LNCS. Springer, 2012, pp. 250-265.
