Vitenskapelig Kapittel/Artikkel/Konferanseartikkel
-
Cagne, Pierre; Buchholz, Ulrik Torben; Kraus, Nicolai
et al. (2024). On symmetries of spheres in univalent foundations. (ekstern lenke)
-
Bezem, Marcus Aloysius; Nieuwenhuis, Robert
(2016). Completeness of Cutting Planes Revisited. (ekstern lenke)
-
Bezem, Marcus A.
(2013). Platek's system Y: fixed point recursion. (ekstern lenke)
-
Bezem, Marcus A.
(2013). Gödel's system T: higher-order primitive recursion. (ekstern lenke)
-
Bezem, Marcus A.
(2013). Spector's system B: bar recursion. (ekstern lenke)
-
Tvedt, Bård Henning; Bezem, Marcus A.
(2012). Towards automated scheduling in the oil industry: modeling safety constraints. (ekstern lenke)
-
Walicki, Michal; Bezem, Marc; Szajnkenig, Wojciech
(2006). A strongly complete logic of dense time intervals. (ekstern lenke)
-
Bezem, Marcus Aloysius; Hendriks, Dimitri
(2006). On the mechanization of Hessenberg's Theorem. (ekstern lenke)
-
Bezem, Marcus Aloysius; Coquand, Thierry
(2004). Newman's Lemma -- a Case Study in Proof Automation and Geometric Logic. (ekstern lenke)
-
,
(2003). Mathematical Background. (ekstern lenke)
-
, ; Klop, Jan Willem; Oostrom, Vincent van
(2003). Advanced ARS theory. (ekstern lenke)
-
, ; Klop, Jan Willem
(2003). Abstract reduction systems. (ekstern lenke)
Vitenskapelig artikkel
-
Bezem, Marc; Coquand, Thierry; Dybjer, Peter
et al. (2023). Type Theory with Explicit Universe Polymorphism. (ekstern lenke)
-
Bezem, Marc; Coquand, Thierry
(2022). Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism. (ekstern lenke)
-
Bezem, Marc; Coquand, Thierry; Dybjer, Peter
et al. (2021). On generalized algebraic theories and categories with families. (ekstern lenke)
-
Bezem, Marc; Buchholtz, Ulrik; Grayson, Daniel R.
et al. (2021). Construction of the circle in UniMath. (ekstern lenke)
-
Bezem, Marc; Coquand, Thierry; Dybjer, Peter
et al. (2020). A Note on Generalized Algebraic Theories and Categories with Families. (ekstern lenke)
-
Bezem, Marcus Aloysius; Coquand, Thierry
(2019). Skolem’s Theorem in Coherent Logic. (ekstern lenke)
-
Adams, Robin; Bezem, Marcus Aloysius; Coquand, Thierry
(2018). A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic. (ekstern lenke)
-
Bezem, Marcus Aloysius; Coquand, Thierry; Nakata, Keiko
et al. (2018). Realizability at Work: Separating Two Constructive Notions of Finiteness. (ekstern lenke)
-
Bezem, Marcus Aloysius; Buchholtz, Ulrik; Coquand, Thierry
(2018). Syntactic forcing models for coherent logic. (ekstern lenke)
-
Bezem, Marcus Aloysius; Coquand, Thierry; Huber, Simon
(2018). The univalence axiom in cubical sets. (ekstern lenke)
-
Bezem, Marcus Aloysius; Buchholtz, Ulrik; Coquand, Thierry
(2017). Syntactic Forcing Models for Coherent Logic. (ekstern lenke)
-
Bezem, Marcus Aloysius; Coquand, Thierry; Huber, Simon
(2017). The univalence axiom in cubical sets. (ekstern lenke)
-
Adams, Robin; Bezem, Marcus Aloysius; Coquand, Thierry
(2016). A Strongly Normalizing Computation Rule for Univalence in Higher-Order Minimal Logic. (ekstern lenke)
-
Asin, Roberto; Bezem, Marcus Aloysius; Nieuwenhuis, Robert
(2015). Improving IntSat by expressing disjunctions of bounds as linear constraints. (ekstern lenke)
-
Bezem, Marcus Aloysius; Coquand, Thierry; Parmann, Erik
(2015). Non-constructivity in kan simplicial sets. (ekstern lenke)
-
Bezem, Marcus Aloysius; Coquand, Thierry
(2015). A Kripke model for simplicial sets. (ekstern lenke)
-
Bezem, Marcus Aloysius; Coquand, Thierry; Huber, Simon
(2014). A Model of Type Theory in Cubical Sets. (ekstern lenke)
-
Stojanovic, Sana; Narboux, Julien; Bezem, Marcus Aloysius
et al. (2014). A vernacular for coherent logic. (ekstern lenke)
-
Bezem, Marcus A.; Hovland, Dag; Truong, Anh Hoang
(2012). A type system for counting instances of software components. (ekstern lenke)
-
Bezem, Marcus Aloysius; Grabmayer, Clemens; Walicki, Michal
(2012). Expressive power of digraph solvability. (ekstern lenke)
-
Bezem, Marcus A.; Uustalu, Tarmo; Nakata, Keiko
(2012). On streams that are finitely red. (ekstern lenke)
-
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. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2010). Euclid's Lemma Revisited. (ekstern lenke)
-
Bezem, Marcus Aloysius; Nieuwenhuis, Robert; Rodriguez-Carbonell, Enric
(2010). Hard problems in max-algebra, control theory, hypergraphs and other areas. (ekstern lenke)
-
Walicki, Michal; Bezem, Marcus Aloysius; Szajnkenig, Wojciech
(2009). Developing bounded reasoning. (ekstern lenke)
-
Fisher, John; Bezem, Marcus Aloysius
(2009). Skolem Machines. (ekstern lenke)
-
Bezem, Marcus Aloysius; Hendriks, Dimitri
(2008). On the mechanization of the proof of Hessenberg's theorem in coherent logic. (ekstern lenke)
-
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. (ekstern lenke)
-
Bezem, Marcus Aloysius; Nieuwenhuis, Robert; Rodriguez-Carbonell, Enric
(2008). The Max-Atom Problem and Its Relevance. (ekstern lenke)
-
Bezem, Marcus Aloysius; Fisher, John, R.
(2007). Query Completeness of Skolem Machine computations. (ekstern lenke)
-
Bezem, Marcus Aloysius; Langholm, Tore; Walicki, Michal
(2007). Completeness and Decidability in Sequence Logic. (ekstern lenke)
-
Bezem, Marcus Aloysius; Fisher, John R.
(2007). Skolem Machines and Geometric Logic. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2005). On the Undecidability of Coherent Logic. (ekstern lenke)
-
Bezem, Marcus Aloysius; Truong, Anh Hoang
(2005). Finding Resource Bounds in the Presence of Explicit Deallocation. (ekstern lenke)
-
Bezem, Marcus Aloysius; Coquand, Thierry
(2005). Automating Coherent Logic. (ekstern lenke)
-
Bezem, Marcus Aloysius; Truong, Anh Hoang
(2004). A type system for the safe instantiation of components. (ekstern lenke)
-
Bezem, Marcus Aloysius; Sloper, Christian; Langholm, Tore
(2004). Black Box and White Box Identification of Formal Languages Using Test Sets. (ekstern lenke)
-
Bezem, Marcus Aloysius; Coquand, Thierry
(2003). Newman's Lemma -- a Case Study in Proof Automation and Geometric Logic. (ekstern lenke)
-
Bezem, Marcus Aloysius; Hendriks, Dimitri; Nivelle, Hans de
(2003). Automated Proof Construction in Type Theory Using Resolution. (ekstern lenke)
Vitenskapelig antologi/Konferanseserie
Rapport
-
Bezem, Marcus Aloysius; Weide, Niels Van der
(2019). Book of Abstracts of TYPES 2019. (ekstern lenke)
-
Awodey, Steve; Bezem, Marcus A.; Coquand, Thierry
et al. (2013). Homotopy Type Theory (www.homotopytypetheory.org/book). (ekstern lenke)
-
Walicki, Michal Anton S; Bezem, Marcus Aloysius; Grabmayer, Clemens
(2010). Expressive power of digraph solvability. (ekstern lenke)
-
Bezem, Marcus Aloysius; Ahrendt, Wolfgang; Nivelle, Hans De
et al. (2005). Disproving Distributivity in Lattices Using Geometric Logic. (ekstern lenke)
Doktorgradsavhandling
Faglig foredrag
Vitenskapelig foredrag
-
Bezem, Marcus Aloysius
(2018). The Univalence Axiom in Dependent Type Theory. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2016). "Elements of Mathematics" in the Digital Age. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2016). A taxonomy of mathematical mistakes. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2016). Coherent Logic – an overview. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2014). Coherent Logic and Applications. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2014). Homotopy Type Theory I. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2014). Homotopy Type Theory II. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2013). "Elements of Mathematics" in the Digital Age. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2013). pplex - A Tool for Teaching the Simplex Method. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2012). A set that is streamless but not provably Noetherian. (ekstern lenke)
-
Bezem, Marcus A.
(2012). Elements of Mathematics in the Digital Age. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2011). A Hard Problem in Max-Algebra, Control Theory, Hypergraphs and Other Areas. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2011). Bar Recursion. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2011). Constructive Finiteness. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2011). A set that is streamless but not provably Noetherian. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2011). A set that is streamless but not provably Noetherian. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2009). Automating Coherent Logic - an overview. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2009). Existence of Shortest Paths in Hypergraphs and other Hard Problems. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2008). The Max-Atom Problem and Hypergraphs. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2008). The Max-Atom Problem. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2008). Automating Coherent Logic. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2008). The Max-Atom Problem and its Relevance. (ekstern lenke)
-
Walicki, Michal; Bezem, Marcus Aloysius; Langholm, Tore
(2007). Sekvenslogikk. (ekstern lenke)
-
Bezem, Marcus Aloysius; Fisher, John R.
(2007). Query Completeness of Skolem Machine Computations. (ekstern lenke)
-
Bezem, Marcus Aloysius; Langholm, Tore; Walicki, Michal
(2007). Completeness and Decidability in Sequence Logic. (ekstern lenke)
-
Bezem, Marcus Aloysius; Walicki, Michal
(2006). Decidability and Completeness of Sequence Logic. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2006). Propositional SAT - the search for a model of a given proposition. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2006). Theory and Practice of Coherent Logic. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2006). On the mechanization of the proof of Hessenberg's Theorem. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2005). Disproving Distributivity in Lattices Using Geometric Logic. (ekstern lenke)
-
Bezem, Marcus Aloysius; Truong, Anh Hoang
(2004). Counting instances of software components. (ekstern lenke)
-
Bezem, Marcus Aloysius; Truong, Huong Anh
(2003). A Type System for the Safe Instantiation of Components. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2003). Newman's Lemma -- a case study in proof automation and geometric logic. (ekstern lenke)
-
Bezem, Marcus Aloysius; Truong, Huong Anh
(2003). A Type System for the Safe Instantiation of Components. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2002). Hoapata programs are monotonic. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2002). An improved extensionality criterion for higher-order logic programs. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2002). Automating the proof of Newman's Lemma. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2002). Automating the proof of Newman's Lemma. (ekstern lenke)
-
Bezem, Marcus Aloysius; Apt, K.R.A.
(2001). Formulas as Programs. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2001). Type Theory. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2001). An improved extensionality criterion for higher-order logic programs. (ekstern lenke)
-
Bezem, Marcus Aloysius
(2001). An improved extensionality criterion for higher-order logic programs. (ekstern lenke)
Anmeldelse
Mastergradsoppgave
Kompendium
Se en full oversikt over publikasjoner i Cristin