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 metadatas

https://hal.inria.fr/hal-00983850
Contributor : Xavier Leroy <>
Submitted on : Friday, April 25, 2014 - 7:33:55 PM
Last modification on : Friday, May 25, 2018 - 12:02:07 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

165