# Logical Relations as Types: Proof-Relevant Parametricity for Program Modules

@article{Sterling2021LogicalRA, title={Logical Relations as Types: Proof-Relevant Parametricity for Program Modules}, author={Jonathan Sterling and Robert Harper}, journal={ArXiv}, year={2021}, volume={abs/2010.08599} }

The theory of program modules is of interest to language designers not only for its practical importance to programming, but also because it lies at the nexus of three fundamental concerns in language design:
the phase distinction
,
computational effects
, and
type abstraction
. We contribute a fresh “synthetic” take on program modules that treats modules as the fundamental constructs, in which the usual suspects of prior module calculi (kinds, constructors, dynamic programs) are… Expand

#### 6 Citations

The Multiverse: Logical Modularity for Proof Assistants

- Computer Science
- ArXiv
- 2021

The multiverse is proposed, a general type-theoretic approach to endow proof assistants with logical modularity that describes the inclusion of Coq-style propositions, the strict propositions of Gilbert et al., the exceptional type theory of Pédrot and Tabareau, and general axiomatic extensions of the logic. Expand

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq

- Computer Science
- 2021 IEEE 34th Computer Security Foundations Symposium (CSF)
- 2021

SSProve is introduced, the first general verification framework for machine-checked state-separating proofs, which combines high-level modular proofs about composed protocols with a probabilistic relational program logic for formalizing the lower-level details, which together enable constructing fully machine- checked crypto proofs in the Coq proof assistant. Expand

Normalization for multimodal type theory

- Computer Science
- ArXiv
- 2021

The conversion problem for multimodal type theory (MTT) is considered by characterizing the normal forms of the type theory and proving normalization, which follows from a novel adaptation of Sterling’s Synthetic Tait Computability. Expand

Normalization for Cubical Type Theory

- Computer Science, Mathematics
- 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
- 2021

The normalization result is reduction-free, in the sense of yielding a bijection between equivalence classes of terms in context and a tractable language of β/η-normal forms. Expand

A cost-aware logical framework

- Computer Science
- ArXiv
- 2021

It is argued that the cost structure of programsmotivates a phase distinction between intension and extension, which contributes a synthetic account of cost structure as a computational effect in which cost-aware programs enjoy an internal noninterference property: input/output behavior cannot depend on cost. Expand

A Cubical Language for Bishop Sets

- Computer Science, Mathematics
- ArXiv
- 2020

We present XTT, a version of Cartesian cubical type theory specialized for Bishop sets a la Coquand, in which every type enjoys a definitional version of the uniqueness of identity proofs. Using… Expand

#### References

SHOWING 1-10 OF 195 REFERENCES

Abstract effects and proof-relevant logical relations

- Computer Science
- POPL 2014
- 2012

We give 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… Expand

Proofs for free

- Computer Science
- Journal of Functional Programming
- 2012

It is shown how a typing judgement in System F can be translated into a relational statement (in second-order predicate logic) about inhabitants of the type, and it is obtained that for pure type systems (PTSs) there is a PTS that can be used as a logic for parametricity. Expand

The essence of ML

- Computer Science
- POPL '88
- 1988

It is proved that the important programming features of ML cannot be added to any impredicative language, such as the Girard-Reynolds calculus, without implicitly assuming a type of all types. Expand

Deciding type equivalence in a language with singleton kinds

- Computer Science
- POPL '00
- 2000

Inspired by Coquand's result for type theory, the decidability of constructor equivalence for λ&Pgr;&Sgr;S≤ is proved by exhibiting a novel — though slightly inefficient — type-directed comparison algorithm. Expand

Proofs for free Parametricity for dependent types JEAN -P HILIPPE B ERNARDY and P ATRIK J ANSSON

- Mathematics
- 2012

Reynolds’ abstraction theorem (Reynolds, J. C. (1983) Types, abstraction and parametric polymorphism, Inf. Process. 83(1), 513–523) shows how a typing judgement in System F can be translated into a… Expand

A reasonably exceptional type theory

- Computer Science
- Proc. ACM Program. Lang.
- 2019

RETT is the first full dependent type theory to support consistent reasoning about exceptional terms, and the CoqRETT plugin readily brings this ability to Coq programmers. Expand

A type-theoretic interpretation of standard ML

- Computer Science
- Proof, Language, and Interaction
- 2000

Robin Milner's work on ML culminated in his ambitious proposal for Standard ML that sought to extend ML to a full-scale programming language supporting functional and imperative programming and an expressive module system and provided a precise de nition of the static and dynamic semantics in a uniform relational framework. Expand

A General Framework for Relational Parametricity

- Computer Science, Mathematics
- LICS
- 2018

This work develops an abstract framework for relational parametricity that delivers a model expressing Reynolds' theory in a direct and natural way, and offers a novel relationally parametric model of System F (after Orsanigo), which is proof-relevant in the sense that witnesses of relatedness are themselves suitably related. Expand

Proof-Relevant Logical Relations for Name Generation

- Computer Science
- TLCA
- 2013

This work addresses the issue of contextual equivalence in higher-order languages with name generation by using a monad that combines dynamic allocation with continuations, at some cost to abstraction. Expand

Formal parametric polymorphism

- Mathematics
- 1993

A polymorphic function is parametric if its behavior does not depend on the type at which it is instantiated. Starting with Reynolds' work, the study of parametricity is typically semantic. In this… Expand