Krivine, Jean-Louis; Parigot, Michel Programming with proofs. (English) Zbl 0699.68020 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. Cited in 1 ReviewCited in 24 Documents 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 PDF BibTeX XML Cite \textit{J.-L. Krivine} and \textit{M. Parigot}, J. Inf. Process. Cybern. 26, No. 3, 149--167 (1990; Zbl 0699.68020)