|
[9]
|
Jean-Christophe Filliâtre.
Proofs on inductive predicates in why3.
In Big Specification: Specification, Proof, and Testing at
Scale, Cambridge, UK, October 2024.
Invited talk.
[ bib |
full text on HAL ]
|
|
[8]
|
Sylvie Boldo, François Clément, David Hamelin, Micaela Mayero, and
Pierre Rousselin.
Teaching divisibility and binomials with Coq.
In 13th International Workshop on Theorem proving components for
Educational software, Nancy, France, 2024.
[ bib |
full text on HAL ]
|
|
[7]
|
Guillaume Melquiond and Josué Moreau.
A safe low-level language for computer algebra and its formally
verified compiler.
In 29th ACM SIGPLAN International Conference on Functional
Programming, volume 8, pages 121--146, Milan, Italy, 2024.
[ bib |
full text on HAL ]
|
|
[6]
|
Florian Faissole, Paul Geneau de Lamarlière, and Guillaume Melquiond.
End-to-end formal verification of a fast and accurate floating-point
approximation.
In 5th International Conference on Interactive Theorem Proving,
volume 309, pages 14:1--14:18, Tbilisi, Georgia, 2024. Leibniz International
Proceedings in Informatics.
[ bib |
DOI |
full text on HAL ]
|
|
[5]
|
Guillaume Melquiond.
Turning the Coq proof assistant into a pocket calculator.
In Coq 2024 - 15th Coq Workshop, Tbilisi, Georgia, 2024.
[ bib |
full text on HAL ]
|
|
[4]
|
Paul Bonnot, Benoît Boyer, Florian Faissole, Claude Marché, and
Raphaël Rieu-Helft.
Formally verified rounding errors of the logarithm-sum-exponential
function.
In Formal Methods in Computer-Aided Design. IEEE, 2024.
[ bib |
full text on HAL ]
|
|
[3]
|
François Pottier, Armaël Guéneau, Jacques-Henri Jourdan, and Glen
Mével.
Thunks and debits in separation logic with time credits.
In POPL 2024 - 51st ACM SIGPLAN Symposium on Principles of
Programming Languages, volume 8. SIGPLAN, ACM, 2024.
[ bib |
full text on HAL ]
|
|
[2]
|
Amin Timany, Armaël Guéneau, and Lars Birkedal.
The logical essence of well-bracketed control flow.
In POPL 2024 - 51st ACM SIGPLAN Symposium on Principles of
Programming Languages. SIGPLAN, ACM, 2024.
[ bib |
full text on HAL ]
|
|
[1]
|
Claude Marché and Denis Cousineau.
De l'avantage de nuancer les décisions binaires.
In 35es Journées Francophones des Langages Applicatifs,
2024.
[ bib |
full text on HAL ]
|