SKIL: A system for programming with proofs. SKIL (synthesizing knowledge in intuitionistic logic) is an interactive theorem prover dedicated to program synthesis and implemented in Quintus- Prolog. The object-level logic is a second-order constructive logic denoted AF2 which includes induction through the data type definitions [{it J.-L. Krivine} and {it M. Parigot}, J. Inf. Process. Cybern. 26, No. 3, 149-167 (1990; Zbl 0699.68020)]. Since the object-level is constructive, terms of λ-calculus are constructed during the proof search. These extracted terms are programs following the programming with proofs paradigm, having the two properties of correctness and termination [loc. cit.]. That is, the system is in fact a program synthesis environment, since a specification can be regarded as a proposition and its extracted term as a program which meets this specification.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element