Multi angle Proof and computation in Coq
Auteurs : Théry, Laurent (Auteur de la Conférence)
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.)