# A relational modal logic for higher-order stateful ADTs

@inproceedings{Dreyer2010ARM, title={A relational modal logic for higher-order stateful ADTs}, author={Derek Dreyer and Georg Neis and Andreas Rossberg and Lars Birkedal}, booktitle={POPL '10}, year={2010} }

The method of logical relations is a classic technique for proving the equivalence of higher-order programs that implement the same observable behavior but employ different internal data representations. Although it was originally studied for pure, strongly normalizing languages like System F, it has been extended over the past two decades to reason about increasingly realistic languages. In particular, Appel and McAllester's idea of step-indexing has been used recently to develop syntactic… Expand

#### Supplemental Presentations

#### 61 Citations

The impact of higher-order state and control effects on local relational reasoning

- Computer Science
- Journal of Functional Programming
- 2012

This paper defines the first fully abstract logical relation for an ML-like language with recursive types, abstract types, general references and call/cc, and shows how it can enhance the proving power of the possible-worlds model in correspondingly orthogonal ways. Expand

The impact of higher-order state and control effects on local relational reasoning

- Computer Science
- ICFP '10
- 2010

The first fully abstract logical relation for an ML-like language with recursive types, abstract types, general references and call/cc is defined, and it is shown how the proving power of this model can be enhanced under orthogonal restrictions to the expressive power of the language. Expand

The marriage of bisimulations and Kripke logical relations

- Computer Science
- POPL '12
- 2012

RTSs show how bisimulations' support for reasoning about recursive features via *coinduction* can be synthesized with KLRs' support about local state via *state transition systems*, and designed to avoid the limitations of KLRs and bisimulation that preclude their generalization to inter-language reasoning. Expand

Decomposing Logical Relations with Forcing

- Mathematics
- 2011

Logical relations have now the maturity to deal with program equivalence for realistic programming languages with features likes recursive types, higher-order references and first-class… Expand

Decomposing Logical Relations with Forcing Guilhem Jaber

- 2019

Logical relations have now the maturity to deal with program equivalence for realistic programming languages with features likes recursive types, higher-order references and first-class… Expand

A relational realizability model for higher-order stateful ADTs

- Mathematics, Computer Science
- J. Log. Algebraic Methods Program.
- 2012

We present a realizability model for reasoning about contextual equivalence of higher-order programs with impredicative polymorphism, recursive types, and higher-order mutable state. The model… Expand

Predoc Internship Introductory report Toward a formalization in Coq of a parallelization theorem for a concurrent language with general references: an introduction to logical relations

- 2013

Birkedal et al. have recently designed a logical relation for showing the correctness of program transformations for a concurrent language with higher-order functions as well as dynamic memory… Expand

A relational logic for higher-order programs

- Computer Science
- Journal of Functional Programming
- 2019

This work presents a logic, called relational higher-order logic (RHOL), for proving relational properties of a simply typed λ-calculus with inductive types and recursive definitions, and defines sound embeddings for several existing relational type systems such as relational refinement types and type systems for dependency analysis and relative cost. Expand

Logical Step-Indexed Logical Relations

- Computer Science
- 2009 24th Annual IEEE Symposium on Logic In Computer Science
- 2009

A logic LSLR is defined, which is inspired by Plotkin and Abadi's logic for parametricity, but also supports recursively defined relations by means of the modal"later" operator from Appel et al.'s "very modal model" paper. Expand

Logical Step-Indexed Logical Relations

- Computer Science
- LICS
- 2009

A logic LSLR is defined, which is inspired by Plotkin and Abadi's logic for parametricity, but also supports recursively defined relations by means of the modal"later" operator from Appel et al.'s "very modal model" paper. Expand

#### References

SHOWING 1-10 OF 49 REFERENCES

Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types

- Computer Science
- ESOP
- 2006

We present a sound and complete proof technique, based on syntactic logical relations, for showing contextual equivalence of expressions in a λ-calculus with recursive types and impredicative… Expand

Logical Step-Indexed Logical Relations

- Computer Science
- 2009 24th Annual IEEE Symposium on Logic In Computer Science
- 2009

A logic LSLR is defined, which is inspired by Plotkin and Abadi's logic for parametricity, but also supports recursively defined relations by means of the modal"later" operator from Appel et al.'s "very modal model" paper. Expand

Small bisimulations for reasoning about higher-order imperative programs

- Computer Science
- POPL '06
- 2006

We introduce a new notion of bisimulation for showing contextual equivalence of expressions in an untyped lambda-calculus with an explicit store, and in which all expressed values, including… Expand

Operational reasoning for functions with local state

- Mathematics
- 1999

Languages such as ML or Lisp permit the use of recursively defined function expressions with locally declared storage locations. Although this can be very convenient from a programming point of view… Expand

State-dependent representation independence

- Computer Science
- POPL '09
- 2009

This paper develops a possible-worlds model in which relational interpretations of types are allowed to grow over time in a manner that is tightly coupled with changes to some local state, and employs a step-indexed stratification of possible worlds, which facilitates a simplified account of mutable references of higher type. Expand

A very modal model of a modern, major, general type system

- Computer Science
- POPL '07
- 2007

A model of recursive and impredicatively quantified types with mutable references is presented, interpreting all of the type constructors needed for typed intermediate languages and typed assembly languages used for object-oriented and functional languages and establishing a soundness proof of the typing systems underlying these TILs and TALs---ensuring that every well-typed program is safe. Expand

A theory of indirection via approximation

- Computer Science
- POPL '10
- 2010

A general method to construct models containing indirect reference by presenting a "theory of indirection", which is easy to apply to new settings and has a simple axiomatization, which is complete in the sense that all models of it are isomorphic. Expand

Separation Logic for Higher-Order Store

- Computer Science
- CSL
- 2006

This paper introduces an extension of the logic and proves it sound, including the Frame Rule that enables specifications of code to be extended by invariants on parts of the heap that are not accessed, and introduces the benefits of local reasoning available to languages with higher-order store. Expand

Functional translation of a calculus of capabilities

- 2008

A type system designed for a high-level calculus with higher-order functions, algebraic data structures, and references, and a translation of this imperative calculus into a pure calculus, which provides a foundation for the long-term objective of designing a system for specifying and certifying imperative programs with dynamic memory allocation. Expand

Engineering formal metatheory

- Computer Science
- POPL '08
- 2008

This work proposes a novel style for formalizing metatheory, combining locally nameless representation of terms and cofinite quantification of free variable names in inductivedefinitions of relations on terms, leading to developments that are faithful to informal practice, yet require noexternal tool support and little infrastructure within the proof assistant. Expand