Academic chapter/article/Conference paper

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

Academic article

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

Academic anthology/Conference proceedings

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

Report

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

Doctoral dissertation

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

Lecture

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

Academic lecture

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

Book review

• Bezem, Marcus Aloysius (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)

Masters thesis

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

Compendium

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

See a complete overview of publications in Cristin.