Search

• < Previous
• 1
• 2
• Next >

---

Logical Step-Indexed Logical Relations

Derek Dreyer ; Amal Ahmed ; Lars Birkedal.

Appel and McAllester's "step-indexed" logical relations have proven to be a simple and effective technique for reasoning about programs in languages with semantically interesting types, such as general recursive types and general reference types. However, proofs using step-indexed models typically&nbsp;[&hellip;]

---

The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types

Ranald Clouston ; Aleš Bizjak ; Hans Bugge Grathwohl ; Lars Birkedal.

We present the guarded lambda-calculus, an extension of the simply typed lambda-calculus with guarded recursive and coinductive types. The use of guarded recursive types ensures the productivity of well-typed programs. Guarded recursive types may be transformed into coinductive types by a&nbsp;[&hellip;]

---

Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages

Lars Birkedal ; Noah Torp-Smith ; Hongseok Yang.

We show how to give a coherent semantics to programs that are well-specified in a version of separation logic for a language with higher types: idealized algol extended with heaps (but with immutable stack variables). In particular, we provide simple sound rules for deriving higher-order frame&nbsp;[&hellip;]

---

Linear Abadi and Plotkin Logic

Lars Birkedal ; Rasmus E. Møgelberg ; Rasmus Lerchedahl Petersen.

We present a formalization of a version of Abadi and Plotkin's logic for parametricity for a polymorphic dual intuitionistic/linear type theory with fixed points, and show, following Plotkin's suggestions, that it can be used to define a wide collection of types, including existential types,&nbsp;[&hellip;]

---

Relational Parametricity and Separation Logic

Lars Birkedal ; Hongseok Yang.

Separation logic is a recent extension of Hoare logic for reasoning about programs with references to shared mutable data structures. In this paper, we provide a new interpretation of the logic for a programming language with higher types. Our interpretation is based on Reynolds's relational&nbsp;[&hellip;]

---

Step-Indexed Relational Reasoning for Countable Nondeterminism

Lars Birkedal ; Aleš Bizjak ; Jan Schwinghammer.

Programming languages with countable nondeterministic choice are computationally interesting since countable nondeterminism arises when modeling fairness for concurrent systems. Because countable choice introduces non-continuous behaviour, it is well-known that developing semantic models for&nbsp;[&hellip;]

---

Nested Hoare Triples and Frame Rules for Higher-order Store

Jan Schwinghammer ; Lars Birkedal ; Bernhard Reus ; Hongseok Yang.

Separation logic is a Hoare-style logic for reasoning about programs with heap-allocated mutable data structures. As a step toward extending separation logic to high-level languages with ML-style general (higher-order) storage, we investigate the compatibility of nested Hoare triples with several&nbsp;[&hellip;]

---

Two for the Price of One: Lifting Separation Logic Assertions

Jacob Thamsborg ; Lars Birkedal ; Hongseok Yang.

Recently, data abstraction has been studied in the context of separation logic, with noticeable practical successes: the developed logics have enabled clean proofs of tricky challenging programs, such as subject-observer patterns, and they have become the basis of efficient verification tools for&nbsp;[&hellip;]

---

First steps in synthetic guarded domain theory: step-indexing in the topos of trees

Lars Birkedal ; Rasmus Ejlers Møgelberg ; Jan Schwinghammer ; Kristian Støvring.

We present the topos S of trees as a model of guarded recursion. We study the internal dependently-typed higher-order logic of S and show that S models two modal operators, on predicates and types, which serve as guards in recursive definitions of terms, predicates, and types. In particular, we show&nbsp;[&hellip;]

---

ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity

Dan Frumin ; Robbert Krebbers ; Lars Birkedal.

We present a new version of ReLoC: a relational separation logic for proving refinements of programs with higher-order state, fine-grained concurrency, polymorphism and recursive types. The core of ReLoC is its refinement judgment $e \precsim e' : \tau$, which states that a program $e$ refines a&nbsp;[&hellip;]

---