Abstract effects and proof-relevant logical relations

DOI10.1145/2535838.2535869MaRDI QIDQ5408454zbMATH OpenOpenAlexFDO

Authors Nick Benton, Martin Hofmann, Vivek Nigam

Publication date 10 April 2014

Published in Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1212.5692

zbMATH Keywords

logical relationsparametricityprogram transformationregion analysistype and effect systems

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: We introduce a novel variant of logical relations that maps types not merely to partial equivalence relations on values, as is commonly done, but rather to a proof-relevant generalisation thereof, namely setoids. The objects of a setoid establish that values inhabit semantic types, whilst its morphisms are understood as proofs of semantic equivalence. The transition to proof-relevance solves two well-known problems caused by the use of existential quantification over future worlds in traditional Kripke logical relations: failure of admissibility, and spurious functional dependencies. We illustrate the novel format with two applications: a direct-style validation of Pitts and Stark's equivalences for "new" and a denotational semantics for a region-based effect system that supports type abstraction in the sense that only externally visible effects need to be tracked; non-observable internal modifications, such as the reorganisation of a search tree or lazy initialisation, can count as `pure' or `read only'. This `fictional purity' allows clients of a module soundly to validate more effect-based program equivalences than would be possible with traditional effect systems.

Recommendations

• Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
• A Kripke logical relation for effect-based program transformations
• A Kripke logical relation for effect-based program transformations
• The impact of higher-order state and control effects on local relational reasoning
• The impact of higher-order state and control effects on local relational reasoning

Cited in

(9)

• Counting successes: effects and transformations for non-deterministic programs
• Relational cost analysis in a functional-imperative setting
• Internal parametricity for cubical type theory
• On the versatility of open logical relations. Continuity, automatic differentiation, and a containment theorem
• A Kripke logical relation for effect-based program transformations
• Logical relations and nondeterminism
• A model of PCF in guarded type theory
• A fibrational tale of operational logical relations: pure, effectful and differential
• Higher-order asynchronous effects

This page was built for publication: Abstract effects and proof-relevant logical relations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5408454)