More Web Proxy on the site http://driver.im/

research-article

Open access

A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST

Authors:

Léo Stefanesco,

Morten Krogh-Jespersen,

Lars BirkedalAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 2, Issue POPL

Article No.: 64, Pages 1 - 28

https://doi.org/10.1145/3158152

Published: 27 December 2017 Publication History

Abstract

We present a logical relations model of a higher-order functional programming language with impredicative polymorphism, recursive types, and a Haskell-style ST monad type with runST. We use our logical relations model to show that runST provides proper encapsulation of state, by showing that effectful computations encapsulated by runST are heap independent. Furthermore, we show that contextual refinements and equivalences that are expected to hold for pure computations do indeed hold in the presence of runST. This is the first time such relational results have been proven for a language with monadic encapsulation of state. We have formalized all the technical development and results in Coq.

Supplementary Material

Auxiliary Archive (popl18-p27-aux.zip)

Contains the Coq proof of the theorems presented in the paper.

Download
1.33 MB

WEBM File (monadicencapsulation.webm)

Download
111.10 MB

References

[1]

Amal Ahmed. 2004. Semantics of Types for Mutable State. Ph.D. Dissertation. Princeton University.

Digital Library

[2]

Amal Ahmed. 2006. Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types. In ESOP.

Digital Library

[3]

Amal J. Ahmed, Andrew W. Appel, and Roberto Virga. 2002. A Stratified Semantics of General References Embeddable in Higher-Order Logic. In Proceedings of 17th Annual IEEE Symposium Logic in Computer Science. IEEE Computer Society Press, 75–86.

[4]

Andrew Appel and David McAllester. 2001. An Indexed Model of Recursive Types for Foundational Proof-Carrying Code. TOPLAS 23, 5 (2001), 657–683.

Digital Library

[5]

Andrew Appel, Paul-André Melliès, Christopher Richards, and Jérôme Vouillon. 2007. A Very Modal Model of a Modern, Major, General Type System. In POPL.

[6]

Nick Benton and Peter Buchlovsky. 2007. Semantics of an effect analysis for exceptions. In TLDI.

Digital Library

[7]

Nick Benton, Andrew Kennedy, Lennart Beringer, and Martin Hofmann. 2007. Relational semantics for effect-based program transformations with dynamic allocation. In PPDP.

Digital Library

[8]

Nick Benton, Andrew Kennedy, Lennart Beringer, and Martin Hofmann. 2009. Relational semantics for effect-based program transformations: higher-order store. In PPDP.

Digital Library

[9]

Nick Benton, Andrew Kennedy, Martin Hofmann, and Lennart Beringer. 2006. Reading, writing and relations. In PLAS. Springer.

Digital Library

[10]

Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Kristian Støvring, Jacob Thamsborg, and Hongseok Yang. 2011. StepIndexed Kripke Models over Recursive Worlds. In POPL.

[11]

D. Dreyer, A. Ahmed, and L. Birkedal. 2011. Logical Step-Indexed Logical Relations. LMCS 7, 2:16 (2011).

[12]

Matthias Felleisen and Robert Hieb. 1992. The revised report on the syntactic theories of sequential control and state. TCS 103, 2 (1992), 235–271.

Digital Library

[13]

D. K. Gifford and J. M. Lucassen. 1986. Integrating functional and imperative programming. In LISP.

Digital Library

[14]

Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. 2016. Higher-order ghost state. In ICFP. 256–269.

Digital Library

[15]

Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In POPL. 637–650.

[16]

Robbert Krebbers, Ralf Jung, AleÅą Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. 2017a. The essence of higher-order concurrent separation logic. In European Symposium on Programming (ESOP).

Digital Library

[17]

Robbert Krebbers, Amin Timany, and Lars Birkedal. 2017b. Interactive Proofs in Higher-Order Concurrent Separation Logic. In POPL.

Digital Library

[18]

Morten Krogh-Jespersen, Kasper Svendsen, and Lars Birkedal. 2017. A relational model of types-and-effects in higher-order concurrent separation logic. In POPL.

Digital Library

[19]

John Launchbury and Simon L. Peyton Jones. 1994. Lazy Functional State Threads. In Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation (PLDI ’94). ACM, New York, NY, USA, 24–35.

Digital Library

[20]

John Launchbury and Simon L. Peyton Jones. 1995. State in haskell. Lisp and symbolic computation 8, 4 (1995), 293–341.

Digital Library

[21]

E. Moggi and Amr Sabry. 2001. Monadic Encapsulation of Effects: A Revised Approach (Extended Version). J. Funct. Program. 11, 6 (Nov. 2001), 591–627.

Digital Library

[22]

John C. Reynolds. 1983. Types, Abstraction, and Parametric Polymorphism. Information Processing (1983).

[23]

Steven Schäfer, Tobias Tebbi, and Gert Smolka. 2015. Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions. In ITP (LNCS), Vol. 9236. 359–374.

[24]

Miley Semmelroth and Amr Sabry. 1999. Monadic Encapsulation in ML. In Proceedings of the Fourth ACM SIGPLAN International Conference on Functional Programming (ICFP ’99). ACM, New York, NY, USA, 8–17.

Digital Library

[25]

Jacob Thamsborg and Lars Birkedal. 2011. A Kripke logical relation for effect-based program transformations. In ICFP.

Digital Library

Cited By

Vindum SGeorges ABirkedal LStark KTimany ABlazy STabareau N(2025)The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation LogicProceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3703595.3705876(83-97)Online publication date: 10-Jan-2025
https://dl.acm.org/doi/10.1145/3703595.3705876
Gao CParreaux LChiba SThüm T(2024)Seamless Scope-Safe Metaprogramming through Polymorphic Subtype Inference (Short Paper)Proceedings of the 23rd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/3689484.3690733(121-127)Online publication date: 21-Oct-2024
https://dl.acm.org/doi/10.1145/3689484.3690733
Timany AKrebbers RDreyer DBirkedal L(2024)A Logical Approach to Type SoundnessJournal of the ACM10.1145/367695471:6(1-75)Online publication date: 11-Nov-2024
https://dl.acm.org/doi/10.1145/3676954
Show More Cited By

Index Terms

A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST
1. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program constructs
      1. Functional constructs
      2. Type structures
    2. Program reasoning
      1. Invariants

Recommendations

Mechanized logical relations for termination-insensitive noninterference

We present an expressive information-flow control type system with recursive types, existential types, label polymorphism, and impredicative type polymorphism for a higher-order programming language with higher-order state. We give a novel semantic model ...
Structural Logical Relations
LICS '08: Proceedings of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science

Tait's method (a.k.a. proof by logical relations) is a powerful proof technique frequently used for showing foundational properties of languages based on typed lambda-calculi. Historically, these proofs have been extremely difficult to formalize in ...
Selective strictness and parametricity in structural operational semantics, inequationally

Parametric polymorphism constrains the behavior of pure functional programs in a way that allows the derivation of interesting theorems about them solely from their types, i.e., virtually for free. The formal background of such 'free theorems' is well ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 2, Issue POPL

January 2018

1961 pages

EISSN:2475-1421

DOI:10.1145/3177123

Issue’s Table of Contents

Copyright © 2017 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 December 2017

Published in PACMPL Volume 2, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

31
Total Citations
View Citations
611
Total Downloads

Downloads (Last 12 months)111
Downloads (Last 6 weeks)14

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Vindum SGeorges ABirkedal LStark KTimany ABlazy STabareau N(2025)The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation LogicProceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3703595.3705876(83-97)Online publication date: 10-Jan-2025
https://dl.acm.org/doi/10.1145/3703595.3705876
Gao CParreaux LChiba SThüm T(2024)Seamless Scope-Safe Metaprogramming through Polymorphic Subtype Inference (Short Paper)Proceedings of the 23rd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences10.1145/3689484.3690733(121-127)Online publication date: 21-Oct-2024
https://dl.acm.org/doi/10.1145/3689484.3690733
Timany AKrebbers RDreyer DBirkedal L(2024)A Logical Approach to Type SoundnessJournal of the ACM10.1145/367695471:6(1-75)Online publication date: 11-Nov-2024
https://dl.acm.org/doi/10.1145/3676954
Goncharov SMilius STsampas SUrbat HSobocinski PLago UEsparza J(2024)Bialgebraic Reasoning on Higher-order Program EquivalenceProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662099(1-15)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662099
Gregersen SAguirre AHaselwarter PTassarotti JBirkedal L(2024)Asynchronous Probabilistic Couplings in Higher-Order Separation LogicProceedings of the ACM on Programming Languages10.1145/36328688:POPL(753-784)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632868
Timany AGregersen SStefanesco LHinrichsen JGondelman LNieto ABirkedal L(2024)Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional RefinementProceedings of the ACM on Programming Languages10.1145/36328518:POPL(241-272)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632851
Goncharov SSantamaria ASchröder LTsampas SUrbat H(2024)Logical Predicates in Higher-Order Mathematical Operational SemanticsFoundations of Software Science and Computation Structures10.1007/978-3-031-57231-9_3(47-69)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57231-9_3
Breitner J(2023)More Fixpoints! (Functional Pearl)Proceedings of the ACM on Programming Languages10.1145/36078537:ICFP(686-710)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607853
Ciobâcă ŞLucanu DBuruiană A(2023)Operationally-based program equivalence proofs using LCTRSsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2023.100894135(100894)Online publication date: Oct-2023
https://doi.org/10.1016/j.jlamp.2023.100894
Xie NCong YIkemori KLeijen D(2022)First-class names for effect handlersProceedings of the ACM on Programming Languages10.1145/35632896:OOPSLA2(30-59)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563289
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents