111 Cummington St., Boston, MA 02215 | cs-www.bu.edu
Last updated: July 20, 2010

Reports

Below is a selection of papers that report work done as part of the Church Project.

Members: To add a new report, consult the maintenance page.


Copyright notice: The documents contained in these pages are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.

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)