Miguel Pagano

24 papers C 1Journal 11Unranked 12
YearRankTypeTitle / Venue / Authors
2025 — conf
Dependently Sorted Nominal Signatures.
LFMTP@FSCD
Maribel Fernández, Miguel Pagano, Nora Szasz, Álvaro Tasistro
2024 J jnl
The formal verification of the ctm approach to forcing.
Ann. Pure Appl. Log.
Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf, Matías Steinberg
2022 — conf
Nominal Sets in Agda - A Fresh and Immature Mechanization.
LSFA
Miguel Pagano, José E. Solsona
2022 J jnl
The Independence of the Continuum Hypothesis in Isabelle/ZF.
Arch. Formal Proofs
Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf, Matías Steinberg
2022 J jnl
The formal verification of the ctm approach to forcing.
CoRR
Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf, Matías Steinberg
2022 J jnl
Transitive Models of Fragments of ZFC.
Arch. Formal Proofs
Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf, Matías Steinberg
2020 — conf
A formalisation of LEGv8 in Agda.
SBLP
Santiago Arranz-Olmos, Martín Fernández, Matías Steinberg, Alejandro Gadea, Emmanuel Gunther, Miguel Pagano
2020 — conf
Formalization of Forcing in Isabelle/ZF.
IJCAR (2)
Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf
2020 J jnl
Formalization of Forcing in Isabelle/ZF.
Arch. Formal Proofs
Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf
2020 J jnl
Formalization of Forcing in Isabelle/ZF.
CoRR
Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf
2020 J jnl
Mechanization of coherence and adequacy: Being extrinsic extended to subtyping.
Sci. Comput. Program.
Alejandro Gadea, Emmanuel Gunther, Miguel Pagano
2019 J jnl
Mechanization of Separation in Generic Extensions.
CoRR
Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf
2018 C conf
An Internalist Approach to Correct-by-Construction Compilers.
PPDP
Alberto Pardo, Emmanuel Gunther, Miguel Pagano, Marcos Viera
2018 — conf
First Steps Towards a Formalization of Forcing.
LSFA
Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf
2018 J jnl
First steps towards a formalization of Forcing.
CoRR
Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf
2017 — conf
Biorthogonality for a Lazy language.
IFL
Daniel Fridlender, Alejandro Gadea, Miguel Pagano, Leonardo Rodríguez
2017 — conf
Formalization of Universal Algebra in Agda.
LSFA
Emmanuel Gunther, Alejandro Gadea, Miguel Pagano
2017 — conf
The importance of being Extrinsic: Coherence and adequacy for a call-by-value language.
SBLP
Alejandro Gadea, Emmanuel Gunther, Miguel Pagano
2015 — conf
Proving Correctness of a Compiler Using Step-indexed Logical Relations.
LSFA
Leonardo Rodríguez, Miguel Pagano, Daniel Fridlender
2015 J jnl
Pure type systems with explicit substitutions.
J. Funct. Program.
Daniel Fridlender, Miguel Pagano
2013 — conf
A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language.
TYPES
Leonardo Rodríguez, Daniel Fridlender, Miguel Pagano
2013 — conf
A Type-Checking Algorithm for Martin-Löf Type Theory with Subtyping Based on Normalisation by Evaluation.
TLCA
Daniel Fridlender, Miguel Pagano
2011 J jnl
A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
Log. Methods Comput. Sci.
Andreas Abel, Thierry Coquand, Miguel Pagano
2009 — conf
A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance.
TLCA
Andreas Abel, Thierry Coquand, Miguel Pagano