Nominal sets in Agda : A Fresh and Immature Mechanization

Loading...
Thumbnail Image
Date
2022
Authors
Pagano, Miguel
Solsona, Jose E.
Publisher
DOI
ISSN
ISBN
Abstract
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.
En
Thesis note
Thesis degree name
7 p.
Notes
Incluye bibliografía.
En: The Seventeenth International Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2022) (pp. 87-93). Belo Horizonte, Brazil.
Subject
Type
Article
Access the full text
Citation
Pagano, M., & Solsona, J. E. (2022). Nominal Sets in Agda: A Fresh and Immature Mechanization. Recuperado de https://rad.ort.edu.uy/handle/20.500.11968/6406
View in library
Rights license
Collections