Miguel Pagano

Publication Activity (10 Years)

Years Active: 2009-2024
Publications (10 Years): 17

Top Topics

Coloured Petri Nets

Formal Verification

Top Venues

Arch. Formal Proofs

Publications

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