Constructive Theories with Abstract Data Types for Program Synthesis
The research explained in this paper originates from program synthesis in the frame of intuitionistic logic  and has been furtherly developed as a study involving, on the one hand, constructive proofs as programs , on the other hand the possibility of providing axiomatizations of mathematical structures (abstract data types) compatible with constructive logical principles .
KeywordsAtomic Formula Intuitionistic Logic Constructive Theory Induction Principle Abstract Data Type
Unable to display preview. Download preview PDF.
- Bates J., Constable R. — Proofs as programs — ACM Transactions on Programming Languages and Systems, Vol. 7, n.1, 1985.Google Scholar
- 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
- 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
- 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
- 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
- Goad C. — Computational uses of the manipulation of formal proofs — Rep. STAN-CS-80-819,Stanford University, 1980.Google Scholar
- 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
- Manna Z. — Mathematical theory of computation — Mc Grow Hill, 1973.Google Scholar
- 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
- Medvedev T. — Finite problems — Sov.Math.Dok. vol.3,1962.Google Scholar
- Miglioli P., Ornaghi M. — A logically justified model of computation I,II — Fundamenta Informaticae IV.1,2, 1981.Google Scholar
- Miglioli P., Moscato U., Ornaghi M. — Constructive theories with superintuitionistic deductive systems: some results and techniques — Internal report, 1986.Google Scholar