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).
Type de document :
Communication dans un congrès
IHP thematic trimester on Semantics of proofs and certified mathematics, Apr 2014, Paris, France. 2014
Liste complète des métadonnées

https://hal.inria.fr/hal-00983850
Contributeur : Xavier Leroy <>
Soumis le : vendredi 25 avril 2014 - 19:33:55
Dernière modification le : lundi 5 octobre 2015 - 16:57:02

Identifiants

  • 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, Apr 2014, Paris, France. 2014. <hal-00983850>

Partager

Métriques

Consultations de la notice

127