Skip to Main content Skip to Navigation
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 : Monday, December 14, 2020 - 5:00:06 PM


  • 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