Multiple Recursion in Type Theory
Status: presented at TYPES 2008

Alonzo — a compiler for Agda PDF
Status: presented at AIM6 and TYPES2007

Valid XML Transformations with Dependent Types PDF
Status: manuscript, 2007

A Tool for Automated Theorem Proving in Agda (with Fredrik Lindblad) PDF
Status: presented at TYPES 2004, published in LNCS 3839, 2006

Veryfying Haskell Programs Using Constructive Type Theory
(with Andreas Abel, Ana Bove, John Hughes and Ulf Norell): PS PDF
Status: presented at Haskell Workshop in Sep 2005;

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; published in Nordic Journal of Computing.

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.