16 citations
- Université Paris-SaclayFR2 papers
- AdaCore (France)FR1 paper
- Board of the Swiss Federal Institutes of TechnologyCH1 paper
- Centre National de la Recherche ScientifiqueFR1 paper
- CERMICSFR1 paper
- ETH ZurichCH1 paper
- Institut national de recherche en sciences et technologies du numériqueFR1 paper
- Laboratoire Méthodes FormellesFR1 paper
- National University of Ireland, MaynoothIE1 paper
- The University of MelbourneAU1 paper
- Tohono O'odham Community CollegeUS1 paper
- Università della Svizzera italianaCH1 paper
3 papers
cs.LO2021★ 2 cited
A strong call-by-need calculus
Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond
We present a call-by-need -calculus that enables strong reduction (that is, reduction inside the body of abstractions) and guarantees that arguments are only evaluated if needed…
cs.LO2021
A Coq Formalization of Lebesgue Integration of Nonnegative Functions
Sylvie Boldo, François Clément, Florian Faissole +2
Integration, just as much as differentiation, is a fundamental calculus tool that is widely used in many scientific domains. Formalizing the mathematical concept of integration and…
cs.LO2020★ 16 cited
VerifyThis 2019: A Program Verification Competition (Extended Report)
Claire Dross, Carlo A. Furia, Marieke Huisman +2
VerifyThis is a series of program verification competitions that emphasize the human aspect: participants tackle the verification of detailed behavioral properties -- something tha…