Proof of imperative programs in type theory

Jean Christophe Filliâtre

doi:10.1007/3-540-48167-2_6

Proof of imperative programs in type theory

Jean Christophe Filliâtre

INRIA Saclay, Laboratoire de Recherche en Informatique (LRI), Université Paris Sud

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

Résumé

We present a new approach to certifying functional programs with imperative aspects, in the context of Type Theory. The key is a functional translation of imperative programs, based on a combination of the type and effect discipline and monads. Then an incomplete proof of the specification is built in the Type Theory, whose gaps would correspond to proof obligations. On sequential imperative programs, we get the same proof obligations as those given by Floyd-Hoare logic. Compared to the latter, our approach also includes functional constructions in a straight-forward way. This work has been implemented in the Coq Proof Assistant and applied on non-trivial examples.

langue originale	Anglais
titre	Types for Proofs and Programs - International Workshop, TYPES 1998, Selected Papers
rédacteurs en chef	Thorsten Altenkirch, Bernhard Reus, Wolfgang Naraschewski
Editeur	Springer Verlag
Pages	78-92
Nombre de pages	15
ISBN (imprimé)	3540665374, 9783540665373
Les DOIs	https://doi.org/10.1007/3-540-48167-2_6
état	Publié - 1 janv. 1999
Modification externe	Oui
Evénement	2nd International Workshop on Types for Proofs and Programs, TYPES 1998 - Kloster Irsee, Allemagne Durée: 27 mars 1998 → 31 mars 1998

Série de publications

Nom	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	1657
ISSN (imprimé)	0302-9743
ISSN (Electronique)	1611-3349

Une conférence

Une conférence	2nd International Workshop on Types for Proofs and Programs, TYPES 1998
Pays/Territoire	Allemagne
La ville	Kloster Irsee
période	27/03/98 → 31/03/98

Accès au document

10.1007/3-540-48167-2_6

Contient cette citation

Filliâtre, J. C. (1999). Proof of imperative programs in type theory. Dans T. Altenkirch, B. Reus, & W. Naraschewski (eds.), Types for Proofs and Programs - International Workshop, TYPES 1998, Selected Papers (p. 78-92). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 1657). Springer Verlag. https://doi.org/10.1007/3-540-48167-2_6

Filliâtre, Jean Christophe. / Proof of imperative programs in type theory. Types for Proofs and Programs - International Workshop, TYPES 1998, Selected Papers. Editeur / Thorsten Altenkirch ; Bernhard Reus ; Wolfgang Naraschewski. Springer Verlag, 1999. p. 78-92 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{926995f3e9e7466bb55a214f31d80afd,

title = "Proof of imperative programs in type theory",

abstract = "We present a new approach to certifying functional programs with imperative aspects, in the context of Type Theory. The key is a functional translation of imperative programs, based on a combination of the type and effect discipline and monads. Then an incomplete proof of the specification is built in the Type Theory, whose gaps would correspond to proof obligations. On sequential imperative programs, we get the same proof obligations as those given by Floyd-Hoare logic. Compared to the latter, our approach also includes functional constructions in a straight-forward way. This work has been implemented in the Coq Proof Assistant and applied on non-trivial examples.",

author = "Filli{\^a}tre, \{Jean Christophe\}",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1999.; 2nd International Workshop on Types for Proofs and Programs, TYPES 1998 ; Conference date: 27-03-1998 Through 31-03-1998",

year = "1999",

month = jan,

day = "1",

doi = "10.1007/3-540-48167-2\_6",

language = "English",

isbn = "3540665374",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "78--92",

editor = "Thorsten Altenkirch and Bernhard Reus and Wolfgang Naraschewski",

booktitle = "Types for Proofs and Programs - International Workshop, TYPES 1998, Selected Papers",

}

Filliâtre, JC 1999, Proof of imperative programs in type theory. Dans T Altenkirch, B Reus & W Naraschewski (eds), Types for Proofs and Programs - International Workshop, TYPES 1998, Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), VOL. 1657, Springer Verlag, p. 78-92, 2nd International Workshop on Types for Proofs and Programs, TYPES 1998, Kloster Irsee, Allemagne, 27/03/98. https://doi.org/10.1007/3-540-48167-2_6

Proof of imperative programs in type theory. / Filliâtre, Jean Christophe.
Types for Proofs and Programs - International Workshop, TYPES 1998, Selected Papers. Ed. / Thorsten Altenkirch; Bernhard Reus; Wolfgang Naraschewski. Springer Verlag, 1999. p. 78-92 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 1657).

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

TY - GEN

T1 - Proof of imperative programs in type theory

AU - Filliâtre, Jean Christophe

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 1999.

PY - 1999/1/1

Y1 - 1999/1/1

N2 - We present a new approach to certifying functional programs with imperative aspects, in the context of Type Theory. The key is a functional translation of imperative programs, based on a combination of the type and effect discipline and monads. Then an incomplete proof of the specification is built in the Type Theory, whose gaps would correspond to proof obligations. On sequential imperative programs, we get the same proof obligations as those given by Floyd-Hoare logic. Compared to the latter, our approach also includes functional constructions in a straight-forward way. This work has been implemented in the Coq Proof Assistant and applied on non-trivial examples.

AB - We present a new approach to certifying functional programs with imperative aspects, in the context of Type Theory. The key is a functional translation of imperative programs, based on a combination of the type and effect discipline and monads. Then an incomplete proof of the specification is built in the Type Theory, whose gaps would correspond to proof obligations. On sequential imperative programs, we get the same proof obligations as those given by Floyd-Hoare logic. Compared to the latter, our approach also includes functional constructions in a straight-forward way. This work has been implemented in the Coq Proof Assistant and applied on non-trivial examples.

U2 - 10.1007/3-540-48167-2_6

DO - 10.1007/3-540-48167-2_6

M3 - Conference contribution

AN - SCOPUS:84957007970

SN - 3540665374

SN - 9783540665373

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 78

EP - 92

BT - Types for Proofs and Programs - International Workshop, TYPES 1998, Selected Papers

A2 - Altenkirch, Thorsten

A2 - Reus, Bernhard

A2 - Naraschewski, Wolfgang

PB - Springer Verlag

T2 - 2nd International Workshop on Types for Proofs and Programs, TYPES 1998

Y2 - 27 March 1998 through 31 March 1998

ER -

Filliâtre JC. Proof of imperative programs in type theory. Dans Altenkirch T, Reus B, Naraschewski W, rédacteurs en chef, Types for Proofs and Programs - International Workshop, TYPES 1998, Selected Papers. Springer Verlag. 1999. p. 78-92. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-48167-2_6

Proof of imperative programs in type theory

Résumé

Série de publications

Une conférence

Accès au document

Empreinte digitale

Contient cette citation