Reseña: Coq, a proof assistant based on higher-order intuitionistic type theory
La semana pasada Jean-Pierre Jouannaud hizo una presentación sobre razonamiento automático en el Instituto de estudios avanzados de la Universidad de Tsinghua: Coq, a proof assistant based on higher-order intuitionistic type theory.
En la presentación se incluyen comentarios sobre objetivos y logros del razonamiento formalizado, los fundamentos teóricos de los demostradores, la correspondencia de Curry-Horward, el cálculo de construcciones de Coq y su adecuación.