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

https://hal.inria.fr/hal-00983850
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

Identifiers

  • HAL Id : hal-00983850, version 1

Collections

`

Citation

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⟩

Share

Metrics

Record views

191