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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

12 Citations (Scopus)

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.

Original language	English
Title of host publication	Types for Proofs and Programs - International Workshop, TYPES 1998, Selected Papers
Editors	Thorsten Altenkirch, Bernhard Reus, Wolfgang Naraschewski
Publisher	Springer Verlag
Pages	78-92
Number of pages	15
ISBN (Print)	3540665374, 9783540665373
DOIs	https://doi.org/10.1007/3-540-48167-2_6
Publication status	Published - 1 Jan 1999
Externally published	Yes
Event	2nd International Workshop on Types for Proofs and Programs, TYPES 1998 - Kloster Irsee, Germany Duration: 27 Mar 1998 → 31 Mar 1998

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	1657
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	2nd International Workshop on Types for Proofs and Programs, TYPES 1998
Country/Territory	Germany
City	Kloster Irsee
Period	27/03/98 → 31/03/98

Access to Document

10.1007/3-540-48167-2_6

Cite this

Filliâtre, J. C. (1999). Proof of imperative programs in type theory. In T. Altenkirch, B. Reus, & W. Naraschewski (Eds.), Types for Proofs and Programs - International Workshop, TYPES 1998, Selected Papers (pp. 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. editor / Thorsten Altenkirch ; Bernhard Reus ; Wolfgang Naraschewski. Springer Verlag, 1999. pp. 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. in 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, pp. 78-92, 2nd International Workshop on Types for Proofs and Programs, TYPES 1998, Kloster Irsee, Germany, 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).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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. In Altenkirch T, Reus B, Naraschewski W, editors, 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

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this