About

Researcher

Department of Computer Science

Czech Technical University in Prague

huertjon @ cvut . cz

Aalborg University

jjhymuni @ cs . aau . dk

I am a researcher focused on interactive theorem-proving and formal verification. Currently, I am a Marie Curie (MSCA) fellow at the Czech Technical University in Prague on a research leave from an assistant professorship 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 around 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. You can see my publications here. I have also worked as a postdoc at the University of Copenhagen, as a Data Scientist at Twinkl Educational Publishing, and 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 tengo un permiso temporal por parte de la Universidad de Aalborg, donde ejerzo como profesor asistente, para realizar un proyecto Marie Curie (MSCA) en la Universidad Checa y Técnica de Praga. 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). Realizé 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 ciber-físicos en la asistente de pruebas Isabelle/HOL y la verificacion de herramientas de monitoreo en tiempo de ejecución. Puedes ver mi lista de publicaciones aquí. También he trabajado como 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.