Constructive system for automatic program synthesis

AbstractThis paper describes a constructive system, based on a particular typed λ-calculus with constants and λ-expressions as types. This theory is principally based on intuitionistic type theory on the general idea of programming proofs which means extracting programs from constructive proofs. It can be considered as a basis of a system for automatized program sythesis by developing adapted techniques of programmation. It allows to partially automate the construction of programs from different specifications by a type-driven strategy. Moreover, the corresponding logical theory appears like a good base of higher-order calculus