Home
University of Bergen
Marcus Aloysius Bezem's picture

Marcus Aloysius Bezem

Professor
Department of Informatics
Home Page
  • E-mailMarc.Bezem@uib.no
  • Phone+47 55 58 41 77
  • Visitor Address
    HIB - Thormøhlensgt. 55
  • Postal Address
    Postboks 7803
    5020 Bergen
Academic article
  • Bezem, Marcus Aloysius; Coquand, Thierry. 2019. Skolem’s Theorem in Coherent Logic. Fundamenta Informaticae. 1-14.
  • Bezem, Marcus Aloysius; Coquand, Thierry; Huber, Simon. 2018. The univalence axiom in cubical sets. Journal of automated reasoning. 1-13.
  • Bezem, Marcus Aloysius; Buchholtz, Ulrik; Coquand, Thierry. 2018. Syntactic forcing models for coherent logic. Indagationes mathematicae. 1441-1464.
  • Bezem, Marcus Aloysius; Coquand, Thierry; Nakata, Keiko; Parmann, Erik. 2018. Realizability at Work: Separating Two Constructive Notions of Finiteness. Leibniz International Proceedings in Informatics. 6:1-6:23.
  • Adams, Robin; Bezem, Marcus Aloysius; Coquand, Thierry. 2018. A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic. Leibniz International Proceedings in Informatics. 3:1-3:20.
  • Bezem, Marcus Aloysius; Coquand, Thierry; Huber, Simon. 2017. The univalence axiom in cubical sets. arXiv.org.
  • Bezem, Marcus Aloysius; Buchholtz, Ulrik; Coquand, Thierry. 2017. Syntactic Forcing Models for Coherent Logic. arXiv.org.
  • Adams, Robin; Bezem, Marcus Aloysius; Coquand, Thierry. 2016. A Strongly Normalizing Computation Rule for Univalence in Higher-Order Minimal Logic. arXiv.org.
  • Bezem, Marcus Aloysius; Coquand, Thierry; Parmann, Erik. 2015. Non-constructivity in kan simplicial sets. Leibniz International Proceedings in Informatics. 92-106.
  • Asin, Roberto; Bezem, Marcus Aloysius; Nieuwenhuis, Robert. 2015. Improving IntSat by expressing disjunctions of bounds as linear constraints. AI Communications. 205-209.
  • Bezem, Marcus Aloysius; Coquand, Thierry. 2015. A Kripke model for simplicial sets. Theoretical Computer Science. 86-91.
  • Stojanovic, Sana; Narboux, Julien; Bezem, Marcus Aloysius; Janicic, Predrag. 2014. A vernacular for coherent logic. Lecture Notes in Computer Science (LNCS). 388-403.
  • Bezem, Marcus Aloysius; Coquand, Thierry; Huber, Simon. 2014. A Model of Type Theory in Cubical Sets. Leibniz International Proceedings in Informatics. 107-128.
  • Bezem, Marcus A.; Uustalu, Tarmo; Nakata, Keiko. 2012. On streams that are finitely red. Logical Methods in Computer Science. 1-20.
  • Bezem, Marcus Aloysius; Grabmayer, Clemens; Walicki, Michal. 2012. Expressive power of digraph solvability. Annals of Pure and Applied Logic. 200-213.
  • Bezem, Marcus A.; Hovland, Dag; Truong, Anh Hoang. 2012. A type system for counting instances of software components. Theoretical Computer Science. 29-48.
  • 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. Lecture Notes in Computer Science (LNCS). 353-368.
  • Bezem, Marcus Aloysius; Nieuwenhuis, Robert; Rodriguez-Carbonell, Enric. 2010. Hard problems in max-algebra, control theory, hypergraphs and other areas. Information Processing Letters. 133-138.
  • Bezem, Marcus Aloysius. 2010. Euclid's Lemma Revisited. Normat. 184.
  • Fisher, John; Bezem, Marcus Aloysius. 2009. Skolem Machines. Fundamenta Informaticae. 79-103.
  • Walicki, Michal; Bezem, Marcus Aloysius; Szajnkenig, Wojciech. 2009. Developing bounded reasoning. Journal of Logic, Language and Information. 97-129.
  • Bezem, Marcus Aloysius; Nieuwenhuis, Robert; Rodriguez-Carbonell, Enric. 2008. The Max-Atom Problem and Its Relevance. Lecture Notes in Computer Science (LNCS). 47-61.
  • Bezem, Marcus Aloysius; Hendriks, Dimitri. 2008. On the mechanization of the proof of Hessenberg's theorem in coherent logic. Journal of automated reasoning. 61-85.
  • 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. Discrete Applied Mathematics. 3506-3509.
  • Bezem, Marcus Aloysius; Fisher, John R. 2007. Skolem Machines and Geometric Logic. Lecture Notes in Computer Science (LNCS). 201-215.
  • Bezem, Marcus Aloysius; Fisher, John, R. 2007. Query Completeness of Skolem Machine computations. Lecture Notes in Computer Science (LNCS). 182-192.
  • Bezem, Marcus Aloysius; Langholm, Tore; Walicki, Michal. 2007. Completeness and Decidability in Sequence Logic. Lecture Notes in Computer Science (LNCS). 123-137.
  • Bezem, Marcus Aloysius. 2005. On the Undecidability of Coherent Logic. Lecture Notes in Computer Science (LNCS). 6-13.
  • Bezem, Marcus Aloysius; Truong, Anh Hoang. 2005. Finding Resource Bounds in the Presence of Explicit Deallocation. Lecture Notes in Computer Science (LNCS). 227-241.
  • Bezem, Marcus Aloysius; Coquand, Thierry. 2005. Automating Coherent Logic. Lecture Notes in Computer Science (LNCS). 246-260.
  • Bezem, Marcus Aloysius; Sloper, Christian; Langholm, Tore. 2004. Black Box and White Box Identification of Formal Languages Using Test Sets. Grammars. 111-123.
  • Bezem, Marcus Aloysius; Truong, Anh Hoang. 2004. A type system for the safe instantiation of components. Electronical Notes in Theoretical Computer Science. 197-217.
  • Bezem, Marcus Aloysius; Coquand, Thierry. 2003. Newman's Lemma -- a Case Study in Proof Automation and Geometric Logic. Bulletin of the European Association for Theoretical Computer Science. 86-100.
  • Bezem, Marcus Aloysius; Hendriks, Dimitri; de Nivelle, Hans. 2003. Automated Proof Construction in Type Theory Using Resolution. Journal of automated reasoning. 253-275.
Report
  • Bezem, Marcus Aloysius; Van der Weide, Niels. 2019. Book of Abstracts of TYPES 2019. .
  • Awodey, Steve; Bezem, Marcus A.; Coquand, Thierry; Voevodsky, Vladimir. 2013. Homotopy Type Theory (www.homotopytypetheory.org/book). .
  • Walicki, Michal Anton S; Bezem, Marcus Aloysius; Grabmayer, Clemens. 2010. Expressive power of digraph solvability. .
  • Bezem, Marcus Aloysius; Ahrendt, Wolfgang; De Nivelle, Hans; Baumgartner, Peter. 2005. Disproving Distributivity in Lattices Using Geometric Logic. .
Lecture
  • Adams, Robin; Bezem, Marcus Aloysius; Coquand, Thierry. 2016. A Strongly Normalizing Computation Rule for the Univalence Axiom in Higher-Order Propositional Logic.
Popular scientific lecture
  • Bezem, Marcus Aloysius. 2018. Homotopy Type Theory and Univalent Foundations.
Academic lecture
  • Bezem, Marcus Aloysius. 2018. The Univalence Axiom in Dependent Type Theory .
  • Bezem, Marcus Aloysius. 2016. Coherent Logic – an overview.
  • Bezem, Marcus Aloysius. 2016. A taxonomy of mathematical mistakes.
  • Bezem, Marcus Aloysius. 2016. "Elements of Mathematics" in the Digital Age.
  • Bezem, Marcus Aloysius. 2014. Homotopy Type Theory II.
  • Bezem, Marcus Aloysius. 2014. Homotopy Type Theory I.
  • Bezem, Marcus Aloysius. 2014. Coherent Logic and Applications.
  • Bezem, Marcus Aloysius. 2013. pplex - A Tool for Teaching the Simplex Method.
  • Bezem, Marcus Aloysius. 2013. "Elements of Mathematics" in the Digital Age.
  • Bezem, Marcus A. 2012. Elements of Mathematics in the Digital Age.
  • Bezem, Marcus Aloysius. 2012. A set that is streamless but not provably Noetherian.
  • Bezem, Marcus Aloysius. 2011. Constructive Finiteness.
  • Bezem, Marcus Aloysius. 2011. Bar Recursion.
  • Bezem, Marcus Aloysius. 2011. A set that is streamless but not provably Noetherian.
  • Bezem, Marcus Aloysius. 2011. A set that is streamless but not provably Noetherian.
  • Bezem, Marcus Aloysius. 2011. A Hard Problem in Max-Algebra, Control Theory, Hypergraphs and Other Areas.
  • Bezem, Marcus Aloysius. 2009. Existence of Shortest Paths in Hypergraphs and other Hard Problems.
  • Bezem, Marcus Aloysius. 2009. Automating Coherent Logic - an overview.
  • Bezem, Marcus Aloysius. 2008. The Max-Atom Problem and its Relevance.
  • Bezem, Marcus Aloysius. 2008. The Max-Atom Problem and Hypergraphs.
  • Bezem, Marcus Aloysius. 2008. The Max-Atom Problem.
  • Bezem, Marcus Aloysius. 2008. Automating Coherent Logic.
  • Walicki, Michal; Bezem, Marcus Aloysius; Langholm, Tore. 2007. Sekvenslogikk.
  • Bezem, Marcus Aloysius; Fisher, John R. 2007. Query Completeness of Skolem Machine Computations.
  • Bezem, Marcus Aloysius; Langholm, Tore; Walicki, Michal. 2007. Completeness and Decidability in Sequence Logic.
  • Bezem, Marcus Aloysius. 2006. Theory and Practice of Coherent Logic.
  • Bezem, Marcus Aloysius. 2006. Propositional SAT - the search for a model of a given proposition.
  • Bezem, Marcus Aloysius. 2006. On the mechanization of the proof of Hessenberg's Theorem.
  • Bezem, Marcus Aloysius; Walicki, Michal. 2006. Decidability and Completeness of Sequence Logic.
  • Bezem, Marcus Aloysius. 2005. Disproving Distributivity in Lattices Using Geometric Logic.
  • Bezem, Marcus Aloysius; Truong, Anh Hoang. 2004. Counting instances of software components.
  • Bezem, Marcus Aloysius. 2003. Newman's Lemma -- a case study in proof automation and geometric logic.
  • Bezem, Marcus Aloysius; Truong, Huong Anh. 2003. A Type System for the Safe Instantiation of Components.
  • Bezem, Marcus Aloysius; Truong, Huong Anh. 2003. A Type System for the Safe Instantiation of Components.
  • Bezem, Marcus Aloysius. 2002. Hoapata programs are monotonic.
  • Bezem, Marcus Aloysius. 2002. Automating the proof of Newman's Lemma.
  • Bezem, Marcus Aloysius. 2002. Automating the proof of Newman's Lemma.
  • Bezem, Marcus Aloysius. 2002. An improved extensionality criterion for higher-order logic programs.
  • Bezem, Marcus Aloysius. 2001. Type Theory.
  • Bezem, Marcus Aloysius; Apt, K.R.A. 2001. Formulas as Programs.
  • Bezem, Marcus Aloysius. 2001. An improved extensionality criterion for higher-order logic programs.
  • Bezem, Marcus Aloysius. 2001. An improved extensionality criterion for higher-order logic programs.
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. Bulletin of Symbolic Logic. 296-297.
Compendium
  • Bezem, Marcus Aloysius. 2001. The Curry-Howard-De Bruijn Correspondence "Propositions as Types".
Masters thesis
  • Burrows, Eva. 2003. Formulas as programs.
Doctoral dissertation
  • Jahren, Eivind. 2018. Three exact methods for some problems in Combinatorial Optimization.
  • Parmann, Erik. 2016. Case Studies in Constructive Mathematics.
Academic chapter/article/Conference paper
  • Bezem, Marcus Aloysius; Nieuwenhuis, Robert. 2016. Completeness of Cutting Planes Revisited. 10 pages.
  • Bezem, Marcus A. 2013. Spector's system B: bar recursion. 9 pages.
  • Bezem, Marcus A. 2013. Platek's system Y: fixed point recursion. 3 pages.
  • Bezem, Marcus A. 2013. Gödel's system T: higher-order primitive recursion. 21 pages.
  • Tvedt, Bård Henning; Bezem, Marcus A. 2012. Towards automated scheduling in the oil industry: modeling safety constraints. 6 pages.
  • Bezem, Marcus Aloysius; Hendriks, Dimitri. 2006. On the mechanization of Hessenberg's Theorem.
  • Walicki, Michal; Bezem, Marc; Szajnkenig, Wojciech. 2006. A strongly complete logic of dense time intervals.
  • Bezem, Marcus Aloysius; Coquand, Thierry. 2004. Newman's Lemma -- a Case Study in Proof Automation and Geometric Logic. 16 pages.
  • Bezem, Marcus Aloysius. 2003. Mathematical Background. 36 pages.
  • Bezem, Marcus Aloysius; Klop, Jan Willem; van Oostrom, Vincent. 2003. Advance ARS theory. 32 pages.
  • Bezem, Marcus Aloysius; Klop, Jan Willem. 2003. Abstract reduction systems. 17 pages.

More information in national current research information system (CRIStin)