Miguel Pagano

According to our database, Miguel Pagano authored at least 18 papers between 2011 and 2024.

Collaborative distances:

• Dijkstra number of five.
• Erdős number of four.

2024

The formal verification of the ctm approach to forcing.

Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf, Matías Steinberg

Ann. Pure Appl. Log., 2024

2022

Nominal Sets in Agda - A Fresh and Immature Mechanization.

Miguel Pagano, José E. Solsona

Proceedings of the Proceedings 17th International Workshop on Logical and Semantic Frameworks with Applications, 2022

The Independence of the Continuum Hypothesis in Isabelle/ZF.

Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf, Matías Steinberg

Arch. Formal Proofs, 2022

Transitive Models of Fragments of ZFC.

Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf, Matías Steinberg

Arch. Formal Proofs, 2022

2020

Mechanization of coherence and adequacy: Being extrinsic extended to subtyping.

Alejandro Gadea, Emmanuel Gunther, Miguel Pagano

Sci. Comput. Program., 2020

Formalization of Forcing in Isabelle/ZF.

Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf

Arch. Formal Proofs, 2020

A formalisation of LEGv8 in Agda.

Santiago Arranz Olmos, Martín Fernández, Matías Steinberg, Alejandro Gadea, Emmanuel Gunther, Miguel Pagano

Proceedings of the SBLP '20: 24th Brazilian Symposium on Programming Languages, 2020

2019

Mechanization of Separation in Generic Extensions.

Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf

CoRR, 2019

2018

First Steps Towards a Formalization of Forcing.

Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf

Proceedings of the 13th Workshop on Logical and Semantic Frameworks with Applications, 2018

An Internalist Approach to Correct-by-Construction Compilers.

Alberto Pardo, Emmanuel Gunther, Miguel Pagano, Marcos Viera

Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, 2018

2017

Formalization of Universal Algebra in Agda.

Emmanuel Gunther, Alejandro Gadea, Miguel Pagano

Proceedings of the 12th Workshop on Logical and Semantic Frameworks, with Applications, 2017

The importance of being Extrinsic: Coherence and adequacy for a call-by-value language.

Alejandro Gadea, Emmanuel Gunther, Miguel Pagano

Proceedings of the 21st Brazilian Symposium on Programming Languages, 2017

Biorthogonality for a Lazy language.

Daniel Fridlender, Alejandro Gadea, Miguel Pagano, Leonardo Rodríguez

Proceedings of the 29th Symposium on Implementation and Application of Functional Programming Languages, 2017

2015

Pure type systems with explicit substitutions.

Daniel Fridlender, Miguel Pagano

J. Funct. Program., 2015

Proving Correctness of a Compiler Using Step-indexed Logical Relations.

Leonardo Rodríguez, Miguel Pagano, Daniel Fridlender

Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications, 2015

2013

A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language.

Leonardo Rodríguez, Daniel Fridlender, Miguel Pagano

Proceedings of the 19th International Conference on Types for Proofs and Programs, 2013

A Type-Checking Algorithm for Martin-Löf Type Theory with Subtyping Based on Normalisation by Evaluation.

Daniel Fridlender, Miguel Pagano

Proceedings of the Typed Lambda Calculi and Applications, 11th International Conference, 2013

2011

A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance

Andreas Abel, Thierry Coquand, Miguel Pagano

Log. Methods Comput. Sci., 2011