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
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
Lecture
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
Masters thesis
Compendium
See a complete overview of publications in Cristin.