Academic article

• Marc Bezem; Thierry Coquand; Peter Dybjer et al. (2026). A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism. (external link)
• Robin Adams; Marcus Aloysius Bezem; Thierry Coquand (2016). A Strongly Normalizing Computation Rule for Univalence in Higher-Order Minimal Logic. (external link)
• Michal Walicki; Marcus Aloysius Bezem; Wojciech Szajnkenig (2009). Developing bounded reasoning. (external link)
• Marc Bezem; Thierry Coquand; Peter Dybjer et al. (2023). Type Theory with Explicit Universe Polymorphism. (external link)
• Marc Bezem; Thierry Coquand; Peter Dybjer et al. (2020). A Note on Generalized Algebraic Theories and Categories with Families. (external link)
• Marcus Aloysius Bezem (2005). On the Undecidability of Coherent Logic. (external link)
• Marcus Aloysius Bezem; Thierry Coquand (2003). Newman's Lemma -- a Case Study in Proof Automation and Geometric Logic. (external link)
• Marcus Aloysius Bezem; Dimitri Hendriks; Hans de Nivelle (2003). Automated Proof Construction in Type Theory Using Resolution. (external link)
• Marcus Aloysius Bezem; Anh Hoang Truong (2005). Finding Resource Bounds in the Presence of Explicit Deallocation. (external link)
• Marcus Aloysius Bezem; Thierry Coquand (2005). Automating Coherent Logic. (external link)
• Marcus Aloysius Bezem; Dimitri Hendriks (2008). On the mechanization of the proof of Hessenberg's theorem in coherent logic. (external link)
• Marcus A. Bezem; Dag Hovland; Anh Hoang Truong (2012). A type system for counting instances of software components. (external link)
• Marcus Aloysius Bezem; Thierry Coquand (2019). Skolem’s Theorem in Coherent Logic. (external link)
• Marcus Aloysius Bezem; Clemens Grabmayer; Michal Walicki (2012). Expressive power of digraph solvability. (external link)
• Marcus A. Bezem; Tarmo Uustalu; Keiko Nakata (2012). On streams that are finitely red. (external link)
• Marcus Aloysius Bezem; Anh Hoang Truong (2004). A type system for the safe instantiation of components. (external link)
• Marcus Aloysius Bezem; Thierry Coquand; Simon Huber (2014). A Model of Type Theory in Cubical Sets. (external link)
• Sana Stojanovic; Julien Narboux; Marcus Aloysius Bezem et al. (2014). A vernacular for coherent logic. (external link)
• Roberto Asin; Marcus Aloysius Bezem; Robert Nieuwenhuis (2015). Improving IntSat by expressing disjunctions of bounds as linear constraints. (external link)
• Robin Adams; Marcus Aloysius Bezem; Thierry Coquand (2018). A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic. (external link)
• Marcus Aloysius Bezem; Thierry Coquand; Keiko Nakata et al. (2018). Realizability at Work: Separating Two Constructive Notions of Finiteness. (external link)
• Marcus Aloysius Bezem; Thierry Coquand; Erik Parmann (2015). Non-constructivity in kan simplicial sets. (external link)
• Marcus Aloysius Bezem; Thierry Coquand (2015). A Kripke model for simplicial sets. (external link)
• Marcus Aloysius Bezem; Robert Nieuwenhuis; Enric Rodriguez-Carbonell (2008). Exponential behaviour of the Butkovič–Zimmermann algorithm for solving two-sided linear systems in max-algebra. (external link)
• Marcus Aloysius Bezem; Robert Nieuwenhuis; Enric Rodriguez-Carbonell (2008). The Max-Atom Problem and Its Relevance. (external link)
• Marcus Aloysius Bezem (2010). Euclid's Lemma Revisited. (external link)
• Keiko Nakata; Tarmo Uustalu; Marcus Aloysius Bezem (2011). A Proof Pearl with the Fan Theorem and Bar Induction - Walking through Infinite Trees with Mixed Induction and Coinduction. (external link)
• Marcus Aloysius Bezem; Ulrik Buchholtz; Thierry Coquand (2018). Syntactic forcing models for coherent logic. (external link)
• Marcus Aloysius Bezem; Thierry Coquand; Simon Huber (2018). The univalence axiom in cubical sets. (external link)
• Marcus Aloysius Bezem; Christian Sloper; Tore Langholm (2004). Black Box and White Box Identification of Formal Languages Using Test Sets. (external link)
• Marcus Aloysius Bezem; John, R. Fisher (2007). Query Completeness of Skolem Machine computations. (external link)
• Marcus Aloysius Bezem; Tore Langholm; Michal Walicki (2007). Completeness and Decidability in Sequence Logic. (external link)
• Marcus Aloysius Bezem; John R. Fisher (2007). Skolem Machines and Geometric Logic. (external link)
• Marc Bezem; Thierry Coquand; Peter Dybjer et al. (2021). On generalized algebraic theories and categories with families. (external link)
• Marcus Aloysius Bezem; Robert Nieuwenhuis; Enric Rodriguez-Carbonell (2010). Hard problems in max-algebra, control theory, hypergraphs and other areas. (external link)
• Marc Bezem; Thierry Coquand (2022). Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism. (external link)
• Marc Bezem; Ulrik Buchholtz; Daniel R. Grayson et al. (2021). Construction of the circle in UniMath. (external link)
• Marcus Aloysius Bezem; Ulrik Buchholtz; Thierry Coquand (2017). Syntactic Forcing Models for Coherent Logic. (external link)
• Marcus Aloysius Bezem; Thierry Coquand; Simon Huber (2017). The univalence axiom in cubical sets. (external link)
• John Fisher; Marcus Aloysius Bezem (2009). Skolem Machines. (external link)

Conference lecture

• Marcus Aloysius Bezem (2016). "Elements of Mathematics" in the Digital Age. (external link)
• Michal Walicki; Marcus Aloysius Bezem; Tore Langholm (2007). Sekvenslogikk. (external link)
• Marcus Aloysius Bezem (2016). A taxonomy of mathematical mistakes. (external link)
• Marcus Aloysius Bezem (2016). Coherent Logic – an overview. (external link)
• Marcus Aloysius Bezem; Anh Hoang Truong (2004). Counting instances of software components. (external link)
• Marcus Aloysius Bezem (2008). The Max-Atom Problem and Hypergraphs. (external link)
• Marcus Aloysius Bezem (2008). The Max-Atom Problem. (external link)
• Marcus Aloysius Bezem (2018). The Univalence Axiom in Dependent Type Theory. (external link)
• Marcus Aloysius Bezem (2011). A Hard Problem in Max-Algebra, Control Theory, Hypergraphs and Other Areas. (external link)
• Marcus Aloysius Bezem (2002). Hoapata programs are monotonic. (external link)
• Marcus Aloysius Bezem (2002). An improved extensionality criterion for higher-order logic programs. (external link)
• Marcus Aloysius Bezem (2002). Automating the proof of Newman's Lemma. (external link)
• Marcus Aloysius Bezem (2011). Bar Recursion. (external link)
• Marcus Aloysius Bezem (2011). Constructive Finiteness. (external link)
• Marcus Aloysius Bezem (2002). Automating the proof of Newman's Lemma. (external link)
• Marcus Aloysius Bezem (2014). Coherent Logic and Applications. (external link)
• Marcus Aloysius Bezem (2014). Homotopy Type Theory I. (external link)
• Marcus Aloysius Bezem (2014). Homotopy Type Theory II. (external link)
• Marcus Aloysius Bezem; K.R.A. Apt (2001). Formulas as Programs. (external link)
• Marcus Aloysius Bezem (2009). Automating Coherent Logic - an overview. (external link)
• Marcus Aloysius Bezem (2009). Existence of Shortest Paths in Hypergraphs and other Hard Problems. (external link)
• Marcus Aloysius Bezem (2001). Type Theory. (external link)
• Marcus Aloysius Bezem (2001). An improved extensionality criterion for higher-order logic programs. (external link)
• Marcus Aloysius Bezem (2001). An improved extensionality criterion for higher-order logic programs. (external link)
• Marcus Aloysius Bezem; Michal Walicki (2006). Decidability and Completeness of Sequence Logic. (external link)
• Marcus Aloysius Bezem (2006). Propositional SAT - the search for a model of a given proposition. (external link)
• Marcus Aloysius Bezem (2006). Theory and Practice of Coherent Logic. (external link)
• Marcus Aloysius Bezem (2011). A set that is streamless but not provably Noetherian. (external link)
• Marcus Aloysius Bezem (2011). A set that is streamless but not provably Noetherian. (external link)
• Marcus Aloysius Bezem (2012). A set that is streamless but not provably Noetherian. (external link)
• Marcus Aloysius Bezem (2006). On the mechanization of the proof of Hessenberg's Theorem. (external link)
• Marcus Aloysius Bezem (2013). "Elements of Mathematics" in the Digital Age. (external link)
• Marcus Aloysius Bezem (2013). pplex - A Tool for Teaching the Simplex Method. (external link)
• Marcus Aloysius Bezem (2008). Automating Coherent Logic. (external link)
• Marcus Aloysius Bezem; John R. Fisher (2007). Query Completeness of Skolem Machine Computations. (external link)
• Marcus Aloysius Bezem; Tore Langholm; Michal Walicki (2007). Completeness and Decidability in Sequence Logic. (external link)
• Marcus Aloysius Bezem (2005). Disproving Distributivity in Lattices Using Geometric Logic. (external link)
• Marcus Aloysius Bezem; Huong Anh Truong (2003). A Type System for the Safe Instantiation of Components. (external link)
• Marcus Aloysius Bezem (2003). Newman's Lemma -- a case study in proof automation and geometric logic. (external link)
• Marcus Aloysius Bezem; Huong Anh Truong (2003). A Type System for the Safe Instantiation of Components. (external link)
• Marcus A. Bezem (2012). Elements of Mathematics in the Digital Age. (external link)
• Marcus Aloysius Bezem (2008). The Max-Atom Problem and its Relevance. (external link)

Lecture

• Robin Adams; Marcus Aloysius Bezem; Thierry Coquand (2016). A Strongly Normalizing Computation Rule for the Univalence Axiom in Higher-Order Propositional Logic. (external link)
• Marcus Aloysius Bezem (2018). Homotopy Type Theory and Univalent Foundations. (external link)

Working paper

• Marcus Aloysius Bezem (2001). The Curry-Howard-De Bruijn Correspondence "Propositions as Types". (external link)

Doctoral thesis (PhD)

• Eivind Jahren; Marcus Aloysius Bezem (2018). Three exact methods for some problems in Combinatorial Optimization. (external link)
• Erik Parmann; Marcus Aloysius Bezem (2016). Case Studies in Constructive Mathematics. (external link)

Academic book chapter

• Michal Walicki; Marc Bezem; Wojciech Szajnkenig (2006). A strongly complete logic of dense time intervals. (external link)
• Pierre Cagne; Ulrik Torben Buchholz; Nicolai Kraus et al. (2024). On symmetries of spheres in univalent foundations. (external link)
• Marcus A. Bezem (2013). Platek's system Y: fixed point recursion. (external link)
• Bård Henning Tvedt; Marcus A. Bezem (2012). Towards automated scheduling in the oil industry: modeling safety constraints. (external link)
• Marc Bezem (2003). Mathematical Background. (external link)
• Marcus Aloysius Bezem; Thierry Coquand (2004). Newman's Lemma -- a Case Study in Proof Automation and Geometric Logic. (external link)
• Marc Bezem; Jan Willem Klop; Vincent van Oostrom (2003). Advanced ARS theory. (external link)
• Marc Bezem; Jan Willem Klop (2003). Abstract reduction systems. (external link)
• Marcus Aloysius Bezem; Dimitri Hendriks (2006). On the mechanization of Hessenberg's Theorem. (external link)
• Marcus A. Bezem (2013). Gödel's system T: higher-order primitive recursion. (external link)
• Marcus A. Bezem (2013). Spector's system B: bar recursion. (external link)
• Marcus Aloysius Bezem; Robert Nieuwenhuis (2016). Completeness of Cutting Planes Revisited. (external link)

Book anthology

• Marc Bezem; Assia Mahboubi (2020). 25th International Conference on Types for Proofs and Programs (TYPES 2019). (external link)
• Marc Bezem; Jan Willem Klop; Roel de Vrijer (2003). Term rewriting systems : Terese. (external link)

Master’s thesis

• Eva Burrows; Marcus Aloysius Bezem (2003). Formulas as programs. (external link)

Research report

• Steve Awodey; Marcus A. Bezem; Thierry Coquand et al. (2013). Homotopy Type Theory (www.homotopytypetheory.org/book). (external link)
• Marcus Aloysius Bezem; Wolfgang Ahrendt; Hans De Nivelle et al. (2005). Disproving Distributivity in Lattices Using Geometric Logic. (external link)
• Michal Anton S Walicki; Marcus Aloysius Bezem; Clemens Grabmayer (2010). Expressive power of digraph solvability. (external link)
• Marcus Aloysius Bezem; Niels Van der Weide (2019). Book of Abstracts of TYPES 2019. (external link)

Journal review

• Marcus Aloysius Bezem (2006). Book review of F.~Kamareddine, T.~Laan and R.~Nederpelt, "A Modern Perspective on Type Theory - From its Origins until Today" Applied Logic Series 29, Kluwer Academic Publishers. (external link)

See a complete overview of publications in NVA.