# Marc Bezem

Professor
• E-mailMarc.Bezem@uib.no
• Phone+47 55 58 41 77
HIB - Thormøhlens gate 55
5006 Bergen
Postboks 7803
5020 Bergen
• Show author(s) (2022). Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism. Theoretical Computer Science. 1-7.
• Show author(s) (2021). On Generalized Algebraic Theories and Categories with Families. Mathematical Structures in Computer Science. 1-18.
• Show author(s) (2021). Construction of the circle in UniMath. Journal of Pure and Applied Algebra. 21 pages.
• Show author(s) (2020). A Note on Generalized Algebraic Theories and Categories with Families. arXiv.org.
• Show author(s) (2019). Skolem’s Theorem in Coherent Logic. Fundamenta Informaticae. 1-14.
• Show author(s) (2018). The univalence axiom in cubical sets. Journal of automated reasoning. 1-13.
• Show author(s) (2018). Syntactic forcing models for coherent logic. Indagationes mathematicae. 1441-1464.
• Show author(s) (2018). Realizability at Work: Separating Two Constructive Notions of Finiteness. Leibniz International Proceedings in Informatics. 6:1-6:23.
• Show author(s) (2018). A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic. Leibniz International Proceedings in Informatics. 3:1-3:20.
• Show author(s) (2017). The univalence axiom in cubical sets. arXiv.org.
• Show author(s) (2017). Syntactic Forcing Models for Coherent Logic. arXiv.org.
• Show author(s) (2016). A Strongly Normalizing Computation Rule for Univalence in Higher-Order Minimal Logic. arXiv.org.
• Show author(s) (2015). Non-constructivity in kan simplicial sets. Leibniz International Proceedings in Informatics. 92-106.
• Show author(s) (2015). Improving IntSat by expressing disjunctions of bounds as linear constraints. AI Communications. 205-209.
• Show author(s) (2015). A Kripke model for simplicial sets. Theoretical Computer Science. 86-91.
• Show author(s) (2014). A vernacular for coherent logic. Lecture Notes in Computer Science (LNCS). 388-403.
• Show author(s) (2014). A Model of Type Theory in Cubical Sets. Leibniz International Proceedings in Informatics. 107-128.
• Show author(s) (2012). On streams that are finitely red. Logical Methods in Computer Science. 1-20.
• Show author(s) (2012). Expressive power of digraph solvability. Annals of Pure and Applied Logic. 200-213.
• Show author(s) (2012). A type system for counting instances of software components. Theoretical Computer Science. 29-48.
• Show author(s) (2011). A Proof Pearl with the Fan Theorem and Bar Induction - Walking through Infinite Trees with Mixed Induction and Coinduction. Lecture Notes in Computer Science (LNCS). 353-368.
• Show author(s) (2010). Hard problems in max-algebra, control theory, hypergraphs and other areas. Information Processing Letters. 133-138.
• Show author(s) (2010). Euclid's Lemma Revisited. Normat. 184.
• Show author(s) (2009). Skolem Machines. Fundamenta Informaticae. 79-103.
• Show author(s) (2009). Developing bounded reasoning. Journal of Logic, Language and Information. 97-129.
• Show author(s) (2008). The Max-Atom Problem and Its Relevance. Lecture Notes in Computer Science (LNCS). 47-61.
• Show author(s) (2008). On the mechanization of the proof of Hessenberg's theorem in coherent logic. Journal of automated reasoning. 61-85.
• Show author(s) (2008). Exponential behaviour of the Butkovič–Zimmermann algorithm for solving two-sided linear systems in max-algebra. Discrete Applied Mathematics. 3506-3509.
• Show author(s) (2007). Skolem Machines and Geometric Logic. Lecture Notes in Computer Science (LNCS). 201-215.
• Show author(s) (2007). Query Completeness of Skolem Machine computations. Lecture Notes in Computer Science (LNCS). 182-192.
• Show author(s) (2007). Completeness and Decidability in Sequence Logic. Lecture Notes in Computer Science (LNCS). 123-137.
• Show author(s) (2005). On the Undecidability of Coherent Logic. Lecture Notes in Computer Science (LNCS). 6-13.
• Show author(s) (2005). Finding Resource Bounds in the Presence of Explicit Deallocation. Lecture Notes in Computer Science (LNCS). 227-241.
• Show author(s) (2005). Automating Coherent Logic. Lecture Notes in Computer Science (LNCS). 246-260.
• Show author(s) (2004). Black Box and White Box Identification of Formal Languages Using Test Sets. Grammars. 111-123.
• Show author(s) (2004). A type system for the safe instantiation of components. Electronical Notes in Theoretical Computer Science. 197-217.
• Show author(s) (2003). Newman's Lemma -- a Case Study in Proof Automation and Geometric Logic. Bulletin of the European Association for Theoretical Computer Science. 86-100.
• Show author(s) (2003). Automated Proof Construction in Type Theory Using Resolution. Journal of automated reasoning. 253-275.
Report
• Show author(s) (2019). Book of Abstracts of TYPES 2019. .
• Show author(s) (2013). Homotopy Type Theory (www.homotopytypetheory.org/book). .
• Show author(s) (2010). Expressive power of digraph solvability. .
• Show author(s) (2005). Disproving Distributivity in Lattices Using Geometric Logic. .
Lecture
• Show author(s) (2016). A Strongly Normalizing Computation Rule for the Univalence Axiom in Higher-Order Propositional Logic.
Popular scientific lecture
• Show author(s) (2018). Homotopy Type Theory and Univalent Foundations.
• Show author(s) (2018). The Univalence Axiom in Dependent Type Theory .
• Show author(s) (2016). Coherent Logic – an overview.
• Show author(s) (2016). A taxonomy of mathematical mistakes.
• Show author(s) (2016). "Elements of Mathematics" in the Digital Age.
• Show author(s) (2014). Homotopy Type Theory II.
• Show author(s) (2014). Homotopy Type Theory I.
• Show author(s) (2014). Coherent Logic and Applications.
• Show author(s) (2013). pplex - A Tool for Teaching the Simplex Method.
• Show author(s) (2013). "Elements of Mathematics" in the Digital Age.
• Show author(s) (2012). Elements of Mathematics in the Digital Age.
• Show author(s) (2012). A set that is streamless but not provably Noetherian.
• Show author(s) (2011). Constructive Finiteness.
• Show author(s) (2011). Bar Recursion.
• Show author(s) (2011). A set that is streamless but not provably Noetherian.
• Show author(s) (2011). A set that is streamless but not provably Noetherian.
• Show author(s) (2011). A Hard Problem in Max-Algebra, Control Theory, Hypergraphs and Other Areas.
• Show author(s) (2009). Existence of Shortest Paths in Hypergraphs and other Hard Problems.
• Show author(s) (2009). Automating Coherent Logic - an overview.
• Show author(s) (2008). The Max-Atom Problem and its Relevance.
• Show author(s) (2008). The Max-Atom Problem and Hypergraphs.
• Show author(s) (2008). The Max-Atom Problem.
• Show author(s) (2008). Automating Coherent Logic.
• Show author(s) (2007). Sekvenslogikk.
• Show author(s) (2007). Query Completeness of Skolem Machine Computations.
• Show author(s) (2007). Completeness and Decidability in Sequence Logic.
• Show author(s) (2006). Theory and Practice of Coherent Logic.
• Show author(s) (2006). Propositional SAT - the search for a model of a given proposition.
• Show author(s) (2006). On the mechanization of the proof of Hessenberg's Theorem.
• Show author(s) (2006). Decidability and Completeness of Sequence Logic.
• Show author(s) (2005). Disproving Distributivity in Lattices Using Geometric Logic.
• Show author(s) (2004). Counting instances of software components.
• Show author(s) (2003). Newman's Lemma -- a case study in proof automation and geometric logic.
• Show author(s) (2003). A Type System for the Safe Instantiation of Components.
• Show author(s) (2003). A Type System for the Safe Instantiation of Components.
• Show author(s) (2002). Hoapata programs are monotonic.
• Show author(s) (2002). Automating the proof of Newman's Lemma.
• Show author(s) (2002). Automating the proof of Newman's Lemma.
• Show author(s) (2002). An improved extensionality criterion for higher-order logic programs.
• Show author(s) (2001). Type Theory.
• Show author(s) (2001). Formulas as Programs.
• Show author(s) (2001). An improved extensionality criterion for higher-order logic programs.
• Show author(s) (2001). An improved extensionality criterion for higher-order logic programs.
Book review
• Show author(s) (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. Bulletin of Symbolic Logic. 296-297.
• Show author(s) (2020). 25th International Conference on Types for Proofs and Programs (TYPES 2019). Schloss Dagstuhl – Leibniz-Zentrum für Informatik GmbH .
Compendium
• Show author(s) (2001). The Curry-Howard-De Bruijn Correspondence "Propositions as Types".
Masters thesis
• Show author(s) (2003). Formulas as programs.
Doctoral dissertation
• Show author(s) (2018). Three exact methods for some problems in Combinatorial Optimization.
• Show author(s) (2016). Case Studies in Constructive Mathematics.