## Homepage for Benno van den Berg

Universiteit van Amsterdam

Institute for Logic, Language and Computation

P.O. Box 94242, NL

1090 GE Amsterdam

The Netherlands

tel: +31 20 525 5360

email: bennovdberg AT gmail.com

Teaching:Information about my teaching can be found here.

PhD thesis:

Predicative topos theory and models for constructive set theory[PS][PDF]

Defended 22 May 2006, at the University of Utrecht. Supervised by prof. Ieke Moerdijk. Paper copies available on request.

Habilitationsschrift:

Categorical semantics of constructive set theory[PDF]

Defended 3 November 2011, at the Technische Universität Darmstadt. Supervised by prof. Thomas Streicher.

Papers:

Inductive types and exact completion

Annals of Pure and Applied Logic 134 (2005), pp. 95-121.

Non-well-founded trees in categories[PS][PDF]

Joint work with Federico De Marchi. Annals of Pure and Applied Logic 146 (2007), pp. 40-59.

Models of non-well-founded sets via an indexed final coalgebra theorem[PS][PDF]

Joint work with Federico De Marchi. Journal of Symbolic Logic 72-3 (2007), pp. 767-791.

Aspects of predicative Algebraic Set Theory I: Exact completion[PS][PDF]

Joint work with Ieke Moerdijk. Annals of Pure and Applied Logic 156 (2008), pp. 123-159.

Three extensional models of type theory[PS][PDF]

Mathematical Structures in Computer Science 19 (2009), pp. 417-434.

A unified approach to Algebraic Set Theory[PS][PDF]

Joint work with Ieke Moerdijk. In: Logic Colloquium 2006, Lecture Notes in Logic (2009), pp. 18-37.

Aspects of predicative Algebraic Set Theory II: Realizability[PS][PDF]

Joint work with Ieke Moerdijk. Theoretical Computer Science 412 (2011), pp. 1916-1940.

Types are weak omega-groupoids[PS][PDF]

Joint work with Richard Garner. Proceedings of the London Mathematical Society (3) 102 (2011), pp. 370-394.

Topological and simplicial models of identity types[PS][PDF]

Joint work with Richard Garner. ACM Transactions on Computational Logic (TOCL), Volume 13, Number 1 (2012).

Noncommutativity as a colimit[PS][PDF]

Joint work with Chris Heunen. Applied Categorical Structures, volume 20, number 4 (2012), pp. 393-414.

Derived rules for predicative set theory: an application of sheaves[PS][PDF]

Joint work with Ieke Moerdijk. Annals of Pure and Applied Logic, volume 163, issue 10 (2012), pp. 1367-1383.

A functional interpretation for nonstandard arithmetic[PS][PDF]

Joint work with Eyvind Briseid and Pavol Safarik. Annals of Pure and Applied Logic, volume 163, issue 12 (2012), pp. 1962–1994.

No-go theorems for functorial localic spectra of noncommutative rings[PS][PDF]

Joint work with Chris Heunen. Proceedings of the 8th International Workshop on Quantum Physics and Logic, EPTCS, volume 95 (2012), pp. 21-27.

Aspects of predicative Algebraic Set Theory III: Sheaves[PS][PDF]

Joint work with Ieke Moerdijk. Proceedings of the London Mathematical Society (5) 105 (2012), pp. 1076-1122.

Non-deterministic inductive definitions[PDF]

Archive for Mathematical Logic, volume 52, issue 1 (2013), pp. 113-135.

Are there enough injective sets?[PS][PDF]

Joint work with Peter Aczel, Johan Granström and Peter Schuster. Studia Logica (3) 101 (2013), pp. 467-482.

The Herbrand topos[PDF]

Mathematical Proceedings of the Cambridge Philosophical Society, volume 155, number 2 (2013), pp. 361-374.

The axiom of multiple choice and models for constructive set theory[PDF]

Joint work with Ieke Moerdijk. Journal of Mathematical Logic, volume 14, number 1 (2014), 28 pp.

Extending obstruction to noncommutative functorial spectra[PDF]

Joint work with Chris Heunen. Theory and Applications of Categories, volume 29, number 17 (2014), pp. 457-474.

W-types in homotopy type theory[PDF]

Joint work with Ieke Moerdijk. Accepted for publication in Mathematical Structures in Computer Science.

Nonstandard functional interpretations and categorical models[PDF]

Joint work with Amar Hadzihasanovic. Accepted for publication in Notre Dame Journal of Formal Logic.

Preprints:

Notes:

WISC is independent from ZF[PDF]

Unpublished note.

A topos for a nonstandard functional interpretation[PDF]

Unpublished note.

A note on arithmetic in finite types[PDF]

Unpublished note.

Last updated: 12 September 2014