A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance - Andreas Abel 001; Thierry Coquand; Miguel Pagano (Log. Methods Comput. Sci., 2011)

A Type-Checking Algorithm for Martin-Löf Type Theory with Subtyping Based on Normalisation by Evaluation. - Daniel Fridlender; Miguel Pagano (TLCA, 2013)

A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language. - Leonardo Rodríguez; Daniel Fridlender; Miguel Pagano (TYPES, 2013)

Proving Correctness of a Compiler Using Step-indexed Logical Relations. - Leonardo Rodríguez; Miguel Pagano; Daniel Fridlender (LSFA, 2015)

Pure type systems with explicit substitutions. - Daniel Fridlender; Miguel Pagano (J. Funct. Program., 2015)

Biorthogonality for a Lazy language. - Daniel Fridlender; Alejandro Gadea; Miguel Pagano; Leonardo Rodríguez (IFL, 2017)

The importance of being Extrinsic: Coherence and adequacy for a call-by-value language. - Alejandro Gadea; Emmanuel Gunther; Miguel Pagano (SBLP, 2017)

Formalization of Universal Algebra in Agda. - Emmanuel Gunther; Alejandro Gadea; Miguel Pagano (LSFA, 2017)

An Internalist Approach to Correct-by-Construction Compilers. - Alberto Pardo; Emmanuel Gunther; Miguel Pagano; Marcos Viera (PPDP, 2018)

First Steps Towards a Formalization of Forcing. - Emmanuel Gunther; Miguel Pagano; Pedro Sánchez Terraf (LSFA, 2018)

Mechanization of Separation in Generic Extensions. - Emmanuel Gunther; Miguel Pagano; Pedro Sánchez Terraf (CoRR, 2019)

A formalisation of LEGv8 in Agda. - Santiago Arranz-Olmos; Martín Fernández; Matías Steinberg; Alejandro Gadea; Emmanuel Gunther; Miguel Pagano (SBLP, 2020)

Formalization of Forcing in Isabelle/ZF. - Emmanuel Gunther; Miguel Pagano; Pedro Sánchez Terraf (Arch. Formal Proofs, 2020)

Mechanization of coherence and adequacy: Being extrinsic extended to subtyping. - Alejandro Gadea; Emmanuel Gunther; Miguel Pagano (Sci. Comput. Program., 2020)

Transitive Models of Fragments of ZFC. - Emmanuel Gunther; Miguel Pagano; Pedro Sánchez Terraf; Matías Steinberg (Arch. Formal Proofs, 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)

Nominal Sets in Agda - A Fresh and Immature Mechanization. - Miguel Pagano; José E. Solsona (LSFA, 2022)

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)