Semi-constructive formal systems and axiomatization of abstract data types

1. Bates J., Constable R. — Proofs as programs — ACM Transaction on Programming Languages and Systems, vol. 7, n.1, 1985.

   Google Scholar 

2. Bertoni A., Mauri G., Miglioli P., Wirsing M. — On different approaches to abstract data types and the existence of recursive models — EATCS bulletin vol. 9, oct. 1979.

   Google Scholar 

3. 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, pp. 127–170.

   Google Scholar 

4. Bertoni A., Mauri G., Miglioli P., Ornaghi M. — Abstract data types and their extension within a constructive logic — Semantics of data types (Valbonne, 1984), Lecture Notes in Computer Science, vol. 173, Springer-Verlag, Berlin, 1984, pp. 177–195.

   Google Scholar 

5. Bresciani P., Miglioli P., Moscato U., Ornaghi M. — PAP: Proofs as Programs — (abstract), JSL, Vol. 51, n.3, 1986, pp. 852–853.

   Google Scholar 

6. Broy M., Wirsing M. — On the algebraic extension of abstract data types — in: Diaz J., Ramos I. (ed.) — Formalization of programming concepts — Lecture Notes in Comp. Sci. vol. 107, Springer-Verlag, Berlin, 1981.

   Google Scholar 

7. Chang C.C., Keisler H.J. — Model theory — North-Holland, 1973.

   Google Scholar 

8. Girard J. — The system F of variable types 15 years later — Report of CNRS, Paris, 1985.

   Google Scholar 

9. Goad C. — Computational uses of the manipulation of formal proofs — Rep. STAN-CS-80-819, Stanford University, 1980.

   Google Scholar 

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

11. Goto S. — Program synthesis through Gödel's interpretation — Mathematical studies of information processing, (proceedings, Kyoto, 1978), Lecture Notes in Computer Science, vol.75, Springer-Verlag, Berlin, 1979, pp. 302–325.

    Google Scholar 

12. Guttag J., Horning J. — The algebraic specification of abstract data types — Acta Informatica 10, 27–52, 1978.

    Google Scholar 

13. Howard W.A. — The formulae-as-types notion of construction — in To Curry H.B.: essays on combinatory logic, lambda calculus and formalism, Academic Press, London, 1980.

    Google Scholar 

14. Kirk R.E. — A result on propositional logics having the disjunction property — Notre Dame Journal of Formal Logic, 23,1, 71–74, 1982.

    Google Scholar 

15. Kreisel G., Putnam H. — Eine unableitbarkeitsbeismethode für den intuitionistischen Aussagenkalkul — Archiv für Mathematische Logik und Grundlagenforschung, 3, 74–78, 1957.

    Google Scholar 

16. Martin-Löf P. — Constructive Mathematics and Computer Programming — Logic, Methodology and Philosophy of Science VI, L. Cohen, J. Los, H. Pfeiffer, K. Podewski (ed.), North-Holland, Amsterdam, 1982, pp.153–175.

    Google Scholar 

17. Miglioli P., Moscato U., Ornaghi M. — Constructive theories with abstract data types for program synthesis — Proceedings of the symposium Mathematical Logic and its Applications, Plenum Press, New York, 1988, pp.293–302.

    Google Scholar 

18. Miglioli P., Ornaghi M. — A logically justified model of computation I,II — Fundamenta Informaticae, IV.1,2, 1981.

    Google Scholar 

19. Nordstrom B., Smith J.M. — Propositions, Types and Specifications of Programs in Martin-Löf's Type Theory — BIT, Vol. 24, n.3 1984, pp.288–301.

    Google Scholar 

20. Troelstra A.S. — Metamathematical investigation of Intuitionistic Arithmetic and Analysis — Lecture Notes in Mathematics, vol.344, Springer-Verlag, Berlin, 1973.

    Google Scholar 

21. Troelstra A.S. — Aspects of constructive mathematics — in: Barwise J. (ed.) — Handbook of Mathematical Logic, North Holland, Amsterdam 1977.

    Google Scholar 

22. Miglioli P., Moscato U., Ornaghi M. — PAP: a logic programming system based on a constructive logic — LNCS, n.306, Springer Verlag, 1988, pp.143–156.

    Google Scholar 

Download references