Relational Parametricity for Computational Effects

DOI10.2168/LMCS-5(3:7)2009MaRDI QIDQ3395102zbMATH OpenFDO

Authors Rasmus Ejlers Møgelberg, Alex Simpson

Publication date 20 August 2009

Published in Logical Methods in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: According to Strachey, a polymorphic program is parametric if it applies a uniform algorithm independently of the type instantiations at which it is applied. The notion of relational parametricity, introduced by Reynolds, is one possible mathematical formulation of this idea. Relational parametricity provides a powerful tool for establishing data abstraction properties, proving equivalences of datatypes, and establishing equalities of programs. Such properties have been well studied in a pure functional setting. Many programs, however, exhibit computational effects, and are not accounted for by the standard theory of relational parametricity. In this paper, we develop a foundational framework for extending the notion of relational parametricity to programming languages with effects.

Recommendations

• Relational parametricity for control considered as a computational effect
• A computational interpretation of parametricity
• A general framework for relational parametricity
• Relational Parametricity and Control
• scientific article; zbMATH DE number 7633806
• scientific article; zbMATH DE number 2061718
• Relating computational effects by \(\top \top \)-lifting
• Relating Computational Effects by ⊤ ⊤-Lifting
• Relativizing relativized computations

Cited in

(6)

• Relating Computational Effects by ⊤ ⊤-Lifting
• scientific article; zbMATH DE number 2061707 (Why is no real title available?)
• On monadic parametricity of second-order functionals
• Relational parametricity for control considered as a computational effect
• From parametricity to conservation laws, via Noether's theorem
• Pragmatic gradual polymorphism with references

This page was built for publication: Relational Parametricity for Computational Effects

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