[[teaching:cc71y|Página del curso]]

^ Fecha ^  Tema  ^Referencia  ^Adicional ^
| M 30 Jul |introducción          |-  |[[http://pleiad.dcc.uchile.cl/papers/2013/tanter-bits2013.pdf|articulo sobre tipos]] |
| L 4 Ago |semántica via sintaxis  |SEwPR Cap 1  |- |
| M 6 Ago |analizar semántica (intro) |SEwPR Cap 2  |- |
|         |intro a PLT Redex   |SEwPR Cap 11  |{{teaching:cc71y:bool1.rkt}} |
| L 11 Ago |analizar semántica |SEwPR Cap 2 |- |
|          |redex-check   |SEwPR Cap 14  |{{teaching:cc71y:bool2.rkt}} |
| M 13 Ago |contextos de evaluación |{{teaching:cc71y:bool3.rkt}}|[[http://www.eecs.northwestern.edu/~robby/lightweight-metatheory/popl2012-kcdeffmrtf.pdf|Run your research!]]|
| L 18 Ago |lambda calculo |SEwPR Cap 3 |{{teaching:cc71y:lc1.rkt}} |
| M 20 Ago |//paro// ||
| L 25 Ago |lambda calculo |SEwPR Cap 3 |{{teaching:cc71y:control1.pdf|control 1}} |
| M 27 Ago |repaso control 1 |||
|          |fin lambda calculo |SEwPR Cap 3 ||
| 1/3 Sep  |//profe en [[http://icfpconference.org/icfp2014/|conferencia]] -- no hay clase//||
| | **tarea**: estudiar el capitulo 3 hasta 3.7 incluido, experimentando con Redex||
| L 8 Sep |ISWIM  |SEwPR Cap 4||
| L 10 Sep |ISWIM: reducción estándar |SEwPR Cap 5||
| 15/17 Sep  |//vacaciones fiestas patrias//||
| L 22 Sep |Errores |SEwPR Cap 8.1-8.2||
| M 24 Sep |Excepciones y continuaciones |SEwPR Cap 8.3-8.5|{{http://users.dcc.uchile.cl/~etanter/courses/cc71y/tarea2.html|Tarea 2}}|
| L 29 Sep |Intro tipos |{{teaching:cc71y:terminology.pdf}}|{{http://lucacardelli.name/papers/typesystems.pdf|Type systems, L. Cardelli}}|
|          |Aritmética con tipos|TAPL Cap 8.1-8.2|{{teaching:cc71y:typed-arithm1.pdf}}|
| M 1 Oct  |Aritmética con tipos: consistencia  |TAPL Cap 8.3 |{{teaching:cc71y:typed-arithm2.pdf}}|
|          | | |{{teaching:cc71y:control2.pdf|control 2}}|
| L 6 Oct  |Lambda calculo con tipos simples:  |TAPL Cap 9.1-9-3 |{{teaching:cc71y:stlc-progress.pdf}}|
|          |definición y progreso | |SEwPR Cap 10 |
| M 8 Oct  |Lambda calculo con tipos simples: preservación |TAPL Cap 9|{{teaching:cc71y:stlc-preservation.pdf}}|
|          | | |{{teaching:cc71y:control3a.pdf|control 3a}}|
| L 13 Oct  |Extensiones simples |TAPL 11.1-11.8|{{teaching:cc71y:extensions.pdf}}|
| M 15 Oct  |Tipos universales|TAPL 23 |{{teaching:cc71y:universals.pdf}}|
| 20/22 Oct  |//profe en [[http://2014.splashcon.org/home|conferencia]] -- no hay clase//|||
| L 27 Oct  |Tipos existenciales |TAPL 24 |{{teaching:cc71y:existentials.pdf}} ||
|           |//Trailer:// subtipos |TAPL 15 |{{teaching:cc71y:subtyping.pdf}} ||
| M 29 Oct  |Tipos graduales |{{teaching:cc71y:gradual.pdf}}|{{teaching:cc71y:siek-gradual.pdf}}|
| L 3 Nov  |Lógica proposicional y deducción natural|{{teaching:cc71y:natded.pdf}}||
|          |Curry-Howard: proposiciones como tipos|{{teaching:cc71y:pap.pdf}}|{{teaching:cc71y:wadler-pat.pdf}}|
| M 5 Nov  |[[http://en.wikipedia.org/wiki/Lambda_cube|Lambda-cube]]|||
|          |Intro a Coq||{{teaching:cc71y:Vectors.v}}|
| 10/12 Nov  |//estudio personal: capítulos Basics, Induction, Lists, Poly, Logic del [[http://www.cis.upenn.edu/~bcpierce/sf/current/index.html|Software Foundations]] //|||
| L 17 Nov  |Interprete de expresiones y máquina de stack en Coq|CPDT 2.1|{{teaching:cc71y:CC71-1.v}}|
| M 19 Nov  |Compilador y demostración de correctitud|CPDT 2.1|{{teaching:cc71y:CC71-2.v}}|
| M 3 Dec | [[teaching:cc71y:2014-2:miniconf|Mini-conferencia]] |||


Referencias:
  * SEwPR: [[http://mitpress.mit.edu/books/semantics-engineering-plt-redex|Semantics Engineering with PLT Redex]] (disponible en biblioteca)
  * TAPL: [[http://www.cis.upenn.edu/~bcpierce/tapl/|Types and Programming Languages]] (disponible en biblioteca)
  * CPDT: [[http://adam.chlipala.net/cpdt/|Certified Programming with Dependent Types]] (disponible en PDF, y biblioteca)