Skip to main content
PRL Project

Logical Investigations, with the Nuprl Proof Assistant
Table of Contents

Previous Page


[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