Marc Bezem - Biography#
Marc Bezem obtained a MSc degree (Utrecht University, 1981) in mathematics supervised by Barendregt and van Dalen. He obtained a PhD degree (Utrecht University, 1986) in mathematics under supervision of Troelstra and van Dalen, with a thesis entitled `Bar recursion and functionals of finite type'.
Bezem started his research career by proving two isomorphy results for type structures: ECF is isomorphic to ICF^E and and HEO is isomorphic to HRO^E. The latter isomorphy proves that HEO, being the interpretation of the higher types in Hyland's effective topos, is a PER model. These results have found their way to the standard literature in the recent book Higher-Order Computability by Longley and Normann, Springer, 2015. Another early result was the definition of the strongly majorizable functionals and the proof that they form a model of bar recursion containing discontinuous functionals (against most expectations). The strongly majorizable functionals have been extensively used in proof mining, see the book Applied Proof Theory by Kohlenbach, Springer, 2008.
In the Dutch PhD tradition, a PhD thesis is accompanied by a separate list of theorems (`Stellingen'). One of these was actually an early formulation of a constructive infinite Ramsey theorem (decidable case), which was subsequently generalized together with Veldman. This result has finally been formalized in Nuprl as the lemma `intuitionistic-Ramsey'.
The five-year stay at CWI in Amsterdam, after the PhD-graduation in Utrecht in 1986, came with a widening of the research scope to automated theorem proving and logic programming. Most influential has been Bezem's novel approach to termination of logic programs, introducing the concepts of a recurrent program and a bounded goal, and, together with Krzysztof Apt, the concept of an acyclic program. The total number of citations of these works exceeds 500.
From the CWI, Bezem moved in 1991 to a tenured position at Utrecht University. This brought new collaborations and new research themes, such as process theory with Groote and Ponse. Well-known is also the computational interpretation of the Axiom of Choice, joint work with Berardi and Coquand.
From July 2000, Bezem is professor of computer science at the University of Bergen, Norway. Collaboration with Coquand continued on automated reasoning in coherent logic, and on Coquand's cubical set semantics of type theory with Voevodsky's Univalence Axiom (Huber also made important contributions). While old collaborations continued, resulting in the handbook Term Rewriting Systems, CUP, 2003, new came up during sabbaticals and other research stays abroad. Most relevant has been the participation in the special year on Univalent Foundations of Mathematics, held in 2012/13 at the Institute for Advanced Study in Princeton, as well as the visiting professorship Feb - May 2016 at Carnegie Mellon University in Pittsburgh.
Research activity in recent years is tightly connected to the the computational interpretation of univalence in homotopy type theory. The countermodels developed together with Coquand and Parmann show that Voevodsky's model of MLTT+UA, based on simplicial sets, does not admit a computational interpretation. It turns out that Coquand's model(s) based on cubical sets do validate MLTT+UA, but fail to validate the law of the excluded middle (LEM). Investigations in this area are in full swing (at the time of writing, the status of LEM is still open in one case), and will continue in the project led by Bezem an Dundas (Mathematical Institute, University of Bergen) on Homotopy Type Theory and Univalent Foundations at the Centre for Advanced Study at the Norwegian Academy of Science and Letters. In this project, internationally renowned researchers will collaborate in Oslo during the academic year 2018/19.
Bezem is co-editor and co-author of several handbooks, and editor of Indagationes Mathematicae. Through these and other functions (such as president of the EACSL 97-02 and (co-)organizer of TLCA'93, CSL'96, TYPES and CSL'11, and TYPES 2019 in Oslo), he is very well connected with the international research community.
