Proof of Imperative Programs in Type Theory.
Résumé
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.
Les preuves de correction de programmes impératifs sont traditionnellement faites dans des théories du premier ordre dérivées de la logique de Hoare~\cite{Hoare69}. D'un autre côté, les preuves de correction de programmes purement fonctionnels sont le plus souvent faites dans des formalismes d'ordre supérieur. En particulier, la réalisabilité~\cite{Kleene52} permet d'extraire des programmes fonctionnels corrects à partir de preuves constructives de formules existentielles. Dans ce papier, nous établissons une relation entre ces deux approches et montrons comment les preuves en logique de Hoare peuvent être interprétées en théories des types, conduisant à une traduction fonctionnelle des programmes impératifs. Partant de cette idée, nous proposons une interprétation des formules de correction en théorie des types pour un langage de programmation mélangeant des traits impératifs et fonctionnels. Une conséquence de cette interprétation est une solution simple et naturelle aux problèmes des procédures et des effets de bord dans les expressions.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...