Constructive theories with abstract data types for program synthesis

Pierangelo Miglioli

Ugo Moscato

Mario Ornaghi

pp. 293-302

in: Dimiter G. Skordev (ed), Mathematical logic and its applications, Berlin, Springer, 1987

Abstrakt

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