Programming with proofs. (English) Zbl 0699.68020

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.


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