The following pages link to Lars Birkedal (Q444497):
Displaying 50 items.
- Local reasoning about a copying garbage collector (Q3452262) (← links)
- Relational Parametricity and Separation Logic (Q3518282) (← links)
- A Simple Model of Separation Logic for Higher-Order Store (Q3519513) (← links)
- On the Construction of Sorted Reactive Systems (Q3541020) (← links)
- Hoare type theory, polymorphism and separation (Q3546051) (← links)
- A Semantic Foundation for Hidden State (Q3557840) (← links)
- Realisability semantics of parametric polymorphism, general references and recursive types (Q3583027) (← links)
- Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types (Q3617747) (← links)
- Nested Hoare Triples and Frame Rules for Higher-Order Store (Q3644765) (← links)
- (Q4364397) (← links)
- (Q4499148) (← links)
- (Q4499150) (← links)
- (Q4513576) (← links)
- Iris from the ground up: A modular foundation for higher-order concurrent separation logic (Q4625160) (← links)
- (Q4649541) (← links)
- A step-indexed Kripke model of hidden state (Q4911302) (← links)
- StkTokens<i>: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities</i> (Q5016212) (← links)
- Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems (Q5041100) (← links)
- Modalities and Parametric Adjoints (Q5072609) (← links)
- ReLoC (Q5145319) (← links)
- Multimodal Dependent Type Theory (Q5145658) (← links)
- (Q5155670) (← links)
- (Q5155672) (← links)
- A Model of Countable Nondeterminism in Guarded Type Theory (Q5170811) (← links)
- The impact of higher-order state and control effects on local relational reasoning (Q5176935) (← links)
- A kripke logical relation for effect-based program transformations (Q5176994) (← links)
- Ynot (Q5178765) (← links)
- Modal dependent type theory and dependent right adjoints (Q5220184) (← links)
- Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency (Q5244818) (← links)
- A relational modal logic for higher-order stateful ADTs (Q5255072) (← links)
- Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes (Q5271058) (← links)
- Guarded Cubical Type Theory: Path Equality for Guarded Recursion (Q5278409) (← links)
- Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages (Q5310672) (← links)
- Linear Abadi and Plotkin Logic (Q5310673) (← links)
- Programming Languages and Systems (Q5316567) (← links)
- Modular Reasoning about Separation of Concurrent Data Structures (Q5326285) (← links)
- Interactive proofs in higher-order concurrent separation logic (Q5370856) (← links)
- A relational model of types-and-effects in higher-order concurrent separation logic (Q5370857) (← links)
- Relational Reasoning for Recursive Types and References (Q5385588) (← links)
- Modular reasoning about concurrent higher-order imperative programs (Q5408395) (← links)
- Step-indexed kripke models over recursive worlds (Q5408537) (← links)
- Impredicative Concurrent Abstract Predicates (Q5410698) (← links)
- Higher-Order Separation Logic in Isabelle/HOLCF (Q5415649) (← links)
- A Realizability Model for Impredicative Hoare Type Theory (Q5458408) (← links)
- Category-theoretic models of linear Abadi \& Plotkin logic (Q5458501) (← links)
- Polymorphism and separation in hoare type theory (Q5501458) (← links)
- Categorical models for Abadi and Plotkin's logic for parametricity (Q5697712) (← links)
- Step-Indexed Kripke Model of Separation Logic for Storable Locks (Q5739354) (← links)
- Abstract Predicates and Mutable ADTs in Hoare Type Theory (Q5756495) (← links)
- Sortings for Reactive Systems (Q5756600) (← links)
