Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
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⟩



Record views


Files downloads