Temas

• Tema 1: Programación funcional en Isabelle.
• Tema 2a: Razonamiento sobre programas Haskell
• Tema 2b: Razonamiento automático sobre programas en Isabelle/HOL.
• Tema 3: Razonamiento estructurado sobre programas en Isabelle/HOL.
• Tema 4: Razonamiento por casos y por inducción.
• Tema 5a: Verificación de la ordenación por inserción.
• Tema 5b: Verificación de la ordenación por mezcla.
• Tema 6a: Deducción natural proposicional].
• Tema 6b: Deducción natural proposicional con Isabelle/HOL.
• Tema 7a: Deducción natural en lógica de primer orden].
• Tema 7b: Deducción natural en lógica de primer orden con Isabelle/HOL.
• Tema 8: Caso de estudio: Compilación de expresiones.
• Tema 9: Panorama de la demostración asistida por ordenador.

Listas de vídeos de las clases

• [2013-11-27 https://www.youtube.com/watch?v=3ypB3TUmSHg]
• [2013-12-05a https://www.youtube.com/watch?v=yazrdrjlbEU]
• [2013-12-05b https://www.youtube.com/watch?v=jwtk99TIoMo]
• [2013-12-12a https://www.youtube.com/watch?v=1GynGGucKRQ]
• [2013-12-19a https://www.youtube.com/watch?v=cCqwFkDWkqI]
• [2013-12-19b https://www.youtube.com/watch?v=lbhkBjbNh3Y]
• [2014-01-09a https://www.youtube.com/watch?v=WakkA2x8Gs8]
• [2014-01-09b https://www.youtube.com/watch?v=9RgFTM5s-nE]
• [2014-01-16a https://www.youtube.com/watch?v=Xf66W5A7yFw]
• [2014-01-16b https://www.youtube.com/watch?v=VlIjp3eyDR4]
• [2014-01-23a https://www.youtube.com/watch?v=u7_3tW8p4Us]
• [2014-01-23b https://www.youtube.com/watch?v=iu2lRLN_Mo4]
• [2014-01-30a https://www.youtube.com/watch?v=Cf3quG6TkXE]
• [2014-01-30b https://www.youtube.com/watch?v=578loXA_ImI]
• [2014-02-06 https://www.youtube.com/watch?v=fd08GOuiaMM]
• [2014-02-13 https://www.youtube.com/watch?v=IFJtN7tlyuc]