A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST
| Autor: | Amin Timany, Lars Birkedal, Morten Krogh-Jespersen, Léo Stefanesco |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2017 |
| Předmět: |
Functional programming
Functional Programming Languages Programming language Computer science Iris 020207 software engineering 02 engineering and technology Logical Relations computer.software_genre Monad (functional programming) Logical relations Program Logics TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Theory of Programming Languages ST Monad 020204 information systems TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS 0202 electrical engineering electronic engineering information engineering Safety Risk Reliability and Quality computer Software Heap (data structure) Program logic Impredicativity |
| Zdroj: | Timany, A, Stefanesco, L, Krogh-Jespersen, M & Birkedal, L 2018, A Logical Relation for Monadic Encapsulation of State : Proving contextual equivalences in the presence of runST . in Proceedings of the ACM on Programming Languages . Association for Computing Machinery, New York, NY, Proceedings of the ACM on Programming Languages, vol. 2, pp. 64:00-64:28, Principles of Programming Languages (POPL) 2018, Los Angeles, California, United States, 07/01/2018 . https://doi.org/10.1145/3158152 |
| DOI: | 10.1145/3158152 |
| Popis: | 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 e 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. ispartof: pages:1-28 ispartof: Proceedings of ACM on Programming Languages (PACMPL) vol:2 pages:1-28 ispartof: Principles of Programming Languages (POPL) location:Los Angeles, CA, USA date:7 Jan - 13 Jan 2018 status: published |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|