Recherche - Archive ouverte HAL Accéder directement au contenu

Filtrer vos résultats

4 résultats
Image document

Cosmo: A Concurrent Separation Logic for Multicore OCaml

Glen Mével , Jacques-Henri Jourdan , François Pottier
Proceedings of the ACM on Programming Languages, 2020, 4 (ICFP), ⟨10.1145/3408978⟩
Article dans une revue hal-02929998v1
Image document

Time Credits and Time Receipts in Iris

Glen Mével , Jacques-Henri Jourdan , François Pottier
European Symposium on Programming, Apr 2019, Prague, Czech Republic. pp.3-29, ⟨10.1007/978-3-030-17184-1_1⟩
Communication dans un congrès hal-02183311v1
Image document

Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model

Glen Mével , Jacques-Henri Jourdan
ICFP 2021 - 26th ACM SIGPLAN International Conference on Functional Programming, Aug 2021, Virtual, Japan. ⟨10.1145/3473571⟩
Communication dans un congrès hal-03298759v1
Image document

Thunks and Debits in Separation Logic with Time Credits

François Pottier , Armaël Guéneau , Jacques-Henri Jourdan , Glen Mével
POPL 2024 - 51st ACM SIGPLAN Symposium on Principles of Programming Languages, SIGPLAN, Jan 2024, Londres, United Kingdom
Communication dans un congrès hal-04238691v2