ModuRes: a Coq library for modular reasoning about concurrent higher-order imperative programming languages

DOI10.1007/978-3-319-22102-1_25MaRDI QIDQ2945650zbMATH OpenOpenAlexFDO

Authors Filip Sieczkowski, Aleš Bizjak, Lars Birkedal

Publication date 14 September 2015

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-22102-1_25

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Semantics in the theory of computing (68Q55) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Multimodal Separation Logic for Reasoning About Operational Semantics
• Some Domain Theory and Denotational Semantics in Coq
• Proof Abstraction for Imperative Languages
• A Coq library for verification of concurrent programs
• Formalized, effective domain theory in Coq

Cited in

(8)

• The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
• Lewis meets Brouwer: constructive strict implication
• An algebraic glimpse at bunched implications and separation logic
• scientific article; zbMATH DE number 7407797 (Why is no real title available?)
• Towards imperative modules: reasoning about invariants and sharing of mutable state
• ModuRes
• \textsf{LOGIC}: a Coq library for logics
• Theoretical and practical approaches to the denotational semantics for MDESL based on UTP

Describes a project that uses

Uses Software

• Coq
• Mechanized Semantic Library
• Rtac

This page was built for publication: ModuRes: a Coq library for modular reasoning about concurrent higher-order imperative programming languages

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2945650)