Skip to Main content Skip to Navigation

Proof of Imperative Programs in Type Theory.

Abstract : Proofs of correctness of imperative programs are traditionally done in first order frameworks derived from Hoare logic~\cite{Hoare69}. On the other hand, correctness proofs of purely functional programs are almost always done in higher order logics. In particular, the realizability~\cite{Kleene52} allow to extract correct functional programs from constructive proofs of existential formulae. In this paper, we establish a relation between these two approaches and show how proofs in Hoare logic can be interpreted in type theory, yielding a translation of imperative programs into functional ones. Starting from this idea, we propose an interpretation of correctness formulae in type theory for a programming language mixing imperative and functional features. One consequence is a good and natural solution to the problems of procedures and side-effects in expressions.
Document type :
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download
Contributor : Colette Orange Connect in order to contact the contributor
Submitted on : Wednesday, April 17, 2019 - 9:12:45 AM
Last modification on : Saturday, September 11, 2021 - 3:19:11 AM


Files produced by the author(s)


  • HAL Id : hal-02102043, version 1



Jean-Christophe Filliatre. Proof of Imperative Programs in Type Theory.. [Research Report] LIP RR-1997-24, Laboratoire de l'informatique du parallélisme. 1997, 2+20p. ⟨hal-02102043⟩



Les métriques sont temporairement indisponibles