Titulación DCC

Un argumento central a favor de los tipos refinados es que deberían eliminar chequeos en tiempo de ejecución: si el compilador demuestra estáticamente que un índice está dentro de un rango, no debería ser necesario chequearlo nuevamente al ejecutar el programa. En la práctica, sistemas como LiquidHaskell y Flux no cumplen esta promesa. Al operar como una capa externa de verificación y no estar integrados con el compilador del lenguaje, solo pueden aceptar o rechazar un programa, pero no afectar su ejecución.

Este proyecto propone el diseño e implementación de un lenguaje y su compilador desde cero, en los que los tipos refinados sean parte integral del proceso de compilación. Esto permitirá que la información verificada de forma estática alimente la generación de código, eliminando los chequeos en runtime que ya fueron demostrados estáticamente.