Skip to Main content Skip to Navigation
New interface
Conference papers

Proof assistants in computer science research

Abstract : This invited talk reflects on how the use of proof assistants is changing the way we do research in various areas of computer science. Three examples are presented: programming languages metatheory (the POPLmark challenge), deductive verification of software (the seL4 project), and formally-verified compilation (the CompCert project).
Document type :
Conference papers
Complete list of metadata
Contributor : Xavier Leroy Connect in order to contact the contributor
Submitted on : Friday, April 25, 2014 - 7:33:55 PM
Last modification on : Thursday, February 3, 2022 - 11:15:57 AM


  • HAL Id : hal-00983850, version 1



Xavier Leroy. Proof assistants in computer science research. IHP thematic trimester on Semantics of proofs and certified mathematics, Institut Henri Poincaré, Apr 2014, Paris, France. ⟨hal-00983850⟩



Record views