Inductive types and exact completion. - Benno van den Berg (Ann. Pure Appl. Log., 2005)

Non-well-founded trees in categories. - Benno van den Berg; Federico De Marchi (Ann. Pure Appl. Log., 2007)

Models of non-well-founded sets via an indexed final coalgebra theorem. - Federico De Marchi; Benno van den Berg (J. Symb. Log., 2007)

Aspects of predicative algebraic set theory I: Exact completion. - Benno van den Berg; Ieke Moerdijk (Ann. Pure Appl. Log., 2008)

Three extensional models of type theory. - Benno van den Berg (Math. Struct. Comput. Sci., 2009)

No-go theorems for functorial localic spectra of noncommutative rings. - Benno van den Berg; Chris Heunen (QPL, 2011)

Aspects of predicative algebraic set theory, II: Realizability. - Benno van den Berg; Ieke Moerdijk (Theor. Comput. Sci., 2011)

Noncommutativity as a Colimit. - Benno van den Berg; Chris Heunen (Appl. Categorical Struct., 2012)

A functional interpretation for nonstandard arithmetic. - Benno van den Berg; Eyvind Martol Briseid; Pavol Safarik (Ann. Pure Appl. Log., 2012)

Derived rules for predicative set theory: An application of sheaves. - Benno van den Berg; Ieke Moerdijk (Ann. Pure Appl. Log., 2012)

Topological and Simplicial Models of Identity Types. - Benno van den Berg; Richard Garner (ACM Trans. Comput. Log., 2012)

Erratum to: Noncommutativity as a Colimit. - Benno van den Berg; Chris Heunen (Appl. Categorical Struct., 2013)

Non-deterministic inductive definitions. - Benno van den Berg (Arch. Math. Log., 2013)

Are There Enough Injective Sets? - Peter Aczel; Benno van den Berg; Johan Georg Granström; Peter Schuster 001 (Stud Logica, 2013)

The axiom of multiple choice and models for constructive set theory. - Benno van den Berg; Ieke Moerdijk (J. Math. Log., 2014)

W-types in homotopy type theory. - Benno van den Berg; Ieke Moerdijk (Math. Struct. Comput. Sci., 2015)

The strength of countable saturation. - Benno van den Berg; Eyvind Martol Briseid; Pavol Safarik (Arch. Math. Log., 2017)

A note on equality in finite-type arithmetic. - Benno van den Berg (Math. Log. Q., 2017)

Nonstandard Functional Interpretations and Categorical Models. - Amar Hadzihasanovic; Benno van den Berg (Notre Dame J. Formal Log., 2017)

W-types in homotopy-type theory - CORRIGENDUM. - Benno van den Berg; Ieke Moerdijk (Math. Struct. Comput. Sci., 2018)

Path Categories and Propositional Identity Types. - Benno van den Berg (ACM Trans. Comput. Log., 2018)

A Kuroda-style j-translation. - Benno van den Berg (Arch. Math. Log., 2019)

Reverse Mathematics and parameter-free Transfer. - Benno van den Berg; Sam Sanders (Ann. Pure Appl. Log., 2019)

A homotopy-theoretic model of function extensionality in the effective topos. - Daniil Frumin; Benno van den Berg (Math. Struct. Comput. Sci., 2019)

Univalent polymorphism. - Benno van den Berg (Ann. Pure Appl. Log., 2020)

Effective Kan fibrations in simplicial sets. - Benno van den Berg; Eric Faber (CoRR, 2020)

Quadratic type checking for objective type theory. - Benno van den Berg; Martijn den Besten (CoRR, 2021)

Converse extensionality and apartness. - Benno van den Berg; Robert Paßmann (Log. Methods Comput. Sci., 2022)

Conservativity of Type Theory over Higher-Order Arithmetic. - Daniël Otten; Benno van den Berg (CSL, 2024)

Preface: Advances in Homotopy Type Theory. - Thorsten Altenkirch; Benno van den Berg; Nicola Gambino; Maria Emilia Maietti (Math. Struct. Comput. Sci., 2024)