ModuRes
ModuRes: A Coq library for modular reasoning about concurrent higher-order imperative programming languages. 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.
Keywords for this software
References in zbMATH (referenced in 4 articles , 1 standard article )
Showing results 1 to 4 of 4.
Sorted by year (- Sheng, Feng; Zhu, Huibiao; He, Jifeng; Yang, Zongyuan; Bowen, Jonathan P.: Theoretical and practical approaches to the denotational semantics for MDESL based on UTP (2020)
- Litak, Tadeusz; Visser, Albert: Lewis meets Brouwer: constructive strict implication (2018)
- Clouston, Ranald; Bizjak, Aleš; Grathwohl, Hans Bugge; Birkedal, Lars: The guarded lambda-calculus: programming and reasoning with guarded recursion for coinductive types (2016)
- Sieczkowski, Filip; Bizjak, Aleš; Birkedal, Lars: ModuRes: a Coq library for modular reasoning about concurrent higher-order imperative programming languages (2015)