ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages

DOI10.1007/978-3-319-22102-1_25zbMath1465.68038OpenAlexW2292986447MaRDI QIDQ2945650

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

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

Related Items (6)

Lewis meets Brouwer: constructive strict implication ⋮ \textsf{LOGIC}: a Coq library for logics ⋮ Theoretical and practical approaches to the denotational semantics for MDESL based on UTP ⋮ An algebraic glimpse at bunched implications and separation logic ⋮ The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types ⋮ ModuRes

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