Logical Investigations, with the Nuprl Proof Assistant
Table of Contents
References
| [BC85] | J. L. Bates and Robert L. Constable. Proofs as programs. In ACM Transactions of Programming Language Systems, 7(1):53-71, 1985. |
| [Bis70] | Errett Bishop. Mathematics as a numerical language. In Intuitionism and Proof Theory. North-Holland, NY, 1970. Pages 53-71. |
| [Con09] | Robert L. Constable. Computational type theory. Scholarpedia, 4(2):7618, 2009. |
| [Gen69] | Gerhard Gentzen. Investigations into logical deduction (1934). In M. Szalo, editor, The Collected Paers of Gerhard Gentzen. North-Holland, Amsterdam, 1969. |
| [Göd58] | K. Gödel. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. In Dialectica, Vol. 12, 1958. Pages 280-287. |
| [GMW79] | Michael Gordon, Robin Milner, and Christopher Wadsworth. Edinburgh LCF: a mechanized logic of computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, NY, 1979. |
| [Tar56] | Alfred Tarski. The Concept of Truth in Formalized Languages. In Logic, Semantics, Metamathematics. Clarendon Press, Oxford, 1956. Pages 152-278. |
Related Books in the Math Library
- Readability Exercise (num theory), by Stuart F. Allen
- Formalizing Constructive Analysis in Nuprl, by Mark Bickford