Marc Bezem

Marc Bezem is a Professor of Informatics at the University of Bergen since July 2000. His research spans mathematical logic, type theory, and automated reasoning, with significant contributions to proof theory, homotopy type theory, and logic programming. He has held visiting positions at Carnegie Mellon University and participated in the Univalent Foundations program at the Institute for Advanced Study in Princeton.

• Education: MSc (1981) and PhD (1986) in Mathematics from Utrecht University, supervised by Barendregt/van Dalen and Troelstra/van Dalen, respectively.
• Key Research: Isomorphy of type structures (ECF/ICF^E, HEO/HRO^E), strongly majorizable functionals, computational interpretation of univalence in homotopy type theory, and termination of logic programs.

His work on bar recursion and cubical set semantics has influenced proof theory and type theory, with applications in proof mining and automated verification. He has collaborated extensively with Coquand, Berardi, Groote, and Ponse.

• Honors: Member of the School of Mathematics at the Institute for Advanced Study (2013).
• Leadership Roles: Co-editor of handbooks, editor of Indagationes Mathematicae, President of EACSL (1997-2002), and organizer of international conferences (TLCA, CSL, TYPES).