Browsing by Author "Pagano, Miguel"

Now showing 1 - 3 of 3
  • Thumbnail Image
    Item
    A machine-checked proof of the Standardization Theorem in Lambda Calculus using multiple substitution
    (Universidad ORT Uruguay, 2018) Copes Sabaj, Martín; Tasistro Souto, Álvaro Daniel; Szasz Cerutti, Nora Adriana; Betarte Guidi, Gustavo Romulo; Pagano, Miguel
    En el siguiente trabajo se presenta la formalización en Agda del Teorema de Estandarización para el Cálculo Lambda. Se presenta un corolario del Teorema de Estandarización junto con la demostración del teorema de reducción más izquierdista (leftmost reduction). Si bien existen formalizaciones de estos resultados, lo innovador que se desarrolla en la presente tesis, consiste en el apego de la formalización del Cálculo Lambda a su presentación usual (variables con nombres). El Cálculo Lambda constituye el fundamento teórico de lenguajes de programación funcionales. En la primera parte de este trabajo se reseña la formalización del Cálculo Lambda que se utiliza como base para el desarrollo de los capítulos siguientes e introduce ciertas definiciones propias. En el tercer capítulo se presenta lo más sustancial de la tesis: las definiciones de diferentes nociones de reducción que permiten probar el Teorema de Estandarización que será en términos de una secuencia de reducción estándar. Primero se presentan las nociones de contracción del redex más izquierdista y luego la noción de reducción del redex en la cabecera (de una aplicación). Se demuestra una definición inductiva equivalente a secuencias de reducción estándar. En este capítulo se van desplegando los lemas necesarios para obtener el teorema de estandarización. En el cuarto capítulo de la tesis se aprovecha el Teorema de Estandarización para probar que si un término tiene forma normal, esta es alcanzable por la estrategia de reducción leftmost-outermost. Concluye con la comparación de este desarrollo con otras formalizaciones del mismo resultado y propone algunas líneas para continuarlo.
  • Thumbnail Image
    Item
    Nominal sets in Agda
    (2022) Pagano, Miguel; Solsona, Jose E.
    In this paper we present our current development on a new formalization of nominal sets in Agda. Our first motivation in having another formalization was to understand better nominal sets and to have a playground for testing type systems based on nominal logic. Not surprisingly, we have independently built up the same hierarchy of types leading to nominal sets. We diverge from other formalizations in how to conceive finite permutations: in our formalization a finite permutation is a permutation (i.e. a bijection) whose domain is finite. Finite permutations have different representations, for instance as compositions of transpositions (the predominant in other formalizations) or compositions of disjoint cycles. We prove that these representations are equivalent and use them to normalize (up to composition order of independent transpositions) compositions of transpositions.
  • Thumbnail Image
    Item
    Normalization Proofs for the Simply-Typed Lambda Calculus in Agda
    (Universidad ORT Uruguay, 2020) Urciuoli Silva, Sebastián; Tasistro Souto, Álvaro Daniel; Szasz Cerutti, Nora Adriana; Fernández, Maribel; Pagano, Miguel
    La siguiente Tesis presenta una formalización en Agda de dos teoremas fundamentales del cálculo lambda: la normalización débil y la normalización fuerte de los términos tipados usando una técnica de prueba propuesta por Joachimski y Matthes. La tesis comienza con una introducción del problema y las técnicas involucradas en la pruebas de normalización; también se presenta la librería de Agda en la que se basa el desarrollo. En los capítulos siguientes se explica de manera amena y se detalla la mecanización de la prueba. El aporte de la tesis consiste en la formalización de una prueba de normalización débil como fuerte. No hay formalizaciones conocidas de la técnica de Joachimski y Matthes. Para completar la prueba, se agrega algunos resultados a la librería en la que se basa el trabajo.