Zobrazeno 1 - 10
of 26
pro vyhledávání: '"Jacques-Henri Jourdan"'
Autor:
Xavier Denis, Jacques-Henri Jourdan
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
Tools and Algorithms for the Construction and Analysis of Systems (TACAS), ETAPS, Apr 2023, Paris, France. pp.93-110, ⟨10.1007/978-3-031-30820-8_9⟩
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783031308192
Tools and Algorithms for the Construction and Analysis of Systems (TACAS), ETAPS, Apr 2023, Paris, France. pp.93-110, ⟨10.1007/978-3-031-30820-8_9⟩
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783031308192
In Rust, programs are often written using iterators, but these pose problems for verification: they are non-deterministic, infinite, and often higher-order, effectful and built using adapters. We present a general framework for specifying and reasoni
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::168ac2d888243a160093dd23473a9260
https://hal.science/hal-03827702v2/file/main.pdf
https://hal.science/hal-03827702v2/file/main.pdf
Publikováno v:
PLDI 2022-43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation
PLDI 2022-43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2022, San Diego CA USA, United States. pp.841-856, ⟨10.1145/3519939.3523704⟩
PLDI '22
PLDI 2022-43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2022, San Diego CA USA, United States. pp.841-856, ⟨10.1145/3519939.3523704⟩
PLDI '22
International audience; Rust is a systems programming language that offers both lowlevel memory operations and high-level safety guarantees, via a strong ownership type system that prohibits mutation of aliased state. In prior work, Matsushita et al.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4135a9010341ceb1abf9c622f2d6ff3a
https://doi.org/10.1145/3519939.3523704
https://doi.org/10.1145/3519939.3523704
Publikováno v:
Formal Methods and Software Engineering ISBN: 9783031172434
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::5a1661338d1bf67e7d7ae548bd3efb6f
https://doi.org/10.1007/978-3-031-17244-1_6
https://doi.org/10.1007/978-3-031-17244-1_6
Publikováno v:
Communications of the Acm, 64, 4, pp. 144-152
Communications of the ACM
Communications of the Acm, 64, 144-152
Communications of the ACM
Communications of the Acm, 64, 144-152
The promise and the challenges of the first industry-supported language to master the trade-off between safety and control.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1dcb3c5cfc0a2cc97d5d03846bc73769
Publikováno v:
Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2020, 4 (POPL), ⟨10.1145/3371101⟩
Proceedings of the ACM on Programming Languages, 2020, 4 (POPL), ⟨10.1145/3371101⟩
Proceedings of the ACM on Programming Languages, ACM, 2020, 4 (POPL), ⟨10.1145/3371101⟩
Proceedings of the ACM on Programming Languages, 2020, 4 (POPL), ⟨10.1145/3371101⟩
International audience; We verify the partial correctness of a "local generic solver", that is, an on-demand, incremental, memoizing least fixed point computation algorithm. The verification is carried out in Iris, a modern breed of concurrent separa
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1a8f73dced264c8159da15fea52104d9
https://hal.archives-ouvertes.fr/hal-02351562/file/main.pdf
https://hal.archives-ouvertes.fr/hal-02351562/file/main.pdf
Publikováno v:
ACM Transactions on Programming Languages and Systems (TOPLAS)
ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2017, 39 (4), pp.1-36. ⟨10.1145/3064848⟩
ACM Transactions on Programming Languages and Systems (TOPLAS), 2017, 39 (4), pp.1-36. ⟨10.1145/3064848⟩
ACM Transactions on Programming Languages and Systems (TOPLAS), ACM, 2017, 39 (4), pp.1-36. ⟨10.1145/3064848⟩
ACM Transactions on Programming Languages and Systems (TOPLAS), 2017, 39 (4), pp.1-36. ⟨10.1145/3064848⟩
International audience; The syntax of the C programming language is described in the C11 standard by an ambiguous context-free grammar, accompanied with English prose that describes the concept of " scope " and indicates how certain ambiguous code fr
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::33a46063777587db07c9fd0a434b2a26
https://doi.org/10.1145/3064848
https://doi.org/10.1145/3064848
Publikováno v:
Programming Languages and Systems ISBN: 9783030171834
ESOP
European Symposium on Programming
European Symposium on Programming, Apr 2019, Prague, Czech Republic. pp.3-29, ⟨10.1007/978-3-030-17184-1_1⟩
ESOP
European Symposium on Programming
European Symposium on Programming, Apr 2019, Prague, Czech Republic. pp.3-29, ⟨10.1007/978-3-030-17184-1_1⟩
International audience; We present a machine-checked extension of the program logic Iris with time credits and time receipts, two dual means of reasoning about time. Whereas time credits are used to establish an upper bound on a program's execution t
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a083bdaf2b61bee531b77cf87fc124a5
https://doi.org/10.1007/978-3-030-17184-1_1
https://doi.org/10.1007/978-3-030-17184-1_1
Publikováno v:
Proceedings of the ACM on Programming Languages, 2(POPL)
Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages
Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust's safety claims have been formall
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f48fb77d90efcb6b190d0e3a41a554b1
https://doi.org/10.1145/3158154
https://doi.org/10.1145/3158154
Autor:
Joseph Tassarotti, Amin Timany, Jacques-Henri Jourdan, Ralf Jung, Derek Dreyer, Robbert Krebbers, Arthur Charguéraud, Jan-Oliver Kaiser
Publikováno v:
Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, 2(ICFP)
International Conference on Functional Programming (ICFP 2018)
International Conference on Functional Programming (ICFP 2018), ACM, Sep 2018, St Louis, MO, United States. pp.77, ⟨10.1145/3236772⟩
Krebbers, R, Jourdan, J-H, Jung, R, Tassarotti, J, Kaiser, J-O, Timany, A, Charguéraud, A & Dreyer, D 2018, ' MoSeL: a general, extensible modal framework for interactive proofs in separation logic ', PACMPL, bind 2, nr. ICFP, s. 77:1-77:30 . https://doi.org/10.1145/3236772
Proceedings of the ACM on Programming Languages, 2(ICFP)
International Conference on Functional Programming (ICFP 2018)
International Conference on Functional Programming (ICFP 2018), ACM, Sep 2018, St Louis, MO, United States. pp.77, ⟨10.1145/3236772⟩
Krebbers, R, Jourdan, J-H, Jung, R, Tassarotti, J, Kaiser, J-O, Timany, A, Charguéraud, A & Dreyer, D 2018, ' MoSeL: a general, extensible modal framework for interactive proofs in separation logic ', PACMPL, bind 2, nr. ICFP, s. 77:1-77:30 . https://doi.org/10.1145/3236772
A number of tools have been developed for carrying out separation-logic proofs mechanically using an interactive proof assistant. One of the most advanced such tools is the Iris Proof Mode (IPM) for Coq, which offers a rich set of tactics for making
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8b8304b64369c2034fce0d766bbd12d0
https://lirias.kuleuven.be/handle/123456789/627447
https://lirias.kuleuven.be/handle/123456789/627447
Publikováno v:
European Symposium on Programming (ESOP)
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Programming Languages and Systems
Krebbers, R, Jung, R, Bizjak, A, Jourdan, J-H, Dreyer, D & Birkedal, L 2017, The Essence of Higher-Order Concurrent Separation Logic . in H Yang (ed.), Programming Languages and Systems: 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22--29, 2017, Proceedings . Springer VS, Springer, Berlin, Heidelberg, Lecture Notes in Computer Science, pp. 696-723, European Symposium on Programming, Uppsala, Sweden, 22/04/2017 . https://doi.org/10.1007/978-3-662-54434-1_26
Programming Languages and Systems
Programming Languages and Systems ISBN: 9783662544334
ESOP
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Programming Languages and Systems
Krebbers, R, Jung, R, Bizjak, A, Jourdan, J-H, Dreyer, D & Birkedal, L 2017, The Essence of Higher-Order Concurrent Separation Logic . in H Yang (ed.), Programming Languages and Systems: 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22--29, 2017, Proceedings . Springer VS, Springer, Berlin, Heidelberg, Lecture Notes in Computer Science, pp. 696-723, European Symposium on Programming, Uppsala, Sweden, 22/04/2017 . https://doi.org/10.1007/978-3-662-54434-1_26
Programming Languages and Systems
Programming Languages and Systems ISBN: 9783662544334
ESOP
Concurrent separation logics CSLs have come of age, and with age they have accumulated a great deal of complexity. Previous work on the Iris logic attempted to reduce the complex logical mechanisms of modern CSLs to two orthogonal concepts: partial c
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3946c8679301309a7c15c2191fc6a3a4