Strong normalization of barrecursive terms without using infinite terms. - Marc Bezem (Arch. Math. Log., 1985)

Isomorphisms Between HEO and HROE, ECF and ICFE. - Marc Bezem (J. Symb. Log., 1985)

Strongly Majorizable Functionals of Finite Type: A Model for Barrecursion Containing Discontinuous Functionals. - Marc Bezem (J. Symb. Log., 1985)

Consistency of Rule-based Expert System. - Marc Bezem (CADE, 1988)

Equivalence of bar recursors in the theory of functionals of finite type. - Marc Bezem (Arch. Math. Log., 1988)

On Estimating the Complexity of Logarithmic Decompositions. - Marc Bezem; Jan van Leeuwen (Inf. Process. Lett., 1988)

Characterizing Termination of Logic Programs with Level Mappings. - Marc Bezem (NACLP, 1989)

Compact and Majorizable Functionals of Finite Type. - Marc Bezem (J. Symb. Log., 1989)

Completeness of Resolution Revisited. - Marc Bezem (Theor. Comput. Sci., 1990)

Semantics and Consistency of Rule-Based Expert Systems. - Marc Bezem (J. Log. Comput., 1991)

Acyclic Programs. - Krzysztof R. Apt; Marc Bezem (New Gener. Comput., 1991)

Strong Termination of Logic Programs. - Marc Bezem (J. Log. Program., 1993)

Invariants in Process Algebra with Data. - Marc Bezem; Jan Friso Groote (CONCUR, 1994)

A Correctness Proof of a One-Bit Sliding Window Protocol in µCRL. - Marc Bezem; Jan Friso Groote (Comput. J., 1994)

Undecidable Goals for Completed Acyclic Programs. - Marc Bezem; Jan Keuzenkamp (New Gener. Comput., 1994)

A realization of the negative interpretation of the Axiom of Choice. - Stefano Berardi; Marc Bezem; Thierry Coquand (TLCA, 1995)

Polymorphic Extensions of Simple Type Structures - With an Application to Bar Recursive Minimization. - Erik Barendsen; Marc Bezem (Ann. Pure Appl. Log., 1996)

A Simple Proof of the Undecidability of Inhabitation in lambdaP. - Marc Bezem; Jan Springintveld (J. Funct. Program., 1996)

Formalizing Process Algebraic Verifications in the Calculus of Constructions. - Marc Bezem; Roland N. Bol; Jan Friso Groote (Formal Aspects Comput., 1997)

Two Finite Specifications of a Queue. - Marc Bezem; Alban Ponse (Theor. Comput. Sci., 1997)

Formulas as Programs - Krzysztof R. Apt; Marc Bezem (CoRR, 1998)

Diagram Techniques for Confluence. - Marc Bezem; Jan Willem Klop; Vincent van Oostrom (Inf. Comput., 1998)

On the Computational Content of the Axiom of Choice. - Stefano Berardi; Marc Bezem; Thierry Coquand (J. Symb. Log., 1998)

Formulas as Programs. - Krzysztof R. Apt; Marc Bezem (The Logic Programming Paradigm, 1999)

Extensionality of Simply Typed Logic Programs. - Marc Bezem (ICLP, 1999)

An Improved Extensionality Criterion for Higher-Order Logic Programs. - Marc Bezem (CSL, 2001)

Automated Proof Construction in Type Theory Using Resolution. - Marc Bezem; Dimitri Hendriks; Hans de Nivelle (J. Autom. Reason., 2002)

Newman's lemma - a case study in proof automation and geometric logic, Logic in Computer Science Column. - Marc Bezem; Thierry Coquand (Bull. EATCS, 2003)

A Type System for the Safe Instantiation of Components. - Marc Bezem; Hoang Truong 001 (FOCLASA, 2003)

A Descriptive Characterisation of Even Linear Languages. - Tore Langholm; Marc Bezem (Grammars, 2003)

Black Box and White Box Identification of Formal Languages Using Test Sets. - Marc Bezem; Christian Sloper; Tore Langholm (Grammars, 2004)

On the Undecidability of Coherent Logic. - Marc Bezem (Processes, Terms and Cycles, 2005)

Finding Resource Bounds in the Presence of Explicit Deallocation. - Hoang Truong 001; Marc Bezem (ICTAC, 2005)

Automating Coherent Logic. - Marc Bezem; Thierry Coquand (LPAR, 2005)

Skolem Machines and Geometric Logic. - John Fisher; Marc Bezem (ICTAC, 2007)

Completeness and Decidability in Sequence Logic. - Marc Bezem; Tore Langholm; Michal Walicki (LPAR, 2007)

Query Completeness of Skolem Machine Computations. - John Fisher; Marc Bezem (MCU, 2007)

The Max-Atom Problem and Its Relevance. - Marc Bezem; Robert Nieuwenhuis; Enric Rodríguez-Carbonell (LPAR, 2008)

Exponential behaviour of the Butkovic-Zimmermann algorithm for solving two-sided linear systems in max-algebra. - Marc Bezem; Robert Nieuwenhuis; Enric Rodríguez-Carbonell (Discret. Appl. Math., 2008)

On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic. - Marc Bezem; Dimitri Hendriks (J. Autom. Reason., 2008)

Skolem Machines. - John Fisher; Marc Bezem (Fundam. Informaticae, 2009)

Developing Bounded Reasoning. - Michal Walicki; Marc Bezem; Wojtek Szajnkenig (J. Log. Lang. Inf., 2009)

Hard problems in max-algebra, control theory, hypergraphs and other areas. - Marc Bezem; Robert Nieuwenhuis; Enric Rodríguez-Carbonell (Inf. Process. Lett., 2010)

A Proof Pearl with the Fan Theorem and Bar Induction - Walking through Infinite Trees with Mixed Induction and Coinduction. - Keiko Nakata 001; Tarmo Uustalu; Marc Bezem (APLAS, 2011)

Expressive power of digraph solvability. - Marc Bezem; Clemens Grabmayer; Michal Walicki (Ann. Pure Appl. Log., 2012)

On streams that are finitely red - Marc Bezem; Keiko Nakata 001; Tarmo Uustalu (Log. Methods Comput. Sci., 2012)

A type system for counting instances of software components. - Marc Bezem; Dag Hovland; Hoang Truong 001 (Theor. Comput. Sci., 2012)

A Model of Type Theory in Cubical Sets. - Marc Bezem; Thierry Coquand; Simon Huber (TYPES, 2013)

A Vernacular for Coherent Logic. - Sana Stojanovic; Julien Narboux; Marc Bezem; Predrag Janicic (CICM, 2014)

Non-Constructivity in Kan Simplicial Sets. - Marc Bezem; Thierry Coquand; Erik Parmann (TLCA, 2015)

A Kripke model for simplicial sets. - Marc Bezem; Thierry Coquand (Theor. Comput. Sci., 2015)

A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic. - Robin Adams 001; Marc Bezem; Thierry Coquand (TYPES, 2016)

Realizability at Work: Separating Two Constructive Notions of Finiteness. - Marc Bezem; Thierry Coquand; Keiko Nakata 001; Erik Parmann (TYPES, 2016)

Improving IntSat by expressing disjunctions of bounds as linear constraints. - Roberto Asín; Marc Bezem; Robert Nieuwenhuis (AI Commun., 2016)

A Strongly Normalizing Computation Rule for Univalence in Higher-Order Minimal Logic. - Robin Adams 001; Marc Bezem; Thierry Coquand (CoRR, 2016)

Construction of the Circle in UniMath. - Marc Bezem; Ulrik Buchholtz; Daniel R. Grayson (CoRR, 2019)

Skolem's Theorem in Coherent Logic. - Marc Bezem; Thierry Coquand (Fundam. Informaticae, 2019)

The Univalence Axiom in Cubical Sets. - Marc Bezem; Thierry Coquand; Simon Huber (J. Autom. Reason., 2019)

A Note on Generalized Algebraic Theories and Categories with Families. - Marc Bezem; Thierry Coquand; Peter Dybjer; Martín Escardó (CoRR, 2020)

On generalized algebraic theories and categories with families. - Marc Bezem; Thierry Coquand; Peter Dybjer; Martín Escardó (Math. Struct. Comput. Sci., 2021)

Type Theory with Explicit Universe Polymorphism. - Marc Bezem; Thierry Coquand; Peter Dybjer; Martín Escardó (TYPES, 2022)

Type Theories with Universe Level Judgements. - Marc Bezem; Thierry Coquand; Peter Dybjer; Martín Escardó (CoRR, 2022)

Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism. - Marc Bezem; Thierry Coquand (Theor. Comput. Sci., 2022)

On symmetries of spheres in univalent foundations. - Pierre Cagne; Ulrik Torben Buchholtz; Nicolai Kraus; Marc Bezem (LICS, 2024)