Abstract
The relationship between constructive mathematics and computer science has been noticed for a long while. But it is rather recent that live interactions between constructive mathematics and computer science began. In theoretical aspects, metamathematics of constructive mathematics are utilized to give semantics of higher order functional programming languages. Researches of constructive mathematics in computer science are not just theoretical. Quite a few systems based on constructive mathematics have been designed and implemented. They are program verification systems, program extraction systems, and high-level programming languages. These developments of systems need theoretical investigations as well and so give new insights into constructive mathematics. Applications of constructive mathematics to semantics of programming languages have begun to produce significant feedbacks to constructive mathematics and related areas, see Hyland (1987), Longo and Moggi (1988+α). Although researches on constructive systems have not yet been used to unvail new aspects of constructive mathematics, there are clues of possible applications of computer systems to theoretical researches in constructive mathematics Coquand (1986), Howe (1987). It is reasonable to imagine that constructive mathematicians a decade later will be helped by computer systems as mathematicians are now helped by computer algebra systems like REDUCE. In this paper, we will give a survey of existing systems based on constructive mathematics to show the readers how constructive theories are used in actual systems.
This paper was written while the author was visiting LFCS, Department of Computer Science, University of Edinburgh. This work is supported by Japanese Organization of Promotion of Science.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Basin, D.A., 1988, An Environment for Automated Reasoning About Partial Functions, in: Springer Lecture Notes in Computer Science 310.
Beeson, M.J., 1985, “The Foundations of Constructive Mathematics”, Springer, Berlin.
Beeson, M.J., 1987, Towards a Computation System Based on Set Theory, preprint.
Bishop, E., 1967, “Foundations of Constructive Analysis,” McGraw-Hill.
de Bruijn, N.G., 1980, A survey of the project AUTOMATE, in: “Essays in Combinatory Logic, Lambda Calculus, and Formalism,” Seldin, J.P. and Hindley, J.R., eds., Academic Press, New York.
Burstall, R., and Lampson, B., 1984, A kernel language for abstract data types and modules, in: Springer Lecture Note in Computer Science 173.
Constable, R.L., 1971, Constructive mathematics and automatics programs writers, in: “Proceedings of IFIP Congress,” Ljubljana.
Constable, R.L., et al., 1986, “Implementing Mathematics with the Nuprl Proof Development System,” Prentice-Hall.
Constable, R.L., Johnson, S.D., and Eichenlaub, C.D., 1982, Introduction to the PL/CV2 Programming Logic, Springer Lecture Notes in Computer Science 135.
Constable, R.L., and Smith, S.F., 1987, Partial Objects in Constructive Type Theory, in: “Second Annual Symposium on Logic in Computer Science,” IEEE.
Coquand, T., 1986, An analysis of Girard’s paradox, in: “First Annual Symposium on Logic in Computer Science,” IEEE.
Coquand, T., and Huet, G., 1985, Constructions: A higher order proof system of mechanizing mathematics, in: Springer Lecture Notes in Computer Science 203.
Coquand, T., and Huet, G., 1988, The Calculus of Constructions, Information and Computation 76.
Despeyroux, J., 1988, First experiments with theorem proving in Centaur: the Calculus of Construction, the Edinburgh Logical Framework, and Theo, in: “GIPE, ESPRIT project 348, Third annual review report.”
Feferman, S., 1975, A language and axioms for explicit mathematics, in: Springer Lecture Notes in Computer Science 450.
Feferman, S., 1979, Constructive theories of functions and classes, in: “Logic Colloquium’78,” North-Holland, Amsterdam.
Felty, A. and Miller, D., Specifying Theorem Provers in a Higher-order Logic Programming Language, in: Springer Lecture Notes in Computer Science 310.
Friedman, H., 1973, Some applications of Kleene’s methods for intuitionistic systems, in: Springer Lecture Note in Mathematics 337, Springer, Berlin.
Friedman, H., 1977, Set theoretic foundations for constructive analysis, Annals of Mathematics 105.
Girard, J.Y., 1972, “Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur”, Ph.D. thesis, University of Paris, VII.
Goad, C., 1980, “Computational uses of the manipulation of form al proofs”, Ph.D. thesis, Stanford University.
Gordon, M.J., Milner, R., and Wadsworth, C.P., 1979, “Edinburgh LCF”, Springer Lecture Notes in Computer Science, Springer-Verlag 78.
Goto, S., 1975, Recursive Realizability and Automatic Program Synthesis (in Japanese), IECE (The Institute of Electrical and Communication Engineers, Japan), Shingaku-Giho AL (Automata and Language) AL-75–54.
Goto, S., 1977, Foundations of Automatic Program Synthesis: an Application of Godel’s Interpretation (in Japanese), Shingaku-Gino AL (Automata and Language) AL-77–16, English version appeared in: Springer Lecture Note in Computer Science 75 (1979).
Goto, S., 1979, Program synthesis from natural deduction proofs, in: “Proceedings of the Sixth International Joint Conference on Artificial Intelligence, vol. 1.”
Griffin, T.G., 1987, An environment for formal systems, Technical Report 87–846, Department of Computer Science, Cornell University.
Harper, R., Honsell, F., and Plotkin, G., 1987, A Framework for Defining Logics, in: “Second Annual Symposium on Logic in Computer Science,” IEEE.
Hayashi, S., 1987, PX: a system extracting programs from proofs, in “Formal Description of Programming Concepts-III,” Wirsing, M., ed., North-Holland, Amsterdam.
Hayashi, S., and Nakano, H., 1988, PX: A Computational Logic, The MIT Press, Cambridge, Massachusetts.
Heyting, A., 1971, Intuitionism, An Introduction, third revised edition, North-Holland, Amsterdam.
Howard, W., 1980, The formulas-as-types notion of construction, in: “Essays on Combinatory Logic, Lambda Calculus and Formalism,” Seldin, J.P. and Hindley, J.R., eds., Academic Press, New York.
Howe, D.J.., 1987, The Computational Behaviour of Girard’s Paradox, in: “Second Annual Symposium on Logic in Computer Science,” IEEE.
Hyland, J.M.E., 1987, A small complete category, preprint.
Longo, J., and Moggi, E., 1988+α, Constructive Natural Deduction and its “modest” Lrterpretation, in: “Semantics of Natural and Computer Languages,” Meseguer et al. eds., The MIT Press, Cambridge, Massachusetts.
Luo, Z., 1988, A Higher-order Calculus and Theory Abstraction, LFCS Report ECS-LFCS-88–57, LFCS, Edinburgh University.
Luo, Z., 1988a, CCω and its Meta Theory, LFCS Report ECS-LFCS-88–58, LFCS, Edinburgh University.
Manna, Z., and Waldinger, R., 1971, Towards automatic program synthesis, Communications of ACM 14.
Martin-Löf, P., 1974, An intuitionistic theory of types: Predicative Part, in: “Logic Colloquium 73,” Rose, H., and Shepherdson, J., eds., North-Holland, Amsterdam.
Martin-Löf, P., 1982, Constructive mathematics and computer programming, in: “Logic, Methodology, and Philosophy of Science VI,” Cohen, L.J., et al., eds., North-Holland, Amsterdam.
Mitchell, J.C., 1986, A type-inference approach to reduction properties and semantics of polymorphic expressions, in: “1986 ACM Symposium on Lisp and Functional Programming.”
Moggi, E., 1988, “The Partial Lambda-Calculus,” Ph.D. thesis, University of Edinburgh.
Myhill, J., 1975, Constructive set theory, J. Symbolic Logic 40.
Nepeĭvoda, N.N., 1978, A relation between the natural deduction rules and operators of higher level algorithmic languages, Soviet Mathematics Doklady 19.
Nordström, B., and Petersson, K., 1983, Types and specifications, in: Proceedings IFIP ’83, Elsevier, Amsterdam.
Nordström, Petersson, and Smith, 1988+α, Programming in Martin-Löf’s type theory. An introduction, out-coming from Oxford University Press.
Paulson, L.C., 1987, The representation of logics in higher-order logic, Cambridge Technical Report 113.
Paulin-Mohring, C., 1986, Algorithm development in the calculus of constructions, in: “First Annual Symposium on Logic in Computer Science,” IEEE.
Paulin-Mohring, C., 1987, Extraction de programmes dans le Calcul des Constructions, preprint.
Reynolds, J.C., 1974, Towards a theory of type structure, in: Springer Lecture Note in Computer Science 19.
Salvesen, A. and Smith, J.M., 1988, The strength of the subset type in Martin-LöPs type theroy, in: “Third Annual Symposium on Logic in Computer Science,” IEEE.
Sato, M., 1979, Towards a mathematical theory of program synthesis, in: ‘Proceedings of the Sixth International Joint Conference on Artificial Intelligence, vol. 2.“
Sato, M., 1985, Typed Logical Calculus, Department of Information Science, Faculty of Science, University of Tokyo, Technical Report 85–13.
Scott, D., 1970, Constructive validity, in: Springer Lecture Notes in Computer Science 125, Springer, Berlin.
Takayama, Y., 1987, Writing Programs as QJ-Proofs and Compiling into PROLOG Programs, in: “Proceedings of 4th Symposium on Logic Programming.”
Takayama, Y., 1988, Proof Theoretic Approach to the Extraction of Redundancy-free Realizer Codes, preprint.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1990 Plenum Press, New York
About this chapter
Cite this chapter
Hayashi, S. (1990). Constructive Mathematics and Computer-Assisted Reasoning Systems. In: Petkov, P.P. (eds) Mathematical Logic. Springer, Boston, MA. https://doi.org/10.1007/978-1-4613-0609-2_4
Download citation
DOI: https://doi.org/10.1007/978-1-4613-0609-2_4
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4612-7890-0
Online ISBN: 978-1-4613-0609-2
eBook Packages: Springer Book Archive