scientific article; zbMATH DE number 7407781

MaRDI QIDQ5155670zbMATH OpenFDO

Authors Dan Frumin, Robbert Krebbers, Lars Birkedal

Publication date 8 October 2021

Full work available at URL https://arxiv.org/abs/2006.13635, https://lmcs.episciences.org/7708

zbMATH Keywords

concurrencyCoqIrisprogram refinementseparation logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• ReLoC: a mechanised relational logic for fine-grained concurrency
• Logical relations for fine-grained concurrency
• Relation-based semantics for concurrency
• Rewriting logic as a semantic framework for concurrency: a progress report
• A machine-checked framework for relational separation logic
• Unifying concurrent and relational refinement
• More relational concurrent refinement: traces and partial relations
• Revisiting concurrent separation logic
• Relational concurrent refinement. III: Traces, partial relations and automata
• Relational concurrent refinement: automata

Cites work

• A bisimulation for type abstraction and recursion
• A completeness theorem for Kleene algebras and the algebra of regular events
• A concurrent logical relation
• A higher-order logic for concurrent termination-preserving refinement
• A Kripke logical relation between ML and assembly
• A perspective on specifying and verifying concurrent modules
• A Powerdomain Construction
• A relational modal logic for higher-order stateful ADTs
• A relational model of types-and-effects in higher-order concurrent separation logic
• A scalable lock-free stack algorithm
• A semantics for concurrent separation logic
• A very modal model of a modern, major, general type system
• Abstraction for concurrent objects
• Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
• Behavioural equivalence via modalities for algebraic effects
• BI as an assertion language for mutable data structures
• Bisimilarity as a theory of functional programming
• Concurrent Kleene algebra and its foundations
• Cumulative inductive types in Coq
• Expressive modular fine-grained concurrency specification
• Formal certification of code-based cryptographic proofs
• Higher-order ghost state
• scientific article; zbMATH DE number 3485174 (Why is no real title available?)
• scientific article; zbMATH DE number 512792 (Why is no real title available?)
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• scientific article; zbMATH DE number 2090728 (Why is no real title available?)
• Impredicative concurrent abstract predicates
• Interactive proofs in higher-order concurrent separation logic
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Local reasoning for global invariants. I: Region logic
• Modular reasoning about separation of concurrent data structures
• Non-parametric parametricity
• Operational reasoning for functions with local state
• Practical foundations for programming languages
• Probabilistic relational reasoning for differential privacy
• Programming Languages and Systems
• Proving linearizability using partial orders
• Relational logic with framing and hypotheses
• Relational separation logic
• ReLoC: a mechanised relational logic for fine-grained concurrency
• Shape-Value Abstraction for Verifying Linearizability
• Simple relational correctness proofs for static analyses and program transformations
• Small bisimulations for reasoning about higher-order imperative programs
• State-dependent representation independence
• Step-indexed relational reasoning for countable nondeterminism
• The existence of refinement mappings
• The impact of higher-order state and control effects on local relational reasoning
• The revised report on the syntactic theories of sequential control and state
• Typed closure conversion preserves observational equivalence
• Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency
• Verifying opacity of a transactional mutex lock

Cited in

(1)

• A logical approach to type soundness

Describes a project that uses

Uses Software

• Coq
• Line-up
• RustBelt

This page was built for publication:

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