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
Journal articles
  • Bezem, Marcus Aloysius; Buchholtz, Ulrik; Coquand, Thierry. 2018. Syntactic forcing models for coherent logic. Indagationes mathematicae. doi: https://doi.org/10.1016/j.indag.2018.06.004
  • Bezem, Marcus Aloysius; Coquand, Thierry; Huber, Simon. 2018. The univalence axiom in cubical sets. Journal of automated reasoning. 1-13. doi: 10.1007/s10817-018-9472-6
  • Bezem, Marcus Aloysius; Buchholtz, Ulrik; Coquand, Thierry. 2017. Syntactic Forcing Models for Coherent Logic. arXiv.org. Technical University.
  • Bezem, Marcus Aloysius; Coquand, Thierry; Huber, Simon. 2017. The univalence axiom in cubical sets. arXiv.org.
  • Adams, Robin; Bezem, Marcus Aloysius; Coquand, Thierry. 2016. A Strongly Normalizing Computation Rule for Univalence in Higher-Order Minimal Logic. arXiv.org.
  • Asin, Roberto; Bezem, Marcus Aloysius; Nieuwenhuis, Robert. 2015. Improving IntSat by expressing disjunctions of bounds as linear constraints. AI Communications. 29: 205-209. doi: 10.3233/AIC-150684
  • Bezem, Marcus Aloysius; Coquand, Thierry. 2015. A Kripke model for simplicial sets. Theoretical Computer Science. 574: 86-91. doi: 10.1016/j.tcs.2015.01.035
  • Bezem, Marcus Aloysius; Coquand, Thierry; Parmann, Erik. 2015. Non-constructivity in kan simplicial sets. Leibniz International Proceedings in Informatics. 38: 92-106. doi: 10.4230/LIPIcs.TLCA.2015.92
  • Bezem, Marcus Aloysius; Coquand, Thierry; Huber, Simon. 2014. A Model of Type Theory in Cubical Sets. Leibniz International Proceedings in Informatics. 26: 107-128. doi: 10.4230/LIPIcs.TYPES.2013.107
  • Stojanovic, Sana; Narboux, Julien; Bezem, Marcus Aloysius; Janicic, Predrag. 2014. A vernacular for coherent logic. Lecture Notes in Computer Science. 8543 LNAI: 388-403. doi: 10.1007/978-3-319-08434-3_28
  • Bezem, Marcus A.; Hovland, Dag; Truong, Anh Hoang. 2012. A type system for counting instances of software components. Theoretical Computer Science. 458: 29-48. doi: 10.1016/j.tcs.2012.07.032
  • Bezem, Marcus A.; Uustalu, Tarmo; Nakata, Keiko. 2012. On streams that are finitely red. Logical Methods in Computer Science. 8: 1-20. doi: 10.2168/LMCS-8(4:4)2012
  • Bezem, Marcus Aloysius; Grabmayer, Clemens; Walicki, Michal. 2012. Expressive power of digraph solvability. Annals of Pure and Applied Logic. 163: 200-213. doi: 10.1016/j.apal.2011.08.004
  • 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. 7078: 353-368.
  • Bezem, Marcus Aloysius. 2010. Euclid's Lemma Revisited. Normat. 58: 184.
  • Bezem, Marcus Aloysius; Nieuwenhuis, Robert; Rodriguez-Carbonell, Enric. 2010. Hard problems in max-algebra, control theory, hypergraphs and other areas. Information Processing Letters. 110: 133-138. doi: 10.1016/j.ipl.2009.11.007
  • Fisher, John; Bezem, Marcus Aloysius. 2009. Skolem Machines. Fundamenta Informaticae. 91: 79-103. doi: 10.3233/FI-2009-0034
  • Walicki, Michal; Bezem, Marcus Aloysius; Szajnkenig, Wojciech. 2009. Developing bounded reasoning. Journal of Logic, Language and Information. 18: 97-129. doi: 10.1007/s10849-008-9070-9
  • Bezem, Marcus Aloysius; Hendriks, Dimitri. 2008. On the mechanization of the proof of Hessenberg's theorem in coherent logic. Journal of automated reasoning. 40: 61-85. doi: 10.1007/s10817-007-9086-x
  • Bezem, Marcus Aloysius; Nieuwenhuis, Robert; Rodriguez-Carbonell, Enric. 2008. The Max-Atom Problem and Its Relevance. Lecture Notes in Computer Science. 5330: 47-61.
  • 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. 156: 3506-3509. doi: 10.1016/j.dam.2008.03.016
  • Bezem, Marcus Aloysius; Fisher, John R. 2007. Skolem Machines and Geometric Logic. Lecture Notes in Computer Science. 4711: 201-215.
  • Bezem, Marcus Aloysius; Fisher, John, R. 2007. Query Completeness of Skolem Machine computations. Lecture Notes in Computer Science. 4664: 182-192.
  • Bezem, Marcus Aloysius; Langholm, Tore; Walicki, Michal. 2007. Completeness and Decidability in Sequence Logic. Lecture Notes in Computer Science. 4790: 123-137.
  • 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. 12: 296-297.
  • Bezem, Marcus Aloysius. 2005. On the Undecidability of Coherent Logic. Lecture Notes in Computer Science. 3838: 6-13.
  • Bezem, Marcus Aloysius; Coquand, Thierry. 2005. Automating Coherent Logic. Lecture Notes in Computer Science. 3835: 246-260.
  • Bezem, Marcus Aloysius; Truong, Anh Hoang. 2005. Finding Resource Bounds in the Presence of Explicit Deallocation. Lecture Notes in Computer Science. 3722: 227-241.
  • Bezem, Marcus Aloysius; Sloper, Christian; Langholm, Tore. 2004. Black Box and White Box Identification of Formal Languages Using Test Sets. Grammars. 7: 111-123.
  • Bezem, Marcus Aloysius; Truong, Anh Hoang. 2004. A type system for the safe instantiation of components. Electronical Notes in Theoretical Computer Science. 97: 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. 79: 86-100.
  • Bezem, Marcus Aloysius; Hendriks, Dimitri; de Nivelle, Hans. 2003. Automated Proof Construction in Type Theory Using Resolution. Journal of automated reasoning. 29: 253-275.
Reports and theses
  • Awodey, Steve; Bezem, Marcus A.; Coquand, Thierry; Voevodsky, Vladimir. 2013. Homotopy Type Theory (www.homotopytypetheory.org/book). The Univalent Foundations Program (IAS),, Princeton.
  • Walicki, Michal Anton S; Bezem, Marcus Aloysius; Grabmayer, Clemens. 2010. Expressive power of digraph solvability. Utrecht University. 23 pages.
  • Bezem, Marcus Aloysius; Ahrendt, Wolfgang; De Nivelle, Hans; Baumgartner, Peter. 2005. Disproving Distributivity in Lattices Using Geometric Logic. CADE-20, Tallinn. 7 pages.
  • Bezem, Marcus Aloysius. 2001. The Curry-Howard-De Bruijn Correspondence "Propositions as Types". BRICS, Aarhus. 12 pages.
Book sections
  • Bezem, Marcus Aloysius; Nieuwenhuis, Robert. 2016. Completeness of Cutting Planes Revisited. Article 5, pages 37-46. In:
    • van Eijck, Jan. 2016. Liber Amicorum Alberti. a Tribute to Albert Visser. College Publications. 236 pages. ISBN: 978-1848902046.
  • Bezem, Marcus A. 2013. Platek's system Y: fixed point recursion. 5.5, pages 312-314. In:
    • Barendregt, Henk; Dekkers, Wil; Statman, Richard. 2013. Lambda calculus with types. Cambridge University Press. 833 pages. ISBN: 978-0-521-76614-2.
  • Bezem, Marcus A. 2013. Spector's system B: bar recursion. 5.4, pages 303-311. In:
    • Barendregt, Henk; Dekkers, Wil; Statman, Richard. 2013. Lambda calculus with types. Cambridge University Press. 833 pages. ISBN: 978-0-521-76614-2.
  • Bezem, Marcus A. 2013. Gödel's system T: higher-order primitive recursion. 5.3, pages 282-302. In:
    • Barendregt, Henk; Dekkers, Wil; Statman, Richard. 2013. Lambda calculus with types. Cambridge University Press. 833 pages. ISBN: 978-0-521-76614-2.
  • Tvedt, Bård Henning; Bezem, Marcus A. 2012. Towards automated scheduling in the oil industry: modeling safety constraints. Paper ICA4423, pages 1-6. In:
    • Arabnia, Hamid R. 2012. Proceedings of the 2012 International Conference on Artificial Intelligence. CSREA Press. ISBN: 1-60132-203-8.
  • Bezem, Marcus Aloysius; Hendriks, Dimitri. 2006. On the mechanization of Hessenberg's Theorem. Extended Abstract 17, pages 160-181. In:
    • Botana, Francisco; Roanes-Lozano, Eugenio. 2006. Automated Deduction in Geometry 2006. 212 pages. ISBN: 84-611-2355-7.
  • Walicki, Michal; Bezem, Marc; Szajnkenig, Wojciech. 2006. A strongly complete logic of dense time intervals. 11, pages 124-135. In:
    • Ågotnes, Thomas; Alechina, Natasha. 2006. Proceedings of the Workshop on Logics for Resource-Bounded Agents (LRBA 06). ESSLLI, Malaga, Spain. 135 pages.
  • Bezem, Marcus Aloysius; Coquand, Thierry. 2004. Newman's Lemma -- a Case Study in Proof Automation and Geometric Logic. 2, pages 267-282. In:
    • Paun, Gheorghe; Salomaa, A; Rozenberg, G. 2004. Current trends in Theoretical Computer Science. World Scientific. 628 pages. ISBN: 981-238-965-2.
  • Bezem, Marcus Aloysius. 2003. Mathematical Background. 790-825. In:
    • 2003. Term Rewriting Systems. Cambridge University Press. ISBN: 0521391156.
  • Bezem, Marcus Aloysius; Klop, Jan Willem. 2003. Abstract reduction systems. 7-23. In:
    • 2003. Term Rewriting Systems. Cambridge University Press. ISBN: 0521391156.
  • Bezem, Marcus Aloysius; Klop, Jan Willem; van Oostrom, Vincent. 2003. Advance ARS theory. 744-775. In:
    • 2003. Term Rewriting Systems. Cambridge University Press. ISBN: 0521391156.

More information in national current research information system (CRIStin)