Extracting programs from proofs by an extension of the Curry-Howard process

  • John N. Crossley
  • John C. Shepherdson
Part of the Progress in Computer Science and Applied Logic book series (PCS, volume 12)


In this paper we provide a general framework for extracting programs from proofs in the language of first order predicate calculus directly, that is to say, without first going through a transformation into second order propositional calculus or other higher order logic.


Induction Hypothesis Free Variable Reduction Rule Natural Deduction Strong Normalization 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Abramsky, S. [1990], Computational Interpretations of Linear Logic. Technical Report 90/20, Department of Computing, Imperial College of Science, Technology and Medicine, London, England.Google Scholar
  2. Avron, A., F. Honsell, I.A. Mason and R. Pollack [1992], Using Typed Lambda Calculus to Implement Formal Systems on a Machine. Journal of Automated Reasoning, 9, 309–354.MathSciNetzbMATHCrossRefGoogle Scholar
  3. Chang, C.-C. and H.J. Keisler [1973], Model Theory. North-Holland, Amsterdam; American Elsevier, New York.zbMATHGoogle Scholar
  4. Cook, S. and A. Urquhart [to appear], Functional Interpretations of Feasibly Constructive Arithmetic. Tech. Report 210/88, Dept of Computer Science, University of Toronto; to appear in Annals of Pure and Applied Logic.Google Scholar
  5. Coquand, T. and G. Huet [1985], Constructions: a higher order proof system for mechanizing mathematics. In Proc. EUROCAL’ 85, Linz, Austria, Lecture notes in Computer Science 203, Springer-Verlag, Berlin.Google Scholar
  6. Crossley, J.N. and J.B. Remmel [1992], Proofs, Programs and Run-Times. To appear in Methods of Logic in Computer Science, Vol. 1, no. 1.Google Scholar
  7. Curry, H.B. and R. Feys [1958], Combinatory Logic, vol. I. North-Holland, Amsterdam.zbMATHGoogle Scholar
  8. Fenstad, J.E. (ed.) [1971], Proceedings of the Second Scandinavian Logic Symposium. North-Holland, Amsterdam.zbMATHGoogle Scholar
  9. Gabbay, D.M. and R.J.G.B. de Queiroz [1992], Extending the Curry-Howard interpretation to linear, relevant and other resource logics. J. Symbolic Logic, 57, No. 4, 1319–1365.MathSciNetzbMATHCrossRefGoogle Scholar
  10. Gallier, J. [1991], Constructive Logics. Part I: A Tutorial on Proof Systems and Typed λ-Calculi. Research Report 8, DEC Paris Research Laboratory.Google Scholar
  11. Gentzen, G. [1943-5], Untersuchungen über das logische Schliessen. Math. Z. 39, 176–210, 405–341.MathSciNetCrossRefGoogle Scholar
  12. Girard, J.-Y. [1971], Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination des coupures dans l’analyse et la théorie des types, in Fenstad [1971], 63–92.Google Scholar
  13. Girard, J.-Y. [1972], Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur. Thèse de Doctorat d’État. Université Paris VII.Google Scholar
  14. Girard, J.-Y. with P. Taylor and Y. Lafont [1989], Proofs and Types. Cambridge University Press, Cambridge.zbMATHGoogle Scholar
  15. Harrop, R. [1956], On disjunctions and existential statements in Intuitionistic systems of logic. Math. Annalen 132, 347–361.MathSciNetzbMATHCrossRefGoogle Scholar
  16. Harrop, R. [1960], Concerning formulas of the types A→ B ν C, A → (Ex)B(x) in Intuitionistic Formal Systems, J. Symb. Logic 25, 27–32.MathSciNetzbMATHCrossRefGoogle Scholar
  17. Hindley, J.R. and J.P. Seldin [1986], Introduction to Combinators and λ-calculus. Cambridge University Press, Cambridge.Google Scholar
  18. Howard, W.A. [1980], The formulae-as-types notion of construction, in Seldin and Hindley (Eds.) [1980], Academic Press, London, 479–490.Google Scholar
  19. Kleene, S.C. [1945], On the interpretation of intuitionistic number theory, J. Symb. Logic 10, 109–124.MathSciNetzbMATHCrossRefGoogle Scholar
  20. Kleene, S.C. [1952], Introduction to metamathematics. North-Holland, Amsterdam; Noordhoff, Groningen; Van Nostrand, New York & Toronto.zbMATHGoogle Scholar
  21. Kleene, S.C. [1962], Disjunction and existence under implication in elementary intuitionistic formalisms, J. Symb. Logic 27, 11–18.MathSciNetCrossRefGoogle Scholar
  22. Kleene, S.C. [1963], An addendum, J. Symb. Logic 28, 154–156.MathSciNetCrossRefGoogle Scholar
  23. McCarty, C. [D.] [1986], Realizability and recursive set theory. Annals of Pure and Applied Logic, 32, 153–183.MathSciNetzbMATHCrossRefGoogle Scholar
  24. Mendelson, E. [1964], Introduction to Mathematical Logic. Van Nostrand, Princeton, New Jersey.Google Scholar
  25. Nerode, A. and R. Shore, Applied Logic (in preparation).Google Scholar
  26. Prawitz, D. [1965], Natural Deduction: A proof-theoretical study. Almqvist & Wiksells, Uppsala.zbMATHGoogle Scholar
  27. Prawitz, D. [1971], Ideas and results in proof theory, in Fenstad, [1971], 235–307.Google Scholar
  28. Reynolds, J.C. [1974], Towards a theory of type structures. In Programming Symposium (Colloque sur la Programmation, Paris), ed. B. Robinet, Springer-Verlag, Berlin, 408–425.CrossRefGoogle Scholar
  29. Russell, B.A.W. and A.N. Whitehead [1913], Principia Mathematica, 3 vols. Cambridge University Press.Google Scholar
  30. Schönfinkel, M. [1924], Über die Bausteine der mathematischen Logik. Mathematische Annalen, Vol. 92, 305–316. (Translated in van Heijenoort [1967], 355–366.)MathSciNetzbMATHCrossRefGoogle Scholar
  31. Seldin, J.P. and J.R. Hindley (Eds.) [1980], To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, London.zbMATHGoogle Scholar
  32. Tait, W.W. [1965], Infinitely long terms of transfinite type. In Formal Systems and Recursive Functions, ed. J.N. Crossley and M.A.E. Dummett, North-Holland, Amsterdam.Google Scholar
  33. Troelstra, A.S. (Ed.) [1973], Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Springer Lecture Notes in Mathematics 344.Google Scholar
  34. van Heijenoort, J. (Ed.) [1967], From Frege to Gödel. Cambridge, Mass., U.S.A.Google Scholar

Copyright information

© Springer Science+Business Media New York 1993

Authors and Affiliations

  • John N. Crossley
    • 1
  • John C. Shepherdson
    • 2
  1. 1.Department of Mathematics and Department of Computer ScienceMonash UniversityClaytonAustralia
  2. 2.School of MathematicsUniversity of BristolBristolEngland

Personalised recommendations