The following pages link to Lars Birkedal (Q444497):
Displaying 50 items.
- (Q198016) (redirect page) (← links)
- A relational realizability model for higher-order stateful ADTs (Q444500) (← links)
- The category-theoretic solution of recursive metric-space equations (Q604478) (← links)
- Synthetic domain theory and models of linear Abadi {\&} Plotkin logic (Q952487) (← links)
- Developing theories of types and computability via realizability (Q1574785) (← links)
- A model of guarded recursion via generalised equilogical spaces (Q1704599) (← links)
- A retrospective on region-based memory management (Q1768483) (← links)
- Equilogical spaces (Q1826625) (← links)
- Relative and modified relative realizability (Q1849865) (← links)
- Relational interpretations of recursive types in an operational setting. (Q1854316) (← links)
- Elementary axioms for local maps of toposes (Q1861481) (← links)
- An inductive characterization of matching in binding bigraphs (Q1941899) (← links)
- On models of higher-order separation logic (Q2130583) (← links)
- Guarded cubical type theory (Q2319985) (← links)
- Relational reasoning for Markov chains in a probabilistic guarded lambda calculus (Q2323974) (← links)
- Reasoning about a machine with local capabilities. Provably safe stack and return pointer management (Q2323991) (← links)
- Compositional non-interference for concurrent programs via separation and framing (Q2324194) (← links)
- Domain-theoretical models of parametric polymorphism (Q2464940) (← links)
- A Kripke logical relation for effect-based program transformations (Q2629855) (← links)
- (Q2753674) (← links)
- A Separation Logic for Fictional Sequential Consistency (Q2802463) (← links)
- Transfinite Step-Indexing: Decoupling Concrete and Logical Steps (Q2802498) (← links)
- Guarded Dependent Type Theory with Coinductive Types (Q2811330) (← links)
- Iris: monoids and invariants as an orthogonal basis for concurrent reasoning (Q2819854) (← links)
- Step-indexed relational reasoning for countable nondeterminism (Q2851672) (← links)
- Parametric domain-theoretic models of polymorphic intuitionistic/linear lambda calculus (Q2852350) (← links)
- Synthetic domain theory and models of linear Abadi \& Plotkin logic (Q2852351) (← links)
- Matching of bigraphs (Q2867883) (← links)
- Fictional Separation Logic (Q2892740) (← links)
- Two for the price of one: lifting separation logic assertions (Q2914243) (← links)
- Charge! (Q2914751) (← links)
- Step-indexed relational reasoning for countable nondeterminism (Q2915708) (← links)
- Views (Q2931804) (← links)
- Logical relations for fine-grained concurrency (Q2931809) (← links)
- ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages (Q2945650) (← links)
- Step-Indexed Logical Relations for Probability (Q2949445) (← links)
- Programming and Reasoning with Guarded Recursion for Coinductive Types (Q2949454) (← links)
- The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types (Q2974778) (← links)
- Higher-order ghost state (Q2985775) (← links)
- Caper (Q2988651) (← links)
- The Essence of Higher-Order Concurrent Separation Logic (Q2988664) (← links)
- A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces (Q3000617) (← links)
- Partiality, State and Dependent Types (Q3007667) (← links)
- Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq (Q3087993) (← links)
- Local realizability toposes and a modal logic for computability (Q3146245) (← links)
- A General Notion of Realizability (Q3149963) (← links)
- The impact of higher-order state and control effects on local relational reasoning (Q3165524) (← links)
- First steps in synthetic guarded domain theory: step-indexing in the topos of trees (Q3166222) (← links)
- Nested Hoare Triples and Frame Rules for Higher-order Store (Q3224687) (← links)
- (Q3431406) (← links)
