Safe Proof Checking in Type Theory with Y. - Herman Geuvers; Erik Poll; Jan Zwanenburg (CSL, 1999)

A Logic for Abstract Data Types as Existential Types. - Erik Poll; Jan Zwanenburg (TLCA, 1999)

Pure Type Systems with Subtyping. - Jan Zwanenburg (TLCA, 1999)

Equational Reasoning via Partial Reflection. - Herman Geuvers; Freek Wiedijk; Jan Zwanenburg (TPHOLs, 2000)

A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals. - Herman Geuvers; Freek Wiedijk; Jan Zwanenburg (TYPES, 2000)

From Algebras and Coalgebras to Dialgebras. - Erik Poll; Jan Zwanenburg (CMCS, 2001)

A Constructive Algebraic Hierarchy in Coq. - Herman Geuvers; Randy Pollack; Freek Wiedijk; Jan Zwanenburg (J. Symb. Comput., 2002)

First Order Logic with Domain Conditions. - Freek Wiedijk; Jan Zwanenburg (TPHOLs, 2003)