Source: http://nuprl.org/book/Bibliography.html
Timestamp: 2019-04-19 19:12:42+00:00

Document:
An introduction to inductive definitions.
In Handbook of Mathematical Logic, J. Barwise, ed.
North-Holland, Amsterdam, 1977, pages 739-782.
The type theoretic interpretation of constructive set theory.
A. MacIntyre, L. Pacholaki, and J. Paris, eds.
North-Holland, Amsterdam, 1978, pages 55-66.
Alfred V. Aho and J. D. Ullman.
L. Aiello, M. Aiello, and R. W. Weyhrauch.
Pascal in LCF: semantics and examples of proof.
The Semantics of Type Theoretic Languages.
Cornell University, August 1986 (expected).
John M. Anderson and Henry W. Johnstone.
Transfinite Type Theory with Transfinite Type Variables.
J. Symbolic Logic, v. 36 (1971), pages 414-432.
M. Artin, A. Grothendieck, and J. L. Verdier.
Théories des topos et cohomologie étale des schémas.
In Lecture Notes in Mathematics, vols. 269 and 270.
Springer-Verlag, New York, 1972 (first appeared in 1963).
A Note on Subtypes in Martin-Löf's Theory of Types.
Algorithm Development in Martin-Löf's Type Theory.
Computer Science Department, University of Essex, England, 1985.
Mathematical Theory of Program Correctness.
Prentice-Hall, Englewood Cliffs, NJ, 1980.
H. Barringer, J. H. Cheng, and C. B. Jones.
A Logic Covering Undefinedness in Program Proofs.
Department of Computer Science, University of Manchester, England, 1984.
Jon Barwise and John Perry.
MIT Press, Cambridge, MA, 1983.
A Logic for Correct Program Development.
Joseph L. Bates and Robert L. Constable.
J. L. Bates and R. L. Constable.
Cornell University, Ithaca, NY, 1983.
Formalizing constructive mathematics: why and how?
Springer-Verlag, New York, 1981, pages 146-190.
Proving programs and programming proofs.
In International Congress on Logic, Methodology and Philosophy of Science, Salzburg, Austria. North-Holland, Amsterdam, 1983.
Semantic construction of intuitionistic logic.
Amsterdam, N.R. 19, n. 11, (1956), pages 357-388.
Mathematics as a numerical language.
J. Myhill, et al., eds.
North-Holland, Amsterdam, 1970, pages 53-71.
Errett Bishop and Douglas Bridges.
Errett Bishop and H. Cheng.
Mem. Am. Math. Soc. 116, 1972.
Artificial Intelligence v. 9 (1977), pages 1-36.
W. Bledsoe, R. Boyer, and W. Henneman.
Computer proofs of limit theorems.
Artificial Intelligence v. 2 (1971), pages 55-77.
Elements of Mathematics, Vol. I: Theory of Sets.
R. Boyer and J. S. Moore.
Academic Press, New York, 1979.
Metafunctions: proving them correct and using them efficiently as new proof procedures.
R. S. Boyer and J. S. Moore, eds.
Academic Press, New York, 1981, pages 103-184.
On the significance of the principle of excluded middle in mathematics, especially in function theory.
In [vanHeijenoort 67], pages 334-345.
The mathematical language AUTOMATH, its usage and some of its extensions.
Lecture Notes in Mathematics, Vol. 125.
Springer-Verlag, New York, 1970, pages 29-61.
A survey of the project AUTOMATH.
J. P. Seldin and J. R. Hindley, eds.
Academic Press, New York, 1980, pages 589-606.
W. Buchholz, S. Feferman, W. Pohlers, and W. Sieg.
Iterated Inductive Definitions and Subsystems of Analysis.
The Computer Modelling of Mathematical Reasoning.
Academic Press, New York, 1983.
Proving properites of programs by structural induction.
Comp. J. v. 12, n. 1, (1969), pages 41-48.
R. M. Burstall and B. Lampson.
A kernel language for abstract data types and modules.
Lecture Notes in Computer Science, Vol. 173.
Springer-Verlag, New York, 1984 pages 1-50.
R. M. Burstall, D. B. MacQueen, and D. T. Sanella.
HOPE: an experimental applicative language.
Stanford University, Stanford, CA, 1980, pages 136-143.
Polymorphism: The ML/LCF/Hope Newsletter I (1983).
A semantics of multiple inheritance.
Springer-Verlag, New York, 1984, pages 51-67.
Toward a logical theory of program data.
Lecture Notes in Computer Science Vol. 131.
Springer-Verlag, New York, 1982, pages 37-51.
Notes on constructive probability theory.
Ann. Probability, v. 2 (1974), pages 51-75.
Eugene Charniak and Drew McDermott.
Derivation of a Parsing Algorithm in Martin-Löf's Theory of Types.
Department of Computer Science, Heriot-Watt University, Edinburgh, Scotland, 1985.
A formulation of the simple theory of types.
J. Symbol. Logic v. 5, (1940), pages 56-68.
Annals of Mathematics Studies, No. 6.
Princeton University Press, Princeton, NJ, 1951.
Edmond M. Clarke, Jr., E. A. Emerson and A. P. Sistla.
Automatic verification of finite state concurrent systems using temporal logic specification: a practical approach.
In 10th ACM Symposium on Principles of Programming Languages.
Type Theoretic Models of Concurency.
W. F. Clocksin and C. S. Mellish.
Constructive mathematics and automatic programs writers.
On the theory of programming logics.
Boulder, Colorado, May 1977, pages 269-285.
Constructive mathematics as a programming logic I: some principles of theory.
Robert L. Constable and N. P. Mendler.
Recursive definitions in type theory.
Springer-Verlag, New York, 1985, pages 61-78.
Robert L. Constable, Scott D. Johnson, and Carl D. Eichenlaub.
Robert L. Constable, Todd B. Knoblock, and Joseph L. Bates.
Writing programs that construct proofs.
Robert L. Constable and Michael J. O'Donnell.
Robert L. Constable and Daniel R. Zlatin.
The type theory of PL/CV3.
Thierry Coquand and Gerard Huet.
Constructions: A Higher Order Proof System for Mechanizing Mathematics.
EUROCAL 85, Linz, Austria, April 1985.
H. B. Curry, R. Feys, and W. Craig.
H. B. Curry, J. R. Hindley, and J. P. Seldin.
The Language Theory of AUTOMATH.
Raven Press, New York, 1965.
Randall Davis and Douglas B. Lenat.
Knowledge-Based Systems in Artificial Intelligence.
M. Davis and J. T. Schwartz.
Metamathematical extensibility for theorem verifiers and proof checkers.
Prentice-Hall, Englewood Cliffs, NJ, 1976.
J. E. Donahue and A. J. Demers.
Cornell University, Ithaca, NY, September 1979.
TOPLAS, v. 7, n. 3, (July 1985), pages 426-445.
Veronique Donzeau-Gouge, Gerard Huet, Gilles Kahn, and Bernard Lang.
Programming environments based on structured editors: the Mentor experience.
INRIA, Rapports de Recherches, No. 26, July 1980.
Artificial Intelligence, v. 12, n. 3.
Elements of Intuitionism, Oxford Logic Series.
Constructive theories of functions and classes.
North-Holland, Amsterdam, 1979, pages 159-224.
Proof Methods for Modal and Intuitionistic Logics.
D. Reidel, Dordrecht, The Netherlands, 1983.
S. Fortune, D. Leivant, and M. O'Donnell.
The expressiveness of simple and second order type structures.
Begriffsschrift, a formula language, modeled upon that for arithmetic, for pure thought.
In [vanHeijenoort 67], pages 1-82.
The consistency of classical set theory relative to set theory with intuitionistic logic.
Semantical Investigations in Heyting's Intuitionistic Logic.
D. Reidel, Dordrecht, The Netherlands, 1981.
In The Collected Papers of Gerhard Gentzen, M. E. Szabo, ed.
Une extension de l'interpretation de Godel a l'analyse, et son application a l'elimination des coupures dans l'analyse et la theorie des types.
North-Holland, Amsterdam, 1971, pages 63-92.
Proofs as descriptions of computation.
Springer-Verlag, New York, 1980, pages 39-52.
J. A. Goguen, J. W. Thatcher and E. G. Wagner.
Initial algebra approach to the specification, correctness and implementation of abstract data types.
In Current Trends in Programming Methodology, Vol. IV, R.
TOPI: The Categorial Analysis of Logic.
Epistemic arithmetic is a Conservative Extension of Intuitionistic Arithmetic.
Nicolas D. Goodman and John Myhill.
The formalization of Bishop's constructive mathematics.
Lecture Notes in Mathematics, Vol. 274.
Springer-Verlag, New York, 1972, pages 83-96.
Michael Gordon, Arthur Milner, and Christopher Wadsworth.
Programming Methodology: A Collection of Articles by Members of IFIP WG2.3.
J. Guttag and J. Horning.
The algebraic specification of abstract data types.
In Programming Methodology, D. Gries, ed.
Aspects of the Implementation of Type Theory.
do considered od: a contribution to the programming calculus.
From Frege to Gödel: A Sourcebook in Mathematical Logic.
Harvard University Press, Cambridge, MA, 1967.
Die formalen Regeln der intuitionistischen Logik.
Academic Press, New York, 1972, pages 83-174.
The formulas-as-types notion of construction.
In To H. B. Curry: Essays on Combinatory Logic, Lambda-Calculus, and Formalism, J. P. Seldin and J. R. Hindley, eds.
Academic Press, New York, 1980, pages 479-490.
A unification algorithm for typed lambda-calculus.
A Computer System for Checking Proofs.
UMI Press, New York, 1983.
Checking Landau's ``Grundlagen'' in the AUTOMATH System.
Eindhoven University, Eindhoven, The Netherlands, 1977.
Also in Math. Centre Tracts No. 83, Math. Centre, Amsterdam, 1979.
Microelectronics and the Personal Computer.
Alan Kay and Adele Goldberg.
Computer, v. 31, (March 1977).
On the interpretation of intuitionistic number theory.
Van Nostrand, Princeton, NJ, 1952.
Stephen C. Kleene and R. E. Vesley.
The Foundations of Intuitionistic Mathematics.
Formal Metamathematics and Reflection in Constructive Type Theory.
Doctoral Dissertation, Computer Science Department, Cornell University, 1986.
The Art of Computer Programming, Vol. I.
Complexity of Finitely Presented Algebras.
AVID: A System for the Interactive Development of Verifiably Correct Programs.
Hilbert's program and the search for automatic proof procedures.
In Symposium on Automatic Demonstration, Lecture Notes in Mathematics, Vol. 125.
Springer-Verlag, New York (1970), pages 128-146.
Cambridge University Press, Cambridge, 1976.
Advances in Mathematics v. 35 (1980).
An abstract notion of realizability for which intuitionistic predicate calculus is complete.
In Intuitionism and Proof Theory, J. Myhill, A. Kino, and R. E. Vesley, eds.
North-Holland, Amsterdam, 1970, pages 227-234.
Structural semantics for polymorphic data types (preliminary report).
In Proceedings of the 10th ACM Symposium in the Principles of Programming Languages, ACM, New York, 1983, pages 155-166.
R. C. Linger, H. D. Mills and B. I. Witt.
Structured Programming Theory and Practice.
Automated Theorem Proving: A Logical Basis.
Foundations for categories and sets.
In Category Theory, Homology Theory and Their Applications II, Lecture Notes in Mathematics, Vol. 92.
Springer-Verlag, New York, 1969, pages 146-164.
Polymorphism Newsletter, v. 2, n. 2 (1985).
D. B. MacQueen, G. D. Plotkin, and R. Sethi.
An ideal model for recursive polymorphic types.
Z. Manna and R. Waldinger.
A deductive approach to program synthesis.
The Logical Basis for Computer Programming.
Almqvist & Wiksell, Stockholm, 1970.
In Proceedings of the Second Scandinavian Logic Symposium, J. E. Fenstad ed.
North-Holland, Amsterdam, 1971, pages 179-216.
An intuitionistic theory of types: predicative part.
H. E. Rose and J. C. Shepherdson, eds.
North-Holland, Amsterdam, 1973, pages 73-118.
Constructive mathematics and computer programming.
In Sixth International Congress for Logic, Methodology, and Philosophy of Science.
North-Holland, Amsterdam, 1982, pages 153-175.
Studies in Proof Theory Lecture Notes, BIBLIOPOLIS, Napoli, 1984.
Reasoning Utility Package User's Manual, Version One.
AI Lab. MIT, AIM-667, April 1982.
Computer programs for checking mathematical proofs.
In Proceedings of the Symposia in Pure Mathematics, Vol. V, Recursive Function Theory.
American Mathematical Society, Providence, RI, 1962.
A basis for a mathematical theory of computation.
In Computer Programming and Formal Systems.
P. Braffort and D. Herschberg, eds.
North-Holland, Amsterdam, 1963, pages 33-70.
Algol 68, A First and Second Course.
Cambridge University Press, Cambridge, 1978.
Recursive Types and Infinite Objects.
G. Metakides and A. Nerode.
Effective content of field theory.
What is a model of the lambda calculus?
The standard ML core language.
R. Milner and R. Weyhrauch.
Proving computer correctness in mechanized logic.
Edinburgh, Scotland, 1972, pages 51-70.
In Mind Design, J. Haugeland, ed.
MIT Press, Cambridge, MA, 1981, pages 95-128.
John Mitchell and Gordon Plotkin.
Abstract types have existential type.
ACM, New York, 1985, pages 37-51.
Academic Press, New York, 1965.
Elementary Induction on Abstract Structures.
Mechanization of existence proofs of recursive functions.
In Proceedings 7th International Conference on Automated Deduction.
Lecture Notes in Computer Science, Vol. 170.
Springer-Verlag, New York, 1984, pages 460-475.
A system of natural reasoning based on a typed -calculus.
Greg Nelson and Derek C. Oppen.
Simplification by cooperating decision procedures.
North-Holland, Amsterdam, 1982, pages 109-122.
Programming in constructive set theory: some examples.
In Proceedings 1981 Conference on Functional Programming Languages and Computer Architecture.
Portsmouth, England, 1981, pages 141-153.
Bengt Nordstrom and Kent Petersson.
In Proceedings IFIP '83, R. E. A. Mason, ed.
North-Holland, Amsterdam, 1983, pages 915-920.
Bengt Nordstrom and Jan Smith.
Propositions, types, and specifications in Martin-Löf's type theory.
BIT, v. 24, n. 3 (1984), pages 288-301.
PRL: Proof Refinement Logic Programmer's Manual (Lambda PRL, VAX Version).
Computer Science Department, Cornell University, New York, 1983.
Equational Logic as a Programming Language.
MIT Press, Cambridge, MA, 1985.
M. S. Paterson and M. N. Wegman.
Tactics and Tacticals in Cambridge LCF.
University of Cambridge, July 1983.
A higher-order implementation of rewriting.
Verifying the Unification Algorithm in LCF.
University of Cambridge, March 1984.
Lessons learned from LCF: a survey of natural deduction proofs.
Comp. J. v. 28 n. 5 (1985).
A Programming System for Type Theory.
Kent Petersson and Jan Smith.
Program Derivation in Type Theory: The Polish Flag Problem.
Doctoral Dissertation, Stanford University, 1966.
LCF considered as a programming language.
University Press of America, Washington, DC, 1982.
Formal reductions of the general combinatorial decision problem.
North-Holland, Amsterdam, 1970, pages 235-308.
Set Theory and Its Logic.
Belknap Press, Combridge, MA, 1963.
MIT Press, Cambridge, MA, 1984.
Thomas W. Reps and B. Alpern.
In 11th ACM Symposium on Principles of Programming Languages.
Thomas W. Reps and Tim Teitelbaum.
Technical Report, TR 84-619, Cornell University, Ithaca, NY, August 1985.
Towards a theory of type structure.
Lecture Notes in Computer Science Vol. 19.
Springer-Verlag, New York, 1974, pages 408-423.
Types, abstraction, and parametric polymorphism.
North-Holland, Amsterdam, 1983, pages 513-523.
A machine-oriented logic based on the resolution principle.
Computational logic: the unification algorithm.
B. Meltzer and D. Michie, eds.
Edinburgh, Scotland, 1971, pages 63-72.
Mathematical logic as based on a theory of types.
In Logic and Knowledge, R. D. Marsh, ed.
George Allen & Unwin, London, 1956.
The Extraction and Optimization of Programs from Constructive Proofs.
Doctoral Dissertation, Computer Science Department, Cornell University, 1985.
W. L. Scherlis and D. Scott.
First steps toward inferential programming.
In Proceedings IFIP Congress, Paris, 1983.
Springer-Verlag, New York, 1970, pages 237-275.
SIAM J. Computing, v. 5 (1976), pages 522-587.
University of Colorado, July 1985.
Jorg Siekmann and Graham Wrightson.
An interpretation of Martin-Löf's type theory in a type-free theory of propositions.
A Note on Tactics in LCF.
University of Edinburgh, Edinburgh, Scotland, 1983.
Theoretical Computer Science, v. 9, (1979), pages 73-81.
Common LISP - The Language.
Digital Press, Burlington, MA, 1984.
Combinators, -terms, and Proof Theory.
D. Reidel, Dordrecht, The Netherlands, 1972.
Approach to Programming Language Theory.
MIT Press, Cambridge, MA, 1977.
University-Level Computer-Assisted Instruction at Stanford: 1968-1981.
Institute for Mathematical Studies in the Social Sciences, Stanford University, Stanford, CA, 1981.
Intensional interpretation of functionals of finite type.
R. Teitelbaum and T. Reps.
Tableau systems for first order number theory and certain higher order theories.
Lecture Notes in Mathematics, Vol. 344.
Choice Sequences: A Chapter of Intuitionistic Mathematics.
Halsted Press (John Wiley & Sons), New York, 1984.
Prolegomena to a theory of formal reasoning.
A. N. Whitehead and B. Russell.
Cambridge University Press, Cambridge, MA, 1925.
Larry Wos, R. Overbeek, L. Ewing, and J. Boyle.
Formalization of classical mathematics in AUTOMATH.

References: V. 
 v. 
 v. 
 v. 
 v. 
 v. 
 v. 
 v. 
 v. 
 v. 
 v. 
 v. 
 v. 
 v. 
 v. 
 v.