English
Proof and computation in Coq
Multi angle
Auteurs : Théry, Laurent (Auteur de la Conférence)
CIRM (Editeur )
68Q60 - Specification and verification (program logics, model checking, etc.)
68T15 - Theorem proving (deduction, resolution, etc.)
68N30 - Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
CIRM (Editeur )
Loading the player...
|
Résumé :
In this talk, we are going to show on some elementary examples how computation can easily be incorporated inside proof in a proof system like Coq.
Codes MSC : 68Q60 - Specification and verification (program logics, model checking, etc.)
68T15 - Theorem proving (deduction, resolution, etc.)
68N30 - Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
|
Informations sur la Vidéo
Réalisateur : Hennenfent, GuillaumeLangue : Anglais Date de publication : 03/02/16 Date de captation : 14/01/16 Sous collection : Research talks arXiv category : Computer Science ; Logic in Computer Science Domaine : Computer Science Format : MP4 (.mp4) - HD Durée : 00:56:59 Audience : Researchers Download : https://videos.cirm-math.fr/2016-01-14_Thery.mp4 
|
Informations sur la Rencontre
Nom de la rencontre : Effective analysis: foundations, implementations, certification / Analyse effective: fondations, programmation, certificationOrganisateurs de la rencontre : Mahboubi, Assia ; Schuster, Peter ; Spitters, Bas Dates : 11/01/16 - 15/01/16 Année de la rencontre : 2016 URL Congrès : http://conferences.cirm-math.fr/1508.html
Données de citation
DOI : 10.24350/CIRM.V.18915003Citer cette vidéo: Théry, Laurent (2016). Proof and computation in Coq. CIRM. Audiovisual resource. doi:10.24350/CIRM.V.18915003 URI : http://dx.doi.org/10.24350/CIRM.V.18915003 |
Voir aussi
- [Multi angle] Verified numerics for ODEs in Isabelle/HOL / Auteur de la Conférence Immler, Fabian.
- [Multi angle] Programming with numerical uncertainties / Auteur de la Conférence Darulova, Eva.
- [Multi angle] Formal verification of numerical analysis programs / Auteur de la Conférence Boldo, Sylvie.
- [ Post-edited] Wrapping in exact real arithmetic / Auteur de la Conférence Müller, Norbert.
Bibliographie
