| A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance M Pagano, T Coquand, A Abel Logical Methods in Computer Science 7, 2011 | 31 | 2011 |
| Formalization of Universal Algebra in Agda E Gunther, A Gadea, M Pagano Electronic Notes in Theoretical Computer Science 338, 147-166, 2018 | 16 | 2018 |
| An Internalist Approach to Correct-by-Construction Compilers A Pardo, E Gunther, M Pagano, M Viera Proceedings of the 20th International Symposium on Principles and Practice …, 2018 | 8 | 2018 |
| Proving Correctness of a Compiler Using Step-indexed Logical Relations L Rodríguez, M Pagano, D Fridlender Electronic Notes in Theoretical Computer Science 323, 197-214, 2016 | 8 | 2016 |
| Formalization of Forcing in Isabelle/ZF E Gunther, M Pagano, PS Terraf International Joint Conference on Automated Reasoning, 221-235, 2020 | 7 | 2020 |
| First steps towards a formalization of Forcing E Gunther, M Pagano, PS Terraf Electronic Notes in Theoretical Computer Science 344, 119-136, 2019 | 7 | 2019 |
| Pure type systems with explicit substitutions D Fridlender, M Pagano Journal of Functional Programming 25, e19, 2015 | 5 | 2015 |
| A type-checking algorithm for Martin-Löf type theory with subtyping based on normalisation by evaluation D Fridlender, M Pagano Typed Lambda Calculi and Applications: 11th International Conference, TLCA …, 2013 | 5 | 2013 |
| The independence of the continuum hypothesis in Isabelle/ZF E Gunther, M Pagano, PS Terraf, M Steinberg Archive of Formal Proofs, 2022 | 3 | 2022 |
| La contrarreforma de la UNC: edX y la mercantilización de la educación superior M Pagano, A Torrano ConCienciaSocial, 2017 | 3 | 2017 |
| The importance of being Extrinsic: Coherence and adequacy for a call-by-value language A Gadea, E Gunther, M Pagano Proceedings of the 21st Brazilian Symposium on Programming Languages, 1-8, 2017 | 3 | 2017 |
| Biorthogonality for a Lazy language D Fridlender, A Gadea, M Pagano, L Rodríguez Proceedings of the 29th Symposium on the Implementation and Application of …, 2017 | 3 | 2017 |
| A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language 19th International Conference on Types for Proofs and Programs (TYPES 2013 …, 2013 | 3* | 2013 |
| Type-Checking and Normalisation By Evaluation for Dependent Type Systems MM Pagano Facultad de Matemática, Astronomía y Física, UNC, 2012 | 3 | 2012 |
| Mechanization of Separation in Generic Extensions E Gunther, M Pagano, PS Terraf arXiv preprint arXiv:1901.03313, 2019 | 2 | 2019 |
| Una reforma neoliberal de la UNC. Mercantilización de educación superior en edXUNCordobaX A Torrano, M Pagano Cuadernos de Coyuntura, 65-71, 2018 | 2 | 2018 |
| Transitive models of fragments of ZFC E Gunther, M Pagano, PS Terraf, M Steinberg Archive of Formal Proofs, 2022 | 1 | 2022 |
| Neoliberalismo real y educación virtual: edX y la UNC A Torrano, M Pagano X Jornadas de Sociología de la Universidad Nacional de La Plata (Ensenada, 5 …, 2018 | 1 | 2018 |
| Proving compiler correctness using step-indexed logical relations L Rodríguez, M Pagano, D Fridlender | 1 | 2016 |
| Nominal Sets in Agda--A Fresh and Immature Mechanization M Pagano, JE Solsona arXiv preprint arXiv:2303.13252, 2023 | | 2023 |
Andreas AbelSenior Lecturer at the Department of Computer Science and Engineering, Gothenburg UniversityVerified email at gu.se
