| 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) |