Repository logo
Repository logo
Universidad ORT Uruguay
Repository logo
  • English
  • Español
  • Português do Brasil
  1. Home
  2. Browse by Author

Browsing by Author "Solsona, Jose E."

Now showing 1 - 1 of 1
Results Per Page
Sort Options
  • Loading...
    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.

Somos parte de:

Logo Silo
Logo La Referencia
Campus Centro
Cuareim 1451, Montevideo, Uruguay

Teléfono central: (598) 2902 1505
Campus Pocitos
Bvar. España 2633, Montevideo, Uruguay