Verificación formal del cálculo ASF en Coq
Loading...
Files
Date
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
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.
Description
Exposición del cálculo λSF, demostración de características principales y verificación formal de algunas de ellas.