# Reasoning about local variables with operationally-based logical relations

@article{Pitts1996ReasoningAL, title={Reasoning about local variables with operationally-based logical relations}, author={Andrew M. Pitts}, journal={Proceedings 11th Annual IEEE Symposium on Logic in Computer Science}, year={1996}, pages={152-163} }

A parametric logical relation between the phrases of an Algol-like language is presented. Its definition involves the structural operational semantics of the language, but was inspired by recent denotationally-based work of O'Hearn and Reynolds on translating Algol into a predicatively polymorphic linear lambda calculus. The logical relation yields an applicative characterisation of contextual equivalence for the language and provides a useful (and complete) method for proving equivalences. Its… Expand

#### Topics from this paper

#### 59 Citations

Relational Reasoning about Functions and Nondeterminism

- Computer Science
- 1999

A uniform, relational proof style for operational arguments about program equivalences is explored, improves and facilitates many previously given proofs, and it is used to establish new proof rules for reasoning about term contexts, recursion, and nondeterminism in higher-order programming languages. 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

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 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

Operational Semantics and Program Equivalence

- Computer Science
- APPSEM
- 2000

This tutorial paper discusses a particular style of operational semantics that enables one to give a 'syntax-directed' inductive definition of termination which is very useful for reasoning about… Expand

Bisimilarity for the Region Calculus

- Computer Science
- High. Order Symb. Comput.
- 2004

This paper presents a theory based on bisimulation, which serves as a coinductive proof principle for showing equivalences of polymorphically region-annotated terms and formulate a syntactic equational theory, which is used elsewhere to prove the soundness of a specializer based on region inference. Expand

Parametric polymorphism and operational equivalence

- Mathematics
- Mathematical Structures in Computer Science
- 2000

Studies of the mathematical properties of impredicative polymorphic types have for the most part focused on the polymorphic lambda calculus of Girard–Reynolds, which is a calculus of total… Expand

Parametric Polymorphism and Operational Equivalence

- Computer Science, Mathematics
- Electron. Notes Theor. Comput. Sci.
- 1997

An operationally-based approach to Reynolds' notion of relational parametricity is developed for an extension of Plotkin's PCF with ∀types and lazy lists and the resulting logical relation is shown to be a useful tool for proving properties of polymorphic types up to a notion of operational equivalence based on Morris-style contextual equivalence. Expand

Operationally-based Program Equivalence Proofs using LCTRSs

- Computer Science
- ArXiv
- 2020

An operationally-based deductive proof method for program equivalence based on encoding the language semantics as logically constrained term rewriting systems (LCTRSs) and the two programs as terms is proposed, which enables the relational verification of program schemas. Expand

An Equational Theory for a Region Calculus

- Mathematics
- 2002

A region calculus is a polymorphically typed lambda calculus with explicit memory management primitives. Every value is annotated with a region in which it is stored. Regions are allocated and… Expand

#### References

SHOWING 1-10 OF 30 REFERENCES

Relational Properties of Domains

- Computer Science, Mathematics
- Inf. Comput.
- 1996

It is shown how the initiality/finality property of invariant relations can be specialized to yield an induction principle for admissible subsets of recursively defined domains, generalizing the principle of structural induction for inductively defined sets. Expand

Parametricity and local variables

- Computer Science
- JACM
- 1995

This work uses relational parametricity to construct a model for an Algol-like language in which interactions between local and non-local entities satisfy certain relational criteria, and supports straightforward validations of all the test equivalences that have been proposed in the literature for local-variable semantics. Expand

Observable Properties of Higher Order Functions that Dynamically Create Local Names, or What's new?

- Mathematics, Computer Science
- MFCS
- 1993

A notion of ‘logical relation’ is introduced which incorporates a version of representation independence for local names and is shown to be complete (and decidable) for expressions of first order types, but incomplete at higher types. Expand

A Fully Abstract Translation between a Lambda-Calculus with Reference Types and Standard ML

- Computer Science
- TLCA
- 1995

This paper describes a syntactic translation for a substantial fragment of the core Standard ML language into a typed λ-calculus with recursive types and imperative features in the form of reference… Expand

From Operational to Denotational Semantics

- Mathematics, Computer Science
- MFPS
- 1991

It is shown how any ordering on programs for which these basic theorems hold can be easily extended to give a fully abstract cpo for the language, giving evidence that any operational semantics with these basicTheorems proven is complete with respect to a denotational semantics. Expand

A Variable Typed Logic of Effects

- Computer Science
- Inf. Comput.
- 1995

A variable typed logic of effects inspired by the variable type systems of Feferman for purely functional languages, which allows for the construction of inductively defined sets and derivation of the corresponding induction principles. Expand

Type Systems for Programming Languages

- Mathematics, Computer Science
- Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics
- 1990

The technique of logical relations is used to prove a semantic completeness theorem and Church–Rosser and strong normalization properties of reduction and encompass basic model-theoretic constructions such as quotients. Expand

Full Abstraction for the Second Order Subset of an Algol-Like Language

- Computer Science
- Theor. Comput. Sci.
- 1996

A denotational semantics for an Algol -like language Alg, which is fully abstract for the second order subset of Alg , which constitutes the first significant full abstraction result for a block structured language with local variables. Expand

Full Abstraction for the Second Order Subset of an Algol-Like Language

- Computer Science
- MFCS
- 1994

We present a denotational semantics for anAlgol like languageAlg which is fully abstract for the second order subset of Alg This constitutes the rst signi cant full abstraction result for a block… Expand

Names and higher-order functions

- Computer Science
- 1994

This dissertation looks in detail at the addition to a functional language of dynamically generated names, an extension of the simply-typed lambdacalculus, which is equivalent to a certain fragment of Standard ML, omitting side-effects, exceptions, datatypes and recursion. Expand