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 :
Reports
Complete list of metadatas

Cited literature [16 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02102043
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:12:45 AM
Last modification on : Sunday, May 5, 2019 - 1:24:46 AM

File

RR1997-24.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02102043, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

6

Files downloads

43