Proof and computation in Coq
Apparaît également dans la collection : Exposés de recherche
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.
Apparaît également dans la collection : Exposés de recherche
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.