[S16] Boletín Semanal 5

Stefan Malewski 8 Dec 202308/12/23 at 14:532023-12-08 14:53:08
Boletines

Presentaciones

Les recuerdo que las presentaciones serán el día 21 de diciembre a las 14:00. Por favor empiecen a enviarme sus slides para que les pueda dar algo de feedback!

[S15] Boletín Semanal 7

Stefan Malewski 1 Dec 202301/12/23 at 10:022023-12-01 10:02:01
Boletines

Presentaciones

Recuerden que las presentaciones serán el día 21 de diciembre a las 14:00.
En la presentación deberán demostrar que son capaces de leer, entender, explicar y presentar sobre sistemas formales, por lo que no se aceptarán presentaciones que no incluyan reglas de tipado y reducción.

Cambios

La presentación debe durar como mucho 20 minutos. Una vez finalizada la presentación habrán 10 minutos para preguntas.

Temas

  • WebAssembly (Ismael Correa)
  • Rust (Cristian Carrión)
  • Types and Effects (Francisco Galdames)
  • Gradual Types (David Ibáñez)
  • Implicits (Fabián Díaz)

[S13] Boletín Semanal 3

Stefan Malewski 17 Nov 202317/11/23 at 09:562023-11-17 09:56:17
Boletines

Hitos Evaluativos

Control 4: Tipos existenciales, operadores de tipos y tipos dependientes. | Fecha de entrega: 22 de Noviembre a las 23:59

Temas de la Semana

Plazo recomendando: Jueves 23 de Noviembre

Subtyping y referencias (Capítulo 24)
[Apuntes: Subtyping | Referencias][Videos: Subtyping | Referencias]
  • Principio de subsumption
  • Juicio de subtyping
  • Varianza
  • Problemas con el subtyping en lenguajes funcionales
  • Referencias
  • Store typing
  • Interacción entre referencias y subtyping
Junten dudas para discutirlas en la clase del próximo jueves!!!
Y no olviden usar el discord!

[S12] Boletín Semanal 5

Stefan Malewski 10 Nov 202310/11/23 at 07:272023-11-10 07:27:10
Boletines

Temas de la Semana

Plazo recomendando: Jueves 16 de Noviembre

Operadores de tipos y Tipos dependientes (Capítulo 18)
[Apuntes: Operadores de tipos | Tipos dependientes][Videos: Operadores de tipos | Tipos dependientes | Demo Coq]

  • Términos, tipos y kinds
  • Computación a nivel de tipos
  • Lambda, F y CC omega.
  • Verificación intrínseca vs extrínsica
  • Tipos inductivos en CIC
  • Demostraciones en Coq
  • Tipos inductivos en Coq

Junten dudas para discutirlas en la clase del próximo jueves!!!
Y no olviden usar el discord!

[S11] Boletín Semanal 2

Stefan Malewski 28 Oct 202328/10/23 at 12:542023-10-28 12:54:28

Hitos Evaluativos

Tarea 3: Non-interference. | Fecha de entrega: 29 de Noviembre a las 23:59

Temas de la Semana

Plazo recomendando: Jueves 9 de Noviembre

Tipos existenciales (Capítulo 17)
[Apuntes: Tipos existenciales][Videos: Tipos existenciales]
  • Tipos de datos abstractos
  • Codificando los tipos existenciales en System F
  • Representation independence
  • Bisimulación

Junten dudas para discutirlas en la clase del próximo jueves!!!
Y no olviden usar el discord!

[S10] Boletín Semanal 4

Stefan Malewski 20 Oct 202320/10/23 at 13:122023-10-20 13:12:20
Boletines

Hitos Evaluativos

Control 3: Estructuras finitas y lógica constructiva. | Fecha de entrega: 25 de Octubre a las 23:59

Temas de la Semana

Plazo recomendando: Jueves 26 de Octubre

System F: Lambda cálculo polimórfico (Capítulo 16)
[Apuntes: System F][Videos: System F]
  • System F
  • Church vs Curry style
  • Codificación de tipos en System F
  • Parametricidad
  • Free theorems

Junten dudas para discutirlas en la clase del próximo jueves!!!
Y no olviden usar el discord!

[S09] Boletín Semanal 4

Stefan Malewski 13 Oct 202313/10/23 at 01:392023-10-13 01:39:13
Boletines

Temas de la Semana

Plazo recomendando: Jueves 19 de Octubre

Terminación de STLC y PCF (Capítulo 19)
[Apuntes: Terminación del STLC | PCF][Videos: Terminación del STLC | PCF]
  • Terminación del STLC
  • Relaciones lógicas
  • Demostrando la terminación de STLC usando relaciones lógicas
  • Recursión general con PCF
  • Puntos fijos
  • PCF vs System T

Junten dudas para discutirlas en la clase del próximo jueves!!!
Y no olviden usar el discord!

[S08] Boletín Semanal 5

Stefan Malewski 6 Oct 202306/10/23 at 04:112023-10-06 04:11:06
Boletines

Hitos Evaluativos

Tarea 2: Tipos de seguridad para un lenguaje con lambdas y estructuras finitas. | Fecha de entrega: 25 de Octubre a las 23:59

Temas de la Semana

Plazo recomendando: Jueves 12 de Octubre

Lógica constructiva con proof terms (Capítulos 12.2.2 y 12.4)
[Apuntes: Lógica constructiva con proof terms][Videos: Lógica constructiva con proof terms]
  • Reglas con proof terms
  • Correspondencia entre demostraciones y programas
  • El lambda cube
  • Lógica clásica vs lógica constructiva

Junten dudas para discutirlas en la clase del próximo jueves!!!
Y no olviden usar el discord!

[S07] Boletín Semanal 6

Stefan Malewski 29 Sep 202329/09/23 at 08:582023-09-29 08:58:29
Boletines

Hitos Evaluativos
Control 2: Funciones de órden superior. | Fecha de entrega: 04 de Octubre a las 23:59

Temas de la Semana

Plazo recomendando: Jueves 05 de Octubre

Tipos de datos finitos y lógica constructiva (Capítulo 10 y 11)
[Apuntes: Tipos de datos finitos | Lógica constructiva][Videos: Tipos de datos finitos | Lógica constructiva]
  • Productos nularios y binarios
  • Productos finitos
  • Sumas nularias y binarias
  • Sumas finitas
  • Codificando tipos con sumas y productos
  • Lógica constructiva
  • Lógica clásica vs constructiva
  • Conexión lógica-programación

Junten dudas para discutirlas en la clase del próximo jueves!!!
Y no olviden usar el discord!

[S06] Boletín Semanal 4

Stefan Malewski 21 Sep 202321/09/23 at 22:502023-09-21 22:50:21
Boletines

Temas de la Semana

Plazo recomendando: Jueves 29 de Septiembre

Funciones (Capítulo 9)
[Apuntes: Recursión primitiva][Videos: Recursión primitiva]
  • Recursión priminitva sobre los naturales
  • System T de Gödel
  • Definabilidad
  • Universalidad

Junten dudas para discutirlas en la clase del próximo jueves!!!
Y no olviden usar el discord!