Abstract
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.
We are deeply indebted to many people, in particular Jean-Yves Girard, without whose work the present exercise could not have been attempted by us. John Crossley wishes to acknowledge important and useful conversations with Bill Howard, Anil Nerode and Jeff Remmel and to acknowledge the significant contributions of Andrei Voronkov, while supported by Australian Research Council grant no. 9101614, which helped to clarify the way to the present approach. John Crossley’s research was partly supported by the Mathematical Sciences Institute, Cornell University and the University of California at San Diego. John Shepherdson’s research was partly supported by the IBM Interface Logic Programming Project at Monash University, IBM Research Agreement no. 15760046.
This work results from a visit by John Crossley to Anil Nerode at the Mathematical Sciences Institute, Cornell University, in 1988. At that time we intensively studied Girard’s DEA lecture notes (subsequently published as Girard [1989]). John Crossley wishes to thank Anil for this and other opportunities over many years.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abramsky, S. [1990], Computational Interpretations of Linear Logic. Technical Report 90/20, Department of Computing, Imperial College of Science, Technology and Medicine, London, England.
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.
Chang, C.-C. and H.J. Keisler [1973], Model Theory. North-Holland, Amsterdam; American Elsevier, New York.
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.
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.
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.
Curry, H.B. and R. Feys [1958], Combinatory Logic, vol. I. North-Holland, Amsterdam.
Fenstad, J.E. (ed.) [1971], Proceedings of the Second Scandinavian Logic Symposium. North-Holland, Amsterdam.
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.
Gallier, J. [1991], Constructive Logics. Part I: A Tutorial on Proof Systems and Typed λ-Calculi. Research Report 8, DEC Paris Research Laboratory.
Gentzen, G. [1943-5], Untersuchungen über das logische Schliessen. Math. Z. 39, 176–210, 405–341.
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.
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.
Girard, J.-Y. with P. Taylor and Y. Lafont [1989], Proofs and Types. Cambridge University Press, Cambridge.
Harrop, R. [1956], On disjunctions and existential statements in Intuitionistic systems of logic. Math. Annalen 132, 347–361.
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.
Hindley, J.R. and J.P. Seldin [1986], Introduction to Combinators and λ-calculus. Cambridge University Press, Cambridge.
Howard, W.A. [1980], The formulae-as-types notion of construction, in Seldin and Hindley (Eds.) [1980], Academic Press, London, 479–490.
Kleene, S.C. [1945], On the interpretation of intuitionistic number theory, J. Symb. Logic 10, 109–124.
Kleene, S.C. [1952], Introduction to metamathematics. North-Holland, Amsterdam; Noordhoff, Groningen; Van Nostrand, New York & Toronto.
Kleene, S.C. [1962], Disjunction and existence under implication in elementary intuitionistic formalisms, J. Symb. Logic 27, 11–18.
Kleene, S.C. [1963], An addendum, J. Symb. Logic 28, 154–156.
McCarty, C. [D.] [1986], Realizability and recursive set theory. Annals of Pure and Applied Logic, 32, 153–183.
Mendelson, E. [1964], Introduction to Mathematical Logic. Van Nostrand, Princeton, New Jersey.
Nerode, A. and R. Shore, Applied Logic (in preparation).
Prawitz, D. [1965], Natural Deduction: A proof-theoretical study. Almqvist & Wiksells, Uppsala.
Prawitz, D. [1971], Ideas and results in proof theory, in Fenstad, [1971], 235–307.
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.
Russell, B.A.W. and A.N. Whitehead [1913], Principia Mathematica, 3 vols. Cambridge University Press.
Schönfinkel, M. [1924], Über die Bausteine der mathematischen Logik. Mathematische Annalen, Vol. 92, 305–316. (Translated in van Heijenoort [1967], 355–366.)
Seldin, J.P. and J.R. Hindley (Eds.) [1980], To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, London.
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.
Troelstra, A.S. (Ed.) [1973], Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Springer Lecture Notes in Mathematics 344.
van Heijenoort, J. (Ed.) [1967], From Frege to Gödel. Cambridge, Mass., U.S.A.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1993 Springer Science+Business Media New York
About this chapter
Cite this chapter
Crossley, J.N., Shepherdson, J.C. (1993). Extracting programs from proofs by an extension of the Curry-Howard process. In: Crossley, J.N., Remmel, J.B., Shore, R.A., Sweedler, M.E. (eds) Logical Methods. Progress in Computer Science and Applied Logic, vol 12. Birkhäuser, Boston, MA. https://doi.org/10.1007/978-1-4612-0325-4_8
Download citation
DOI: https://doi.org/10.1007/978-1-4612-0325-4_8
Publisher Name: Birkhäuser, Boston, MA
Print ISBN: 978-1-4612-6708-9
Online ISBN: 978-1-4612-0325-4
eBook Packages: Springer Book Archive