Programming with proofs. (English) Zbl 0699.68020

Krivine, Jean-Louis; Parigot, Michel

J. Inf. Process. Cybern. 26, No. 3, 149-167 (1990).

Summary: The paper presents a logical framework for constructing a programming language in which one programs by proofs, in order to ensure program correctness. The general programming methodology based on second order intuitionistic logic is the following: (i) the data types are defined by second order formulas from which a representation of the data in lambda- calculus can be extracted automatically (ii) the specification of the programs are expressed by equations (iii) a correct program in lambda- calculus is automatically extracted from a proof of the fact that a function satisfying the equations has the intended type.

MSC:

68N01	General topics in the theory of software
68Q60	Specification and verification (program logics, model checking, etc.)
03F35	Second- and higher-order arithmetic and fragments

Keywords:

automatic programming; mathematics as a programming language; specifications; correct programs; second order intuitionistic