11 citations · 14 across the 5 of their papers we have counts for
7 papers
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…
The formal verification of the ctm approach to forcing
Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf +1
We discuss some highlights of our computer-verified proof of the construction, given a countable transitive set-model of , of generic extensions satisfying $\math…
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…