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