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)

Formalización de fundaciones de la matemática y compiladores correctos por construcción - Emmanuel Gunther (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)

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)