Jul 31: slides “certified software”, primer contact con Coq (primeras definiciones de Basics.v)
Aug 2: Basics.v (ver últimos ejercicios en auxiliar)
Aug 7: Induction.v, Lists.v (hasta antes de options)
Aug 9: Lists.v (final), Poly.v (dejando higher-order/anonymous functions para trabajo casa/auxiliar)
Aug 14: Tactics.v
Aug 16: Logic.v (hasta True)
Aug 21: Logic.v (hasta fun_ext)
Aug 23: Logic.v (clase corta por paro)
Aug 28-30: no hay clases
Sep 4: IndProp.v (hasta regexp - el resto queda para auxiliar)
Sep 6: ProofObjects.v
Sep 11: IndPrinciples.v (rápido) e introducción a programación con tipos dependientes (deptypes.v)
Sep 13: Imp.v (hasta antes de “Evaluation as a Relation”)
<vacaciones 18 / semana olimpica>
Oct 2: Imp.v (hasta ceval_example2)
Oct 5: Imp.v / ImpCEvalFun.v / Extraction.v
Oct 9: feriado
Oct 11: Auto.v / inicio de Equiv.v (definición de nociones de equivalencia)
Oct 16: Equiv.v
Oct 18: Hoare.v (hasta proof rule de SKIP)
Oct 23: Hoare.v
Oct 25: Hoare2.v (hasta Example: Parity)
Oct 30: Hoare2.v
Nov 1: feriado
Nov 6: Smallstep.v (hasta normalizing)
Nov 8: Smallstep.v
Nov 13: Perm.v y Sort.v (libro VFA)
Nov 15: JSCert (M. Bodin)
Nov 20: JSCert (M. Bodin)
Nov 22: Verificación de Programas Probabilísticos (F. Olmedo)