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
Reports

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 metadata

Cited literature [16 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02102043
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

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

24

Files downloads

336