2.13.15 PL/Semántica formal

Temas:
Electivo

• Sintáxis vs. semántica.
• Cálculo Lambda.
• Enfóques a semántica:Operacional, Denotativo, Axiomático.
• Demostración por inducción sobre lenguajes semánticos.
• Definición formal y demostración para sistemas de tipo.
  Ref: Sistemas de tipos
• Parametricidad.
  Ref: Sistemas de tipos
• Uso de semántica formal para modelamiento de sistemas.

Objetivos de Aprendizaje:
Elective:

1. Define una semántica formal para un lenguaje pequeño [Usar]
2. Escribe un programa en cálculo lambda y muestra su evaluación hacia un forma normal [Usar]
3. Discute los diversos enfoques de semánticas operacionales, de notación y axiomáticas [Familiarizarse]
4. Usa la inducción para demostrar las propiedades de todos los programas de un lenguaje [Usar]
5. Usa inducción para demostrar las propiedades de todos los programas de un lenguaje que es bien tipado de acuerdo a un sistema formalmente definido de tipos [Usar]
6. Usa parametricidad para establecer el comportamiento de un código dado solamente su tipo [Usar]
7. Usa semánticas formales para construir un modelo formal de un sistema de software en vez de un lenguaje de programación [Usar]