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)

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

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