Constructive Theories with Abstract Data Types for Program Synthesis

  • Pierangelo Miglioli
  • Ugo Moscato
  • Mario Ornaghi


The research explained in this paper originates from program synthesis in the frame of intuitionistic logic [6] and has been furtherly developed as a study involving, on the one hand, constructive proofs as programs [12], on the other hand the possibility of providing axiomatizations of mathematical structures (abstract data types) compatible with constructive logical principles [3].


Atomic Formula Intuitionistic Logic Constructive Theory Induction Principle Abstract Data Type 
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. [1]
    Bates J., Constable R. — Proofs as programs — ACM Transactions on Programming Languages and Systems, Vol. 7, n.1, 1985.Google Scholar
  2. [2]
    Bertoni A., Mauri G., Miglioli P. — On the power of model theory to specify abstract data types and to capture their recursiveness — Fundamenta Informaticae IV.2, 1983.Google Scholar
  3. [3]
    Bertoni A., Mauri G., Miglioli P., Ornaghi M. — Abstract data types and their extension within a constructive logic — Lect. Notes in Comp. Sci., n.173, Springer, 1984.Google Scholar
  4. [4]
    Bresciani P., Miglioli P., Moscato U., Ornaghi M. — PaP: Proofs as Programs — abstract presented at the ASL meeting, Stanford University,July 15–19, 1985.To appear in JSL.Google Scholar
  5. [5]
    Chang C., Keisler H. — Model theory — North Holland, 1973.zbMATHGoogle Scholar
  6. [6]
    Degli Antoni G., Miglioli P., Ornaghi M. — Top-down approach to the synthesis of programs — Proc. Collo. sur la Programmation, Paris 1974, Lect. Notes in Comp. Sci. n. 19, Springer, 1974.Google Scholar
  7. [7]
    Goad C. — Computational uses of the manipulation of formal proofs — Rep. STAN-CS-80-819,Stanford University, 1980.Google Scholar
  8. [8]
    Goguen J.A., Thatcher J.W., Wagner E.G. — An initial algebra approach to the specification, correctness and implementation of abstract data types — IBM Res. Rep. RC6487, Yorktown Heights, 1976.Google Scholar
  9. [9]
    Manna Z. — Mathematical theory of computation — Mc Grow Hill, 1973.Google Scholar
  10. [10]
    Martin-Lof P. — Constructive Mathematics and Computer Programming — Presented at the 6-th Congress for Logic, Methodology and Philosophy of Sciences, Hannover, 1979.Google Scholar
  11. [11]
    Medvedev T. — Finite problems — Sov.Math.Dok. vol.3,1962.Google Scholar
  12. [12]
    Miglioli P., Ornaghi M. — A logically justified model of computation I,II — Fundamenta Informaticae IV.1,2, 1981.Google Scholar
  13. [13]
    Miglioli P., Moscato U., Ornaghi M. — Constructive theories with superintuitionistic deductive systems: some results and techniques — Internal report, 1986.Google Scholar
  14. [14]
    Troelstra A.S. — Metamathematical investigation of Intuitionistic Arithmetic and Analysis — Lect. Notes in Math., n.344. Springer, 1973.CrossRefGoogle Scholar

Copyright information

© Plenum Press, New York 1987

Authors and Affiliations

  • Pierangelo Miglioli
    • 1
  • Ugo Moscato
    • 1
  • Mario Ornaghi
    • 1
  1. 1.Dept. of Information ScienceUniversity of MilanMilanItaly

Personalised recommendations