scientific article; zbMATH DE number 7407781
From MaRDI portal
Publication:5155670
Robbert Krebbers, Dan Frumin, Lars Birkedal
Publication date: 8 October 2021
Full work available at URL: https://arxiv.org/abs/2006.13635
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Concurrent Kleene algebra and its foundations
- Abstraction for concurrent objects
- A scalable lock-free stack algorithm
- The existence of refinement mappings
- A semantics for concurrent separation logic
- Relational separation logic
- The revised report on the syntactic theories of sequential control and state
- A completeness theorem for Kleene algebras and the algebra of regular events
- Bisimilarity as a theory of functional programming
- A perspective on specifying and verifying concurrent modules
- Behavioural equivalence via modalities for algebraic effects
- Practical Foundations for Programming Languages
- Step-Indexed Relational Reasoning for Countable Nondeterminism
- Probabilistic relational reasoning for differential privacy
- Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
- Higher-order ghost state
- Proving Linearizability Using Partial Orders
- A Higher-Order Logic for Concurrent Termination-Preserving Refinement
- The impact of higher-order state and control effects on local relational reasoning
- A very modal model of a modern, major, general type system
- Simple relational correctness proofs for static analyses and program transformations
- A bisimulation for type abstraction and recursion
- Shape-Value Abstraction for Verifying Linearizability
- A Powerdomain Construction
- Iris from the ground up: A modular foundation for higher-order concurrent separation logic
- Non-parametric parametricity
- Cumulative Inductive Types in Coq
- ReLoC
- Typed closure conversion preserves observational equivalence
- BI as an assertion language for mutable data structures
- Verifying Opacity of a Transactional Mutex Lock
- Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency
- A relational modal logic for higher-order stateful ADTs
- Formal certification of code-based cryptographic proofs
- State-dependent representation independence
- Modular Reasoning about Separation of Concurrent Data Structures
- Small bisimulations for reasoning about higher-order imperative programs
- Interactive proofs in higher-order concurrent separation logic
- A relational model of types-and-effects in higher-order concurrent separation logic
- Local Reasoning for Global Invariants, Part I
- A kripke logical relation between ML and assembly
- Expressive modular fine-grained concurrency specification
- Impredicative Concurrent Abstract Predicates
- Programming Languages and Systems
