Extensions of Structural Synthesis of Programs

Tarmo Uustalu

In 6th NWPT, pages 415-427

Abstract:

Structural synthesis of programs (SSP) is an approach to deductive synthesis of functional programs using types as specifications and based on the Curry-Howard correspondence and on an intensional treatment of the notion of type. The implemented programming environments employing SSP have been based on a fragment of intuitionistic propositional logic (simple type theory) and on a natural-deduction proof system. In the paper, we indicate that the proof search strategy used in these systems is applicable to a variety of natural-deduction proof systems (not necessarily of intuitionistic or propositional logics), and that the object-oriented user front-end specification language of the NUT programming environment can, in fact, be given a useful logical semantics in terms of intuitionistic first-order logic.

Comments
Dept of Teleinformatics, The Royal Inst of Technology, Electrum 204, S-164 40 Kista (Stockholm), Sweden.

Available as PostScript, DVI.

BRICS WWW home page