Search filters

List of works by Lars Birkedal

A Logical Approach to Type Soundness

scientific article published on 10 July 2024

An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic

scientific article published on 05 January 2024

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic

scientific article published on 05 January 2024

BI Hyperdoctrines and Higher-Order Separation Logic

scientific article published in 2005

BI-hyperdoctrines, higher-order separation logic, and abstraction

scientific article published in August 2007

Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code

scientific article published on 14 September 2023

Client-server sessions in linear logic

scientific article published on 19 August 2021

Distributed causal memory: modular specification and verification in higher-order distributed separation logic

scientific article published on 04 January 2021

Equilogical spaces

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs

scientific article published on 15 August 2024

Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly

scientific article published on 08 October 2024

Iris-Wasm: Robust and Modular Verification of WebAssembly Programs

scientific article published on 06 June 2023

Le temps des cerises: efficient temporal stack safety on capability machines using directed capabilities

scientific article published on 29 April 2022

Logical Step-Indexed Logical Relations

article

Logical relations for fine-grained concurrency

Logical relations for fine-grained concurrency

Melocoton: A Program Logic for Verified Interoperability Between OCaml and C

scientific article published on 16 October 2023

Modular verification of op-based CRDTs in separation logic

scientific article published on 31 October 2022

Reasoning about monotonicity in separation logic

scientific article published on 20 January 2021

Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory

scientific article published on 16 October 2023

Tachis: Higher-Order Separation Logic with Credits for Expected Costs

scientific article published on 08 October 2024

Theorems for free from separation logic specifications

scientific article published in 2021

Transfinite Iris: resolving an existential dilemma of step-indexed separation logic

scientific article published on 18 June 2021

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement

scientific article published on 05 January 2024

VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A

scientific article published on 06 June 2023

Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols

scientific article published on 31 August 2023

Views

scientific article (publication date: 23 January 2013)

Paulina is supported by:

About Paulina

Help