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 : vendredi 25 mai 2018 - 12:02:07

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

157