##
**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.

### 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 |