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].


Fami Prova 


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.MATHGoogle 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