Abstract
It is well-known that it is challenging to build semantic models of type systems or logics for reasoning about concurrent higher-order imperative programming languages. One of the key challenges is that such semantic models often involve constructing solutions to certain kinds of recursive domain equations, which in practice has been a barrier to formalization efforts. Here we present the ModuRes Coq library, which provides an easy way to solve such equations. We show how the library can be used to construct models of type systems and logics for reasoning about concurrent higher-order imperative programming languages.
Cite
CITATION STYLE
Sieczkowski, F., Bizjak, A., & Birkedal, L. (2015). ModuRes: A Coq library for modular reasoning about concurrent higher-order imperative programming languages. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9236, pp. 375–390). Springer Verlag. https://doi.org/10.1007/978-3-319-22102-1_25
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
