research-article

Open access

Purity of an ST monad: full abstraction by semantically typed back-translation

Authors:

Dominique Devriese,

Amin TimanyAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 6, Issue OOPSLA1

Article No.: 82, Pages 1 - 27

https://doi.org/10.1145/3527326

Published: 29 April 2022 Publication History

Abstract

In 1995, Launchbury and Peyton Jones extended Haskell with an ST monad that allows the programmer to use higher-order mutable state. They informally argued that these state computations were safely encapsulated, and as such, that the rich reasoning principles stemming from the purity of the language, were not threatened.

In this paper, we give a formal account of the preservation of purity after adding an ST monad to a simply-typed call-by-value recursive lambda calculus. We state and prove full abstraction when embedding the pure language into its extension with ST; contextual equivalences from the pure language continue to hold in the presence of ST.

Proving full abstraction of compilers is usually done by emulating or back-translating the target features (here: ST computations) into the source language, a well-known challenge in the secure compilation community. We employ a novel proof technique for proving our full abstraction result that allows us to use a semantically (but not syntactically) typed back-translation into an intermediate language. We believe that this technique provides additional insight into our proof and that it is of general interest to researchers studying programming languages and compilers using full abstraction.

The results presented here are fully formalized in the Coq proof assistant using the Iris framework.

References

[1]

Martín Abadi. 1998. Protection in Programming-Language Translations: Mobile Object Systems. In European Conference on Object-Oriented Programming. Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-49255-0_70

[2]

Martín Abadi. 1999. Protection in Programming-Language Translations. In Secure Internet Programming. Springer-Verlag. isbn:3-540-66130-1

Digital Library

[3]

Carmine Abate, Roberto Blanco, Deepak Garg, Catalin Hritcu, Marco Patrignani, and Jérémy Thibault. 2019. Journey beyond full abstraction: Exploring robust property preservation for secure compilation. In 2019 IEEE 32nd Computer Security Foundations Symposium (CSF). 256–25615.

[4]

Andrew W. Appel and David McAllester. 2001. An Indexed Model of Recursive Types for Foundational Proof-Carrying Code. ACM Trans. Program. Lang. Syst., 23, 5 (2001), Sept., 657–683. issn:0164-0925 https://doi.org/10.1145/504709.504712

Digital Library

[5]

Dominique Devriese, Marco Patrignani, and Frank Piessens. 2016. Fully-Abstract Compilation by Approximate Back-Translation. In Principles of Programming Languages (POPL ’16). ACM, 164–177. https://doi.org/10.1145/2837614.2837618

Digital Library

[6]

Paul Hudak, John Hughes, Simon Peyton Jones, and Philip Wadler. 2007. A History of Haskell: Being Lazy with Class. In History of Programming Languages.

[7]

Koen Jacobs, Dominique Devriese, and Amin Timany. 2022. Artifact - Purity of an ST Monad. https://doi.org/10.5281/zenodo.6329773

Digital Library

[8]

Koen Jacobs, Amin Timany, and Dominique Devriese. 2021. Fully Abstract from Static to Gradual. Proc. ACM Program. Lang., 5, POPL (2021), Article 7, Jan., 30 pages. https://doi.org/10.1145/3434288

Digital Library

[9]

Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28 (2018).

[10]

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, 24–35. isbn:089791662X https://doi.org/10.1145/178243.178246

Digital Library

[11]

E. Moggi and Amr Sabry. 2001. Monadic encapsulation of effects: a revised approach (extended version). Journal of Functional Programming, 11, 6 (2001), 591–627. https://doi.org/10.1017/S0956796801004154

Digital Library

[12]

Max S. New and Amal Ahmed. 2018. Graduality from Embedding-Projection Pairs. Proc. ACM Program. Lang., 2, ICFP (2018), Article 73, July, 30 pages. https://doi.org/10.1145/3236768

Digital Library

[13]

Max S. New, William J. Bowman, and Amal Ahmed. 2016. Fully Abstract Compilation via Universal Embedding. In International Conference on Functional Programming. ACM, 103–116. https://doi.org/10.1145/2951913.2951941

Digital Library

[14]

Joachim Parrow. 2008. Expressiveness of Process Algebras. Electronic Notes in Theoretical Computer Science, 209 (2008), April, 173–186. issn:1571-0661 https://doi.org/10.1016/j.entcs.2008.04.011

Digital Library

[15]

Marco Patrignani. 2020. Why should anyone use colours? or, syntax highlighting beyond code snippets. arXiv preprint arXiv:2001.11334.

[16]

Marco Patrignani, Amal Ahmed, and Dave Clarke. 2019. Formal Approaches to Secure Compilation: A Survey of Fully Abstract Compilation and Related Work. ACM Comput. Surv., 51, 6 (2019), Article 125, Feb., 36 pages. issn:0360-0300 https://doi.org/10.1145/3280984

Digital Library

[17]

Marco Patrignani, Eric Mark Martin, and Dominique Devriese. 2021. On the Semantic Expressiveness of Recursive Types. Proc. ACM Program. Lang., 5, POPL (2021), Article 21, Jan., 29 pages. https://doi.org/10.1145/3434302

Digital Library

[18]

Benjamin C. Pierce. 2002. Types and programming languages. MIT press.

Digital Library

[19]

Lau Skorstengaard, Dominique Devriese, and Lars Birkedal. 2019. StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities. Proc. ACM Program. Lang., 3, POPL (2019), Jan., 19:1–19:28. issn:2475-1421 https://doi.org/10.1145/3290332

Digital Library

[20]

Amin Timany, Robbert Krebbers, and Lars Birkedal. 2017. Logical relations in Iris. In CoqPL, Date: 2017/01/21-2017/01/21, Location: Paris.

[21]

Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, and Lars Birkedal. 2017. A Logical Relation for Monadic Encapsulation of State: Proving Contextual Equivalences in the Presence of RunST. Proc. ACM Program. Lang., 2, POPL (2017), Article 64, Dec., 28 pages. https://doi.org/10.1145/3158152

Digital Library

[22]

Philip Wadler. 1993. Monads for functional programming. In Program Design Calculi, Manfred Broy (Ed.). Springer Berlin Heidelberg, 233–264. isbn:978-3-662-02880-3

Cited By

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
Lutze MMadsen M(2024)Associated Effects: Flexible Abstractions for Effectful ProgrammingProceedings of the ACM on Programming Languages10.1145/36563938:PLDI(394-416)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656393
Andrici CCiobâcă ȘHriţcu CMartínez GRivas ETanter ÉWinterhalter T(2024)Securing Verified IO Programs Against Unverified Code in F*Proceedings of the ACM on Programming Languages10.1145/36329168:POPL(2226-2259)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632916
Show More Cited By

Index Terms

Purity of an ST monad: full abstraction by semantically typed back-translation
1. Social and professional topics
  1. Professional topics
    1. History of computing
      1. History of programming languages
2. Software and its engineering
  1. Software notations and tools
    1. General programming languages

Recommendations

Bringing back monad comprehensions
Haskell '11: Proceedings of the 4th ACM symposium on Haskell

This paper is about a Glasgow Haskell Compiler (GHC) extension that generalises Haskell's list comprehension notation to monads. The monad comprehension notation implemented by the extension supports generator and filter clauses, as was the case in the ...
The Key monad: type-safe unconstrained dynamic typing
Haskell '16

We present a small extension to Haskell called the Key monad. With the Key monad, unique keys of different types can be created and can be tested for equality. When two keys are equal, we also obtain a concrete proof that their types are equal. This ...
Full Abstraction and the Context Lemma

It is impossible to add a combinator to PCF to achieve full abstraction for models such as Berry's stable domains in a way analogous to the addition of the "parallel-or" combinator that achieves full abstraction for the familiar complete partial order (...

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 6, Issue OOPSLA1

April 2022

687 pages

EISSN:2475-1421

DOI:10.1145/3534679

Issue’s Table of Contents

Copyright © 2022 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: 29 April 2022

Published in PACMPL Volume 6, Issue OOPSLA1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
517
Total Downloads

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

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

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
Lutze MMadsen M(2024)Associated Effects: Flexible Abstractions for Effectful ProgrammingProceedings of the ACM on Programming Languages10.1145/36563938:PLDI(394-416)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656393
Andrici CCiobâcă ȘHriţcu CMartínez GRivas ETanter ÉWinterhalter T(2024)Securing Verified IO Programs Against Unverified Code in F*Proceedings of the ACM on Programming Languages10.1145/36329168:POPL(2226-2259)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632916
Moine AWestrick SBalzer S(2024)DisLog: A Separation Logic for DisentanglementProceedings of the ACM on Programming Languages10.1145/36328538:POPL(302-331)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632853
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
Giallorenzo SMontesi FPeressotti M(2024)Choral: Object-oriented Choreographic ProgrammingACM Transactions on Programming Languages and Systems10.1145/363239846:1(1-59)Online publication date: 16-Jan-2024
https://dl.acm.org/doi/10.1145/3632398
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
Rao XGeorges ALegoupil MWatt CPichon-Pharabod JGardner PBirkedal L(2023)Iris-Wasm: Robust and Modular Verification of WebAssembly ProgramsProceedings of the ACM on Programming Languages10.1145/35912657:PLDI(1096-1120)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591265

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