2.5.23 FPL/Semántica Formal

Temas:
Non Core

• Sintaxis vs semántica
• Enfoques de semántica: axiomática, operacional, denotacional, basada en tipos
• Semántica axiomática de construcciones abstractas como asignación, selección, iteración usando precondición, postcondiciones e invariante de bucle
• Análisis de semántica operacional de construcciones abstractas y secuencia de tales como asignación, evaluación de expresión, selección, iteración usando entorno y almacén:
  1. Ejecución simbólica (symbolic execution)
  2. Verificadores de restricciones (constraint checkers)
• Semántica denotacional:
  1. Cálculo Lambda.
• Demostraciones por inducción sobre la semántica del lenguaje
• Definiciones y demostraciones formales para sistemas de tipos:
  1. Proposiciones como tipos (implicación como función, conjunción como producto, disyunción como suma)
  2. Tipos dependientes (cuantificación universal como función dependiente, cuantificación existencial como producto dependiente)
  3. Parametricidad

Aprendizaje esperado (Learning Outcomes):
NonCore:

1. Construir semántica formal para un lenguaje pequeño [Crear]
2. Escribir un programa de cálculo lambda y mostrar su evaluación a una forma normal [Escribir]
3. Discutir los diferentes enfoques de la semántica operacional, denotacional y axiomática [Debatir]
4. Usar inducción para demostrar propiedades de todos los programas en un lenguaje [Usar]
5. Usar inducción para demostrar propiedades de todos los programas en un lenguaje que está bien tipado según un sistema de tipos definido formalmente [Usar]
6. Usar parametricidad para establecer el comportamiento del código dado solo su tipo [Usar]