|
[6]
|
Guillaume Melquiond and Raphaël Rieu-Helft.
WhyMP, a formally verified arbitrary-precision integer library.
Journal of Symbolic Computation, 115:74--95, 2023.
[ bib |
DOI |
full text on HAL ]
|
|
[5]
|
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin
Timany, Alix Trieu, Dominique Devriese, and Lars Birkedal.
Cerise: Program verification on a capability machine in the presence
of untrusted code.
Journal of the ACM, 2023.
[ bib |
DOI |
full text on HAL ]
|
|
[4]
|
Sylvie Boldo, Claude-Pierre Jeannerod, Guillaume Melquiond, and Jean-Michel
Muller.
Floating-point arithmetic.
Acta Numerica, 32:203--290, 2023.
[ bib |
DOI |
full text on HAL ]
|
|
[3]
|
Érik Martin-Dorel, Guillaume Melquiond, and Pierre Roux.
Enabling floating-point arithmetic in the Coq proof assistant.
Journal of Automated Reasoning, 67(33), 2023.
[ bib |
DOI |
full text on HAL ]
|
|
[2]
|
Thibaut Balabonski, Antoine Lanco, and Guillaume Melquiond.
A strong call-by-need calculus.
Logical Methods in Computer Science, 19(1), 2023.
[ bib |
DOI |
full text on HAL ]
|
|
[1]
|
Sylvie Boldo, Nicolas Brisebarre, and Jean-Michel Muller.
Le dilemme du fabricant de tables.
La Recherche, 572, 2023.
[ bib |
full text on HAL ]
|
|
[8]
|
Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, and
Houda Mouhcine.
A Coq formalization of Lebesgue induction principle and
Tonelli's theorem.
In 25th International Symposium on Formal Methods (FM 2023),
volume 14000 of Lecture Notes in Computer Science, pages 39--55, 2023.
[ bib |
DOI |
full text on HAL ]
|
|
[7]
|
Jean-Christophe Filliâtre and Andrei Paskevich.
L'arithmétique de séparation.
In Timothy Bourke and Delphine Demange, editors, JFLA 2023 -
34èmes Journées Francophones des Langages Applicatifs, pages
274--283, 2023.
[ bib |
full text on HAL ]
|
|
[6]
|
Paul Geneau de Lamarlière, Guillaume Melquiond, and Florian Faissole.
Slimmer formal proofs for mathematical libraries.
In Int. Conf. on Computer Arithmetic, 2023.
[ bib |
full text on HAL ]
|
|
[5]
|
Sylvain Conchon and Alexandrina Korneva.
The cubicle fuzzy loop: A fuzzing-based extension for the Cubicle
model checker.
In Carla Ferreira and Tim A. C. Willemse, editors, Software
Engineering and Formal Method, volume 14323 of Lecture Notes in
Computer Science, pages 30--46. Springer, 2023.
[ bib |
DOI |
full text on HAL ]
|
|
[4]
|
Léo Andrès, Pierre Chambart, and Jean-Christophe Filliâtre.
Wasocaml: compiling OCaml to WebAssembly.
In João Saraiva and João Fernandes, editors, 35th
Symposium on Implementation and Application of Functional Languages, 2023.
[ bib |
full text on HAL ]
|
|
[3]
|
Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars
Birkedal, and Derek Dreyer.
Melocoton: A program logic for verified interoperability between
OCaml and C.
In Object-Oriented Programming, Systems, Languages &
Applications. ACM, 2023.
[ bib |
DOI |
full text on HAL ]
|
|
[2]
|
Xavier Denis and Jacques-Henri Jourdan.
Specifying and verifying higher-order rust iterators.
In Sriram Sankaranarayanan and Natasha Sharygina, editors, Tools
and Algorithms for the Construction and Analysis of Systems, volume 13994 of
Lecture Notes in Computer Science, pages 93--110. Springer, 2023.
[ bib |
DOI |
full text on HAL ]
|
|
[1]
|
Assia Mahboubi and Guillaume Melquiond.
Manifest termination.
In 29th International Conference on Types for Proofs and
Programs, pages 1--3, Valencia, Spain, 2023.
[ bib |
full text on HAL ]
|