|
[10]
|
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 ]
|
|
[9]
|
Marie Kerjean, Micaela Mayero, and Pierre Rousselin.
Maths with Coq in L1, a pedagogical experiment.
In ThEdu 2024 - 13th International Workshop on Theorem proving
components for Educational software, 2024.
[ 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 ]
|
|
[3]
|
Benoît Boyer, Florian Faissole, and Guillaume Melquiond.
Method and system for converting an input computer program into an
output computer program achieving a target global accuracy.
Technical report, Patent number EP4235397, 2024.
[ bib |
full text on HAL ]
|
|
[2]
|
Paul Bonnot, Benoît Boyer, Florian Faissole, and Claude Marché.
Generating and certifying accuracy properties of floating-point
programs.
Technical Report RR-9564, Inria, 2024.
[ bib |
full text on HAL ]
|
|
[1]
|
Denis Cousineau, Hiroaki Inoue, Claude Marché, and David Mentré.
A methodological guide for the validation of logic modelling of
Ladder instructions.
Technical Report 0522, Inria, 2024.
[ bib |
full text on HAL ]
|