Back to Search
Start Over
Proof assistants in computer science research
- Source :
- IHP thematic trimester on Semantics of proofs and certified mathematics, IHP thematic trimester on Semantics of proofs and certified mathematics, Institut Henri Poincaré, Apr 2014, Paris, France
- Publication Year :
- 2014
- Publisher :
- HAL CCSD, 2014.
-
Abstract
- International audience; 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).
Details
- Language :
- English
- Database :
- OpenAIRE
- Journal :
- IHP thematic trimester on Semantics of proofs and certified mathematics, IHP thematic trimester on Semantics of proofs and certified mathematics, Institut Henri Poincaré, Apr 2014, Paris, France
- Accession number :
- edsair.dedup.wf.001..8711cbe33f5e32b2b7de9d9d332fa137