Towards the theory of programming in constructive logic

  • A. A. Voronkov
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 432)


We develop an approach to the theory of extracting programs from proofs based on constructive semantics of the first order formulas called constructive truth. The underlying ideas are discussed. Using this notion of truth we define an appropriate notion of constructive calculus. Some results on relations between our theory and well known notions of constructive logic and the theory of enumerated models are proved.


Predicate Calculus Proof Theory Constructive Proof Abstract Data Type Program Synthesis 
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.


  1. Basin D.A. [1989]. Building theories in Nuprl. — In: Logic at Botic'89, LNCS 363, 1989, 12–25.Google Scholar
  2. Bates J.L., Constable R.L. [1985] Proofs as programs. — ACM Trans. on Programming languages and systems, 1985, v.7, no.1, p.113–136.CrossRefGoogle Scholar
  3. Beeson M. J. [1978a] Some relations between classical and constructive mathematics. — J. Symb. Logic, 1978, v.43, no.2, p.228–246.Google Scholar
  4. Beeson M.J. [1986] Proving programs and programming proofs. — In: VII Int. Congress on Logic, Methodology and Philosophy of Science, Elsevier Sci. Publishers, 1986, p.51–82.Google Scholar
  5. Bertoni A., Mauri G., Miglioli P., Ornaghi M. [1984] Abstract data types and their extension within a constructive logic. — Semantics of Data Types, LNCS 173, 1984, 177–195.Google Scholar
  6. Bishop E. [1970] Mathematics as a numerical language. In: Intuitionism and Proof Theory, North Holland, 1970, p.53–71.Google Scholar
  7. Bresciani P., Miglioli P., Moscato U., Ornaghi M. [1986] PAP — proofs as programs (Abstract). — JSL 51(3), 1986, 852–853.Google Scholar
  8. Chisholm P. [1987] Derivation of a parsing algorithm in Martin-Lof's theory of types. — Science of Computer Programming, 1987, v.8, no.1, p.1–42.CrossRefGoogle Scholar
  9. Constable R.L. [1972] Constructive mathematics and automatic program writers. — In: IFIP'71, North Holland, 1972, p.229–233.Google Scholar
  10. Constable R.L. [1983] Programs as proofs: a synopsis. — Information Processing Letters, 1983, v.16, no.3, p.105–112.CrossRefGoogle Scholar
  11. Constable R.L. e.a. [1986] Implementing mathematics with the Nuprl proof development system. — Prentice Hall, 1986.Google Scholar
  12. Coquand T., Huet G. [1988] The calculus of constructions. — Information and computation, 1988, v.74, no.213, p.95–120.CrossRefGoogle Scholar
  13. Dragalin A.G. [1967] To the basing of Markov's principle. — Soviet Mathematical Doklady, 1967, v.177.Google Scholar
  14. Dragalin A.G. [1978] Mathematical intuitionism. Introduction to the proof theory (Russian). — Moscow, Nauka, 1978.Google Scholar
  15. de Bruin N.G. [1980] A survey of the project AUTOMATH. — In: To H.B.Curry; Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, 1980, p.579–606.Google Scholar
  16. Diller J. [1980] Modified realization and the formulae-as-types notion. In: Festschrift on the occasion of H.B.Curry's 80th Birthday, Academic Press, N.Y., 1980, p.491–502.Google Scholar
  17. Ershov Yu.L. [1973] The theory of A-spaces. — Algebra i Logica, 12(4), 1973.Google Scholar
  18. Ershov Yu.L. [1977] The theory of enumerations (in Russian). — Moscow, Nauka, 1977.Google Scholar
  19. Ershov Yu.L. [1980] Decidability problems and constructive models (in Russian). — Moscow, Nauka, 1980.Google Scholar
  20. Feferman S. [1979] Constructive theories of functions and classes. — In: Logic Colloquium'78, North Holland, 1979, p.159–224.Google Scholar
  21. Feferman S. [1984] Between constructive and classical mathematics. — In: Computation and proof theory, Lecture Notes in Math 1104, 1984, p.143–162.Google Scholar
  22. Goad C.A. [1980a] Proofs as descriptions of computation. — 5th CADE, LNCS 87, 1980, p.39–52.Google Scholar
  23. Goad C.A. [1980b] Computational uses of the manipulation of formal proofs. — Stanford Univ. Department of CS, TR no. STAN-CS-80-819, 1980, 122p.Google Scholar
  24. Gödel K. [1958] Uber eine noch nicht benutzte Erweiterung des finiten Standpunktes. — Dialectica, 1958, v.12, no. 3/4, p.280–287.Google Scholar
  25. Goto S. [1979b] Program synthesis from natural deduction proofs. — 6th IJCAI, 1979, v.1, p.339–341.Google Scholar
  26. Harrop R. [1960] Concerning formulas of the types A→ BB V C, A → (Ex)B(x) in intuitionistic formal system. — J. Symb. Logic, v.17, 1960, pp.27–32.Google Scholar
  27. Hayashi S., Nakano H. [1988] PX: a computational logic. — MIT Press, 1988.Google Scholar
  28. Henson M.C. [1989a] Information loss in the programming logic TK. — Draft, Univ. of Essex, Department of Computer Sci., October, 1989.Google Scholar
  29. Henson M.C. [1989b] Realizability models for program construction. — In: J.L.A. van de Snepsheut (Ed.), Mathematics of Program Construction, LNCS 375, 1989, 256–272.Google Scholar
  30. Huet D. [1986] Computation and deduction. — Carnegie Mellon Univ., 1986.Google Scholar
  31. Kleene S.C. [1952] Introduction to metamathematics. — Van Nostrand P.C., Amsterdam, 1952.Google Scholar
  32. Kleene S.C. [1973] Realizability: a retrospective survey. — LNM 337, 1973.Google Scholar
  33. Kolmogorov A.N. [1932] Zur Deutung der Intuitionistischen Logik. — Mathematische Zeitschrift, v.35, 1932, p.58–65.CrossRefGoogle Scholar
  34. Kreisel G. [1958] Interpretation of analysis by means of constructive functionals of finite types. — In: Constructivity in Mathematics, North Holland, 1958, p.101–128.Google Scholar
  35. Läuchly H. [1970] An abstract notion of realizability for which intuitionistic predicate calculus is complete. — In: Intuitionism and Proof Theory, North Holland, 1970, p.227–234.Google Scholar
  36. Manna Z., Waldinger R. [1979] Synthesis: dreams → programs. — IEEE Trans. Software Engineering, 1979, v.5, no.4, p. 294–328.Google Scholar
  37. Markov A.A., Nagorny N.M. [1986] Theory of algorithms. — Moscow, Nauka, 1986.Google Scholar
  38. Miglioli P., Moscato U., Ornaghi M. [1989] Semi-constructive formal systems and axiomatization of abstract data types. — TAPSOFT'89, LNCS 351, 337–351.Google Scholar
  39. Mints G.E. [1974] E-theorems (in Russian). — Zapiski Nauchnyh seminarov LOMI, 1974, v.40, p.110–118.Google Scholar
  40. Nelson D. [1947] Recursive functionals and intuitionistic number theory. — Trans. Amer. Math. Soc., v.61, 1947, p.307–368.Google Scholar
  41. Nepeivoda N.N. [1979a] An application of proof theory to the problem of con structing correct programs. — Kibernetika, 1979, no.2.Google Scholar
  42. Nepeivoda N.N. [1979b] A method of constructing correct programs from correct subprograms. — Programmirovanie, 1979, no.1.Google Scholar
  43. Nepeivoda N.N., Sviridenko D.I. [1982] Towards the theory of program synthesis (in Russian). — In: Trudy Instituta Matematiki, v.2, Novosibirsk, Nauka, 1982, p.159–175.Google Scholar
  44. Nordstrom B., Peterson K. [1983] Types and specifications. — IFIP'83, NH, 1983, 915–920.Google Scholar
  45. Nordstrom B., Smith J.M. [1984] Propositions, types and specifications of programs in Martin-Lof's type theory. — BIT, 24(3), 1984, 288–301.Google Scholar
  46. Plisko V.E. [1987] On languages with constructive logical connectives. — Soviet Mathematical Doklady, v.296, no. 1., 1987.Google Scholar
  47. Prank R.K. [1981] Expressibility in elementary theory or recursively enumerable sets with realizability logic. — Algebra i Logica, 20(4), 1981.Google Scholar
  48. Prawitz D. Natural deduction. — Stockholm, Almquist and Wicksell, 1965.Google Scholar
  49. Petersson K. [1982] A programming system for type theory. — LPM Memo 21, Dpt of CS, Chalmers Univ. of Technology, Goteborg, 1982.Google Scholar
  50. Scott D.S. [1982] Domains for denotational semantics. In: Lecture Notes in Computer Science 140, 1982, pp.577–612.Google Scholar
  51. Starchenko S.S., Voronkov A.A. [1988] On connections between classical and constructive semantics. — In: COLOG-88 (papers presented at the Int. Conf. on Computer Logic), Part 1, Tallinn, 1988, p.101–112.Google Scholar
  52. Voronkov A.A. [1985] A generalization of the notion of realizability. — Unpublished Manuscript, 25pp. (Abstract was published in Siberian Mathematical Journal, 1986).Google Scholar
  53. Voronkov A.A. [1986a] Logic programs and their synthesis (Russian). Preprint no. 23, Institute of Mathematics, Novosibirsk, 1986.Google Scholar
  54. Voronkov A.A. [1986b] Synthesis of logic programs (Russian). Preprint no. 24, Institute of Mathematics, Novosibirsk, 1986.Google Scholar
  55. Voronkov A.A. [1986c] Intuitionistic list theory (Russian). — In: Abstracts of the 8th All-union Conf. on Mathematical Logic, Moscow, 1986.Google Scholar
  56. Voronkov A.A. [1987a] Constructive logic: a semantic approach. — In: Abstracts of the 8th Int. Congress on Logic, Methodology and Philosophy of Sci., v.5, part 1, Moscow, Nauka, 1987, p.79–82.Google Scholar
  57. Voronkov A.A. [1987b] Deductive program synthesis and Markov's principle. — In: Fundamentals of computation theory, LNCS v.278, 1987, p.479–482.Google Scholar
  58. Voronkov A.A. [1988a] Constructive calculi and constructive models. — Soviet Mathematical Doklady, 299 (1), 1988.Google Scholar
  59. Voronkov A.A. [1988b] Model theory based on the constructive notion of truth. — In: Model Theory and Applications, Trudy Instituta Matematiki, v.8, Novosibirsk, 1988.Google Scholar
  60. Voronkov A.A. [1989a] Program synthesis using proofs in first order logic. (Russian). — To be published in Vychislitelnye sistemy, 1989, 50pp.Google Scholar
  61. Voronkov A.A. [1989b] A theory for programming in constructive logic. — presented to the 3rd Int. Conf. on Computer Sci. Logic, Kaiserslautern, October, 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1990

Authors and Affiliations

  • A. A. Voronkov
    • 1
  1. 1.Institute of MathematicsUniversitetski Prospect 4Novosibirsk 90USSR

Personalised recommendations