11 citations · 14 across the 5 of their papers we have counts for
6 papers · 1 filter
Dependently Sorted Nominal Signatures
Maribel Fernández, Miguel Pagano, Nora Szasz +1
We investigate an extension of nominal many-sorted signatures in which abstraction has a form of instantiation, called generalised concretion, as elimination operator (similarly to…
Nominal Sets in Agda -- A Fresh and Immature Mechanization
Miguel Pagano, José E. Solsona
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 nomin…
Formalization of Forcing in Isabelle/ZF
Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf
We formalize the theory of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of ZFC, we construct a proper g…
Mechanization of Separation in Generic Extensions
Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf
We mechanize, in the proof assistant Isabelle, a proof of the axiom-scheme of Separation in generic extensions of models of set theory by using the fundamental theorems of forcing.…
First steps towards a formalization of Forcing
Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf
We lay the ground for an Isabelle/ZF formalization of Cohen's technique of forcing. We formalize the definition of forcing notions as preorders with top, dense subsets, and generic…
A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
Andreas Abel, Thierry Coquand, Miguel Pagano
We define a logical framework with singleton types and one universe of small types. We give the semantics using a PER model; it is used for constructing a normalisation-by-evaluati…