Scala step-by-step: Soundness for DOT with step-indexed logical relations in Iris

Autor: Amin Timany, Léo Stefanesco, Paolo G. Giarrusso, Lars Birkedal, Robbert Krebbers

Publikováno v: Proceedings of the ACM on Programming Languages, 4(ICFP)

The metatheory of Scala’s core type system—the Dependent Object Types (DOT) calculus—is hard to extend, like the metatheory of other type systems combining subtyping and dependent types. Soundness of important Scala features therefore remains a

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c6ee8f0b2086b741a3b9b82f66bc0bf8
http://resolver.tudelft.nl/uuid:b2942dd8-e6ac-4568-9208-9dbfc20a2a8a

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

Publikováno v: 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

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 prop

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::110877b26313172618fd9d429b227018
https://lirias.kuleuven.be/handle/123456789/598529

Relational reasoning via probabilistic coupling

Autor: Thomas Espitau, Benjamin Grégoire, Gilles Barthe, Léo Stefanesco, Pierre-Yves Strub, Justin Hsu

Publikováno v: Logic for Programming, Artificial Intelligence, and Reasoning ISBN: 9783662488980
LPAR
LPAR, 2015, Suva, France. pp.387-401, ⟨10.1007/978-3-662-48899-7_27⟩

Probabilistic coupling is a powerful tool for analyzing pairs of probabilistic processes. Roughly, coupling two processes requires finding an appropriate witness process that models both processes in the same probability space. Couplings are powerful

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6d98183bfb0cca26ce1ba3aa821a80cb
http://arxiv.org/abs/1509.03476

Concurrent Separation Logic Meets Template Games

Autor: Paul-André Melliès, Léo Stefanesco

Publikováno v: HAL
LICS
Proceedings of the Thirty-Fifth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020)
Proceedings of the Thirty-Fifth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020), Jul 2020, Saarland, Germany

International audience; An old dream of concurrency theory and programming language semantics has been to uncover the fundamental synchronization mechanisms which regulate situations as different as game semantics for higher-order programs, and Hoare

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1af0572c74698af7068c9f432954c9cf
https://hal.inria.fr/hal-03103163