Constructive theories with abstract data types for program synthesis
pp. 293-302
in: Dimiter G. Skordev (ed), Mathematical logic and its applications, Berlin, Springer, 1987Abstract
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].