About

I am a researcher focused on interactive theorem-proving, formal verification and their automation. Currently, I am an Assistant Professor at Aalborg University. I obtained my BSc in Mathematics at the Benemérita Universidad Autónoma de Puebla (BUAP) in Puebla, México (Thesis: Studying the Foundations of Mathematics comparing some of its Axiomatizations). I later did my PhD with an integrated MSc at the University of Sheffield in Computer Science. My research interests lie in proof assistants: their foundations, automation, and practical applications. I developed a framework for verifying cyber-physical systems in the Isabelle/HOL proof assistant and contributed to the verification of generic, runtime monitoring tools. Then, I was a Marie Curie (MSCA) fellow at the Czech Technical University in Prague, where I developed tools for integrating (2023) generative “AI” with the Isabelle prover. You can see my publications here. I have also worked as a postdoc at the University of Copenhagen, a Data Scientist at Twinkl Educational Publishing, and I have taught logic and Isabelle/HOL in México, England, Norway, and Denmark.

Soy un investigador enfocado en verificación formal y en demostraciones de teoremas con ayuda de computadoras. Actualmente soy “Assistant Professor” en la Universidad de Aalborg. Soy graduado de la Lic. en Matemáticas en la Benemérita Universidad Autónoma de Puebla (Tesis: Estudio en los Fundamentos de las Matemáticas comparando algunas de sus Axiomatizaciones). Realicé mi doctorado con maestría integrada en la Universidad de Sheffield, especializándome en Ciencias de la Computación. Mis intereses yacen alrededor de los asistentes de demostraciones matemáticas en computadora: sus fundamentos, automatización y aplicaciones prácticas. Entre mis contribuciones destacan el desarrollo de un método para verificar sistemas ciberfísicos en la asistente de pruebas Isabelle/HOL y la verificación de herramientas de monitoreo en tiempo de ejecución. Realicé recientemente un proyecto Marie Curie (MSCA) en la Universidad Checa y Técnica de Praga donde desarrollé herramientas que integran “inteligencia artificial” generativa (de 2023) con Isabelle. Puedes ver mi lista de publicaciones aquí. También he trabajado como profesor asistente en la Universidad de Aalborg, postdoc en la Universidad de Copenhague, Data Scientist en Twinkl Educational Publishing y he dado cursos sobre lógica e Isabelle/HOL, en México, Inglaterra, Noruega y Dinamarca.