==== Trail 2017/2 ====
    * 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)

[[teaching:cc7125:Proyectos-2017]]