Proof assistants in computer science research

Authors :: Leroy, Xavier
Programming languages, types, compilation and proofs (GALLIUM)
Inria Paris-Rocquencourt
Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
Institut Henri Poincaré
ANR-11-INSE-0003,VERASCO,Vérification formelle d'analyseurs statiques et de compilateurs(2011)
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).

Subjects :: [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS

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

Tools