Universes for Generic Programs and Proofs in Dependent Type Theory (with Peter Dybjer and Patrik Jansson): PS PDF
Status: presented at NWPT in Nov 2002 and APPSEM workshop in Mar 2003; submitted for publication.

Towards Generic Programming in Type Theory PS BIB entry
Status: presented at TYPES in Apr 2002, unpublished.

Some tools for computer-assisted theorem proving in Martin-Löf type theory PS PDF
Status: presented at TPHOL'2001 poster session, published in Supplemental Proceedinghs.

Strategies for interactive proof and program development in Martin-Löf Type Theory PS PDF
Status: presented at IJCAR'2001 workshop Strategies in Automated Deduction, published in workshop proceedings.

LaVaZza: Laziness for Java and Pizza (with Rafal Bledzinski) PS
Status: unpublished.

Complexity of type reconstruction in programming languages with subtyping
PhD thesis, Warsaw University 1997. PDF PS

Predicative Polymorphic Subtyping PS
Warsaw University TR 98-02 (251), 1998.
An extended abstract of this report appeared at MFCS'98.

An algebraic characterization of typability in ML with subtyping PS
Warsaw University TR 96-14 (235), 1996.
An extended abstract of this report appeared at FOSSACS'99.

Some Complexity Bounds for Subtype Inequalities PS
Warsaw University TR 95-20 (220), 1995.
A revised version of this paper was published in Theoretical Computer Science 212 (1999) 3--27

Efficient Type Reconstruction in the Presence of Inheritance PS
Warsaw University TR 94-10 (199), 1994.
An extended abstract of this report appeared at MFCS'93.