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
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
Status: presented at TPHOL'2001 poster session, published in Supplemental Proceedinghs.
Strategies for interactive proof and program
development in Martin-Löf Type Theory
Status: presented at IJCAR'2001 workshop Strategies in Automated Deduction, published in workshop proceedings.
LaVaZza: Laziness for Java and Pizza
(with Rafal Bledzinski)
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
Warsaw University TR 96-14 (235), 1996.
An extended abstract of this report appeared at FOSSACS'99.
Some Complexity Bounds for Subtype Inequalities
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
Warsaw University TR 94-10 (199), 1994.
An extended abstract of this report appeared at MFCS'93.