Theorems for free from separation logic specifications

Autor: Guilhem Jaber, Nikos Tzevelekos, Thomas Dinsdale-Young, Kasper Svendsen, Armaël Guéneau, Lars Birkedal

Publikováno v: Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2021, 5 (ICFP), pp.1-29. ⟨10.1145/3473586⟩
Birkedal, L, Dinsdale-Young, T, Guéneau, A, Jaber, G, Svendsen, K & Tzevelekos, N 2021, ' Theorems for free from separation logic specifications ', Proceedings of the ACM on Programming Languages, vol. 5, no. ICFP, 81 . https://doi.org/10.1145/3473586
Proceedings of the ACM on Programming Languages, 2021, 5 (ICFP), pp.1-29. ⟨10.1145/3473586⟩

International audience; Separation logic specifications with abstract predicates intuitively enforce a discipline that constrains when and how calls may be made between a client and a library. Thus a separation logic specification of a library intuit

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e35f5012f890d1efb00d735a96ce54c2
https://hal.archives-ouvertes.fr/hal-03510684

Complete trace models of state and control

Autor: Guilhem Jaber, Andrzej S. Murawski

Publikováno v: ESOP 2021-30th European Symposium on Programming
ESOP 2021-30th European Symposium on Programming, Mar 2021, Luxembourg, Luxembourg. pp.348-374, ⟨10.1007/978-3-030-72019-3_13⟩
Programming Languages and Systems ISBN: 9783030720186
ESOP
Programming Languages and Systems

We consider a hierarchy of four typed call-by-value languages with either higher-order or ground-type references and with either $$\mathrm {call/cc}$$ call / cc or no control operator.Our first result is a fully abstract trace model for the most expr

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8f62451552a7aff887b68db6258055f9
https://hal.science/hal-03510374

SyTeCi: Automating Contextual Equivalence for Higher-Order Programs with References

Autor: Guilhem Jaber

Publikováno v: Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, In press, 28, pp.1-28. ⟨10.1145/3371127⟩
Proceedings of the ACM on Programming Languages, ACM, In press, 28, pp.1-28. ⟨10.1145/3371127⟩

We propose a framework to study contextual equivalence of programs written in a call-by-value functional language with local integer references. It reduces the problem of contextual equivalence to the problem of non-reachability in a transition syste

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a90d1a3c2e44525bead2321141a6279c
https://hal.science/hal-02388621

A Kripke logical relation for effect-based program transformations

Autor: Guilhem Jaber, Jacob Thamsborg, Lars Birkedal, Filip Sieczkowski

Publikováno v: Birkedal, L, Jaber, G, Sieczkowski, F & Thamsborg, J 2016, ' A Kripke logical relation for effect-based program transformations ', Information and Computation, vol. 249, pp. 160-189 . https://doi.org/10.1016/j.ic.2016.04.003

We present a Kripke logical relation for showing the correctness of program transformations based on a region-polymorphic type-and-effect system for an ML-like programming language with higher-order store and dynamic allocation. We also show how to u

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::116bcecb3c15c97bc759c2db538559b2
https://pure.au.dk/portal/da/publications/a-kripke-logical-relation-for-effectbased-program-transformations(18a38ebf-4477-4156-8122-d8786e0507ec).html

The Definitional Side of the Forcing

Autor: Nicolas Tabareau, Pierre-Marie Pédrot, Guilhem Jaber, Gabriel Lewertowski, Matthieu Sozeau

Publikováno v: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science-LICS 16
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science-LICS '16
LICS
Logics in Computer Science
Logics in Computer Science, May 2016, New York, United States. ⟨10.1145/http://dx.doi.org/10.1145/2933575.2935320⟩
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science

International audience; This paper studies forcing translations of proofs in dependent type theory, through the Curry-Howard correspondence. Based on a call-by-push-value decomposition, we synthesize two simply-typed translations: i) one call-by-valu

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2f614f0d86617ff0897795afebf75615