Marc Bezem - Selected Publications#

Isomorphisms between HEO and HRO^E, ECF and ICF^E. Journal of Symbolic Logic 50:359-371, 1985.

Strongly majorizable functionals of finite type: a model for bar recursion containing discontinuous functionals. Journal of Symbolic Logic 50:652-660, 1985.

Compact and majorizable functionals of finite type. Journal of Symbolic Logic 54:271-280, 1989.

Characterizing termination of logic programs with level mappings. Proceedings NACLP:69-80, MIT Press, 1989.

Completeness of resolution revisited. Theoretical Computer Science 74:227-237, 1990.

Acyclic programs. New Generation Computing 9:335-363, 1991. (with K.R. Apt)

Strong termination of logic programs. Journal of Logic Programming 15(1&2):79-97, 1993.

Ramsey’s theorem and the pigeonhole principle in intuitionistic mathematics. Journal of the London Mathematical Society (2) 47:193-211, 1993. (with W. Veldman)

Invariants in process algebra with data. Proceedings CONCUR94, LNCS 836:401-416. Springer-Verlag, Berlin, 1994. (with J.F. Groote)

A correctness proof of a one-bit sliding window protocol. British Computer Journal 37(4):289-307, 1994. Corrigendum in British Computer Journal 37(7):651. (with J.F. Groote)

Two finite specifications of a queue. Theoretical Computer Science, 177(2):487-507, 1997. (with A. Ponse)

On the computational content of the Axiom of Choice. Journal of Symbolic Logic 63(2):600-622, 1998. (with S. Berardi and T. Coquand)

Diagram techniques for confluence. Information and Computation 141(2):172-204, 1998. (with J.W. Klop and V. van Oostrom)

Automated proof construction in type theory using resolution. Journal of Automated Reasoning 29(3-4):253-275, 2003. (with D. Hendriks and H. de Nivelle)

Automating Coherent Logic. Proceedings LPAR-12, LNCS 3835:246-260, Springer-Verlag, Berlin, 2005. (with T. Coquand)

On the mechanization of the proof of Hessenberg's Theorem in Coherent Logic. Journal of Automated Reasoning 40(1):61-85, 2008. (with D. Hendriks)

Exponential behaviour of the Butkovic-Zimmermann algorithm for solving two-sided linear systems in max-algebra. Discrete Applied Mathematics 156:3506-09, 2008. (+ R.N. & E.R.)

Hard problems in max-algebra, control theory, hypergraphs and other areas. Information Processing Letters 110(4):133-138, 2010. (with R. Nieuwenhuis and E. Rodriguez)

A Type System for Counting Instances of Software Components. Theoretical Computer Science 458:29-48, 2012. (with D. Hovland and H.A. Truong)

A Model of Type Theory in Cubical Sets. Proceedings TYPES 2013, LIPIcs 26:107-128, 2014. (with T. Coquand and S. Huber)

A Kripke Model for Simplicial Sets. Theoretical Computer Science 574:86-91, 2015. (with T. Coquand)

The Univalence Axiom in Cubical Sets. Journal of Automated Reasoning, https://doi.org/10.1007/s10817-018-9472-6. (with T. Coquand and S. Huber)

Syntactic Forcing Models for Coherent Logic. Indagationes Mathematicae, https://doi.org/10.1016/j.indag.2018.06.004. (with U. Buchholtz and T. Coquand)

Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science 55, Cambridge University Press, 2003. (with J.W. Klop and R.C. de Vrijer et al.)

Complete list of publications