Andrei Lapets and Assaf Kfoury. **A User-friendly Interface for a Lightweight Verification System.** (May 2010) (bib) (link) |

Andrei Lapets. **User-friendly Support for Common Concepts in a Lightweight Verifier.** (May 2010) (bib) (link) |

Andrei Lapets and Assaf Kfoury. **Verification with Natural Contexts: Soundness of Safe Compositional Network Sketches.** (October 2009) (bib) (link) |

Sébastien Carlier and J. B. Wells. **The Algebra of Expansion.** (March 2008) (bib) (PDF) |

Kevin Donnelly and Assaf J. Kfoury. **Some Considerations on Formal Semantics For Weak References.** (July 2005) (bib) (PDF) |

Joseph J. Hallett and Assaf J. Kfoury. **A Formal Semantics For Weak References.** (May 2005) (bib) (PDF) |

Adam Bakewell and Assaf J. Kfoury. **Properties of a Rewrite System for Unification with Expansion Variables.** (April 2005) (bib) (PDF) |

Dengping Zhu and Hongwei Xi. **Safe Programming with Pointers through Stateful Views.** (January 2005) (bib) (PDF) |

Henning Makholm and J. B. Wells. **Instant Polymorphic Type Systems for Mobile Process
Calculi: Just Add Reduction Rules and Close.** (bib) (PDF) |

Henning Makholm and J. B. Wells. **Type Inference, Principal Typings, and
Let-Polymorphism for First-Class Mixin Modules.** (bib) (PDF) |

Adam Bakewell and Assaf J. Kfoury. **Unification with Expansion Variables.** (December 2004) (bib) (PDF) |

Henning Makholm and J. B. Wells. **Instant Polymorphic Type Systems for Mobile Process
Calculi: Just Add Reduction Rules and Close.** (November 2004) (bib) (PDF) |

Joseph J. Hallett and Assaf J. Kfoury. **Programming Examples Needing Polymorphic Recursion.** (January 2004) (bib) (PDF) |

Hongwei Xi. **Applied Type System (extended abstract).** (2004) (bib) (PDF) |

Henning Makholm and J. B. Wells. **Type Inference for PolyA.** (January 2004) (bib) (PDF) |

Christian Haack and J. B. Wells. **Type Error Slicing in Implicitly Typed Higher-Order
Languages.** (2004) (bib) (PDF) |

Sébastien Carlier and J. B. Wells. **Type Inference with Expansion Variables and
Intersection Types in System~E and an Exact
Correspondence with $\beta$-Reduction.** (2004) (bib) (PDF) |

Peter Møller Neergaard. **Complexity Aspects of Programming Language Design---From Logspace to Elementary Time via Proofnets and Intersection Types.** (October 2004) (bib) (PDF) |

Peter Møller Neergaard. **A Bargain for Intersection Types: A Simple Strong Normalization Proof.** (bib) (PDF) (link) |

Peter Møller Neergaard. **BC$^\textrm-_\epsilon$: A Recursion-Theoretic Characterization of \textsclogspace.** (March 2004) (bib) (PDF) (link) |

Peter Møller Neergaard. **A Functional Language for Logarithmic Space.** (2004) (bib) (PDF) (link) |

Peter Møller Neergaard and Harry G. Mairson. **Types, Potency, and Idempotency: Why Nonlinearity and Amnesia Make a Type System Work.** (2004) (bib) (PDF) (link) |

Assaf J. Kfoury and J. B. Wells. **Principality and Type Inference for Intersection
Types Using Expansion Variables.** (2004) (bib) (PDF) |

Dengping Zhu and Hongwei Xi. **A Typeful and Tagless Representation for XML Documents.** (November 2003) (bib) (PDF) |

Hongwei Xi. **Facilitating Program Verification with Dependent Types.** (September 2003) (bib) (PDF) |

Chiyan Chen and Hongwei Xi. **Meta-Programming through Typeful Code Representation.** (August 2003) (bib) (PDF) |

Chiyan Chen and Hongwei Xi. **Implementing Typeful Program Transformation.** (June 2003) (bib) (PDF) |

Hongwei Xi. **Dependently Typed Pattern Matching.** (May 2003) (bib) (PDF) |

Hongwei Xi. **Dependently Typed Pattern Matching.** (2003) (bib) (PDF) |

Gang Chen. **Soundness of Coercion in the Calculus of Constructions.** (2003) (bib) |

Gang Chen. **Coercive Subtyping for the Calculus of Constructions
(extended abstract).** (2003) (bib) (PDF) (link) |

Peter Møller Neergaard and Harry G. Mairson. **Rank Bounded Intersection: Types, Potency, and
Idempotency.** (2003) (bib) |

Christian Haack and J. B. Wells. **Type Error Slicing in Implicitly Typed Higher-Order
Languages.** (2003) (bib) (PDF) |

Assaf J. Kfoury and J. B. Wells. **Principality and Type Inference for Intersection
Types Using Expansion Variables.** (August 2003) (bib) (PDF) |

Peter Møller Neergaard and Harry G. Mairson. **How Light is Safe Recursion? Translations Between Logics of Polynomial Time.** (2003) (bib) |

Torben Amtoft and Robert Muller. **Inferring Annotated Types for Inter-procedural
Register Allocation with Constructor Flattening.** (January 2003) (bib) (PDF) |

Peter Møller Neergaard and Morten Heine Bjørnlund Sørensen. **Conservation and Uniform Normalization in $\lambda$-calculi with Erasing Reductions.** (October 2002) (bib) |

Peter Møller Neergaard and Harry G. Mairson. **LAL Is Square: Representation and Expressiveness in Light Affine Logic.** (2002) (bib) (PDF) (link) |

Hongwei Xi. **Dependent Types for Program Termination Verification.** (October 2002) (bib) (PDF) |

Hongwei Xi. **Unifying Object-Oriented Programming with Typed Functional Programming.** (September 2002) (bib) (PDF) |

Gang Chen. **Full Integration of Subtyping and If-expression.** (2002) (bib) (PDF) (link) |

Torben Amtoft and J. B. Wells. **Mobile Processes with Dependent Communication Types
and Singleton Types for Names and Capabilities.** (December 2002) (bib) (PDF) (link) |

Sébastien Carlier. **Polar Type Inference with Intersection Types and $ømega$.** (2002) (bib) |

J. B. Wells. **The Essence of Principal Typings.** (2002) (bib) (PDF) |

J. B. Wells. **The Essence of Principal Typings.** (2002) (bib) (PDF) |

J. B. Wells and Christian Haack. **Branching Types.** (200X) (bib) (PDF) |

J. B. Wells and Christian Haack. **Branching Types.** (2002) (bib) (PDF) |

Torben Amtoft. **Causal Type System for Ambient Movements.** (2002) (bib) (PDF) (link) |

Franklyn Turbak and J. B. Wells. **Cycle Therapy: A Prescription for Fold and Unfold on
Regular Trees.** (2001) (bib) (PDF) |

Santiago M. Pericas-Geertsen. **XML-Fluent Mobile Ambients.** (2001) (bib) (PDF) |

Alan Bawden. **First-class Macros Have Types.** (2000) (bib) (PDF) (link) |

Julia L. Lawall and Harry G. Mairson. **Sharing continuations: proofnets for languages with
explicit control.** (2000) (bib) (PDF) (link) |

C. A. Stewart. **On the formulae-as-types correspondence for
classical logic.** (2000) (bib) |

Assaf J. Kfoury. **A Linearization of the Lambda-Calculus.** (2000) (bib) (PDF) (link) |

Michele Bugliesi and Santiago M. Pericas-Geertsen. **Type Inference for variant object types.** (2000) (bib) (PDF) |

Michele Bugliesi and Santiago M. Pericas-Geertsen. **Depth Subtyping and Type Inference for Object
Calculi.** (2000) (bib) (PDF) |

Torben Amtoft and Franklyn Turbak. **Faithful Translations between Polyvariant Flows and Polymorphic Types.** (2000) (bib) (PDF) (link) |

Torben Amtoft and Franklyn Turbak. **Faithful Translations between Polyvariant Flows and Polymorphic Types.** (2000) (bib) (PDF) |

Elena Machkasova and Franklyn A. Turbak. **A Calculus for Link-time Compilation.** (2000) (bib) (PDF) (link) |

Elena Machkasova and Franklyn Turbak. **A Calculus for Link-time Compilation.** (2000) (bib) |

Assaf J. Kfoury. **Beta-Reduction as Unification.** (1999) (bib) (PDF) (link) |

Assaf J. Kfoury and Santiago M. Pericas-Geertsen. **Type Inference for Recursive Definitions.** (1999) (bib) (PDF) |

Assaf J. Kfoury and Santiago M. Pericas-Geertsen. **Type Inference for Recursive Definitions.** (1999) (bib) (PDF) |

Torben Amtoft. **Partial Evaluation for Constraint-Based Program
Analyses.** (1999) (bib) (PDF) (link) |

Assaf J. Kfoury and J. B. Wells. **Principality and Decidable Type Inference for
Finite-Rank Intersection Types.** (1999) (bib) |

J. B. Wells. **Typability and Type Checking in System F Are Equivalent and Undecidable.** (1999) (bib) |

C.-H. L. Ong and C. A. Stewart. **A Curry-Howard foundation for functional
computation with control.** (1997) (bib) (PDF) (link) |

Anindya Banerjee. **A Modular, Polyvariant, and Type-Based Closure
Analysis.** (1997) (bib) (PDF) (link) |

Assaf J. Kfoury. **Beta-Reduction as Unification.** (July 1996) (bib) (PDF) (link) |

Assaf J. Kfoury. **A Linearization of the Lambda-Calculus.** (September 1996) (bib) (PDF) (link) |

J. B. Wells. **Typability is Undecidable for F+Eta.** (March 1996) (bib) |

Trevor Jim. **Rank 2 Type Systems and Recursive Definitions.** (November 1995) (bib) (PDF) (link) |

Trevor Jim. **What Are Principal Typings and What Are They Good
For?.** (1995) (bib) (PDF) (link) |

A. J. Kfoury and J. B. Wells. **New Notions of Reduction and Non-Semantic Proofs of
$\beta$-Strong Normalization in Typed
$\lambda$-Calculi.** (1995) (bib) (PDF) (link) |

J. B. Wells. **The Undecidability of Mitchell's Subtyping Relation.** (December 1995) (bib) |