Verificación formal del cálculo ASF en Coq - Torres Ruiz, Mateo Alberto (My University, 2019)
Esta tesis explora un nuevo sistema formal que busca servir de base para establecer un paradigma dentro de los lenguajes de programación capaz de aliviar las tensiones existentes entre el paradigma funcional e imperativo. Dicho sistema, encarnado por el cálculo λSF es aquí expuesto en conjunto con las demostraciones de algunas de sus cualidades más importantes, así como la verificación formal de estas en el sistema Coq.
Exposición del cálculo λSF, demostración de características principales y verificación formal de algunas de ellas.
Keywords: Coq; Lenguajes de programación; Cálculo λ; Cálculo SF; Cálculo λSF