Aarhus University Seal / Aarhus Universitets segl

Ynot: Depent Types for Imperative Programs

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

Standard

Ynot: Depent Types for Imperative Programs. / Nanevski, Aleksandar; Morrisett, Greg; Shinnar, Avi; Govereau, Paul; Birkedal, Lars.

International Conference on Functional Programming: Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming,. Vol. session 9 Association for Computing Machinery, 2008. p. 229-240.

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

Harvard

Nanevski, A, Morrisett, G, Shinnar, A, Govereau, P & Birkedal, L 2008, Ynot: Depent Types for Imperative Programs. in International Conference on Functional Programming: Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming,. vol. session 9, Association for Computing Machinery, pp. 229-240.

APA

Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., & Birkedal, L. (2008). Ynot: Depent Types for Imperative Programs. In International Conference on Functional Programming: Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming, (Vol. session 9, pp. 229-240). Association for Computing Machinery.

CBE

Nanevski A, Morrisett G, Shinnar A, Govereau P, Birkedal L. 2008. Ynot: Depent Types for Imperative Programs. In International Conference on Functional Programming: Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming,. Association for Computing Machinery. pp. 229-240.

MLA

Nanevski, Aleksandar et al. "Ynot: Depent Types for Imperative Programs". International Conference on Functional Programming: Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming,. Association for Computing Machinery. 2008, 229-240.

Vancouver

Nanevski A, Morrisett G, Shinnar A, Govereau P, Birkedal L. Ynot: Depent Types for Imperative Programs. In International Conference on Functional Programming: Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming,. Vol. session 9. Association for Computing Machinery. 2008. p. 229-240

Author

Nanevski, Aleksandar ; Morrisett, Greg ; Shinnar, Avi ; Govereau, Paul ; Birkedal, Lars. / Ynot: Depent Types for Imperative Programs. International Conference on Functional Programming: Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming,. Vol. session 9 Association for Computing Machinery, 2008. pp. 229-240

Bibtex

@inproceedings{bcf2ed9ba3d6448eafd5bd95d9802abc,
title = "Ynot: Depent Types for Imperative Programs",
abstract = "We describe an axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher-order, dependently-typed programs with side-effects. Coq already includes a powerful functional language that supports dependent types, but that language is limited to pure, total functions. The key contribution of our extension, which we call Ynot, is the added support for computations that may have effects such as non-termination, accessing a mutable store, and throwing/catching exceptions.The axioms of Ynot form a small trusted computing base which has been formally justified in our previous work on Hoare Type Theory (HTT). We show how these axioms can be combined with the powerful type and abstraction mechanisms of Coq to build higher-level reasoning mechanisms which in turn can be used to build realistic, verified software components. To substantiate this claim, we describe here a representative series of modules thatimplement imperative finite maps, including support for a higherorder (effectful) iterator. The implementations range from simple (e.g., association lists) to complex (e.g., hash tables) but share a common interface which abstracts the implementation details and ensures that the modules properly implement the finite map abstraction.",
author = "Aleksandar Nanevski and Greg Morrisett and Avi Shinnar and Paul Govereau and Lars Birkedal",
year = "2008",
language = "English",
isbn = "978-1-59593-919-7",
volume = "session 9",
pages = "229--240",
booktitle = "International Conference on Functional Programming",
publisher = "Association for Computing Machinery",
address = "United States",

}

RIS

TY - GEN

T1 - Ynot: Depent Types for Imperative Programs

AU - Nanevski, Aleksandar

AU - Morrisett, Greg

AU - Shinnar, Avi

AU - Govereau, Paul

AU - Birkedal, Lars

PY - 2008

Y1 - 2008

N2 - We describe an axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher-order, dependently-typed programs with side-effects. Coq already includes a powerful functional language that supports dependent types, but that language is limited to pure, total functions. The key contribution of our extension, which we call Ynot, is the added support for computations that may have effects such as non-termination, accessing a mutable store, and throwing/catching exceptions.The axioms of Ynot form a small trusted computing base which has been formally justified in our previous work on Hoare Type Theory (HTT). We show how these axioms can be combined with the powerful type and abstraction mechanisms of Coq to build higher-level reasoning mechanisms which in turn can be used to build realistic, verified software components. To substantiate this claim, we describe here a representative series of modules thatimplement imperative finite maps, including support for a higherorder (effectful) iterator. The implementations range from simple (e.g., association lists) to complex (e.g., hash tables) but share a common interface which abstracts the implementation details and ensures that the modules properly implement the finite map abstraction.

AB - We describe an axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher-order, dependently-typed programs with side-effects. Coq already includes a powerful functional language that supports dependent types, but that language is limited to pure, total functions. The key contribution of our extension, which we call Ynot, is the added support for computations that may have effects such as non-termination, accessing a mutable store, and throwing/catching exceptions.The axioms of Ynot form a small trusted computing base which has been formally justified in our previous work on Hoare Type Theory (HTT). We show how these axioms can be combined with the powerful type and abstraction mechanisms of Coq to build higher-level reasoning mechanisms which in turn can be used to build realistic, verified software components. To substantiate this claim, we describe here a representative series of modules thatimplement imperative finite maps, including support for a higherorder (effectful) iterator. The implementations range from simple (e.g., association lists) to complex (e.g., hash tables) but share a common interface which abstracts the implementation details and ensures that the modules properly implement the finite map abstraction.

M3 - Article in proceedings

SN - 978-1-59593-919-7

VL - session 9

SP - 229

EP - 240

BT - International Conference on Functional Programming

PB - Association for Computing Machinery

ER -