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

DOI10.1007/978-3-319-22102-1_25zbMATH Open1465.68038OpenAlexW2292986447MaRDI QIDQ2945650FDOQ2945650

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

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

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)

Cited In (8)

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

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)