3.14.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.
• Parametricidad.
• Uso de semántica formal para modelamiento de sistemas.

Objetivos de Aprendizaje (Learning Outcomes):
Elective:

1. Define una semántica formal para un lenguaje pequeño [Usar (Usage)]
2. Escribe un programa en cálculo lambda y muestra su evaluación hacia un forma normal [Usar (Usage)]
3. Discute los diversos enfoques de semánticas operacionales, de notación y axiomáticas [Familiarizarse (Familiarity)]
4. Usa la inducción para demostrar las propiedades de todos los programas de un lenguaje [Usar (Usage)]
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 (Usage)]
6. Usa parametricidad para establecer el comportamiento de un código dado solamente su tipo [Usar (Usage)]
7. Usa semánticas formales para construir un modelo formal de un sistema de software en vez de un lenguaje de programación [Usar (Usage)]