Logo
PARTICIPANTS
SCHEDULE
REPORTS
MAILING LIST
HACKERS' GUIDE
HOME
 

Bibtex file for the Church Project's reports

Home.bib

@COMMENT{{This file has been generated by bib2bib 1.61}}

@COMMENT{{Command line: bibtex2html/bib2bib -oc reportkeys -ob Home.bib -c churchreport="yes" bibtex/macros.bib bibtex/bibliography.bib bibtex/conferences.bib}}

@PREAMBLE{{{{
  \newcommand{\bibnoop}[1]{}
  \newcommand{\bibvonmagic}[2]{#2}
  \newcommand{\bibsingleletter}[1]{#1}
}}}}

@COMMENT{{PleasedonotputRCS/CVSIdexpansionhere}}

@COMMENT{{***WhoaTOCLseemsliketheabbreviationforTransactions
on Computational Logic.Maybethisisamistake.Checkallentriesusingthisabbreviationtoseeiftheyarecorrect.}}


@TECHREPORT{Bak+Kfo:TR-2005a,
  AUTHOR = {Adam Bakewell and Assaf J. Kfoury},
  TITLE = {Properties of a Rewrite System for
                  Unification with Expansion Variables},
  INSTITUTION = {Church Project, Boston University},
  YEAR = 2005,
  MONTH = APR,
  CHURCHREPORT = {yes},
  TYPE = {Technical Report},
  PDF = {http://cs-people.bu.edu/bake/uwev/propbun.pdf},
  POSTSCRIPT = {http://cs-people.bu.edu/bake/uwev/propbun.ps.gz}
}


@TECHREPORT{Bak+Kfo:BUCS-TR-2004-0xx,
  AUTHOR = {Adam Bakewell and Assaf J. Kfoury},
  TITLE = {Unification with Expansion Variables},
  INSTITUTION = {Department of Computer Science, Boston University},
  YEAR = 2004,
  MONTH = DEC,
  CHURCHREPORT = {yes},
  TYPE = {Technical Report},
  PDF = {http://cs-people.bu.edu/bake/uwev/betau.pdf},
  POSTSCRIPT = {http://cs-people.bu.edu/bake/uwev/betau.ps.gz}
}


@TECHREPORT{Bak+Car+Kfo+Wel:BUCS-TR-2005a,
  AUTHOR = {Adam Bakewell and S{\'e}bastien Carlier and
                  A. J. Kfoury and J. B. Wells},
  TITLE = {Inferring Intersection Typings that are Equivalent
                  to Call-by-Name and Call-by-Value Evaluations},
  INSTITUTION = {Church Project, Boston University},
  YEAR = 2005,
  MONTH = APR,
  DATE = {2005-04-13},
  CHURCHREPORT = {yes},
  TYPE = {Technical Report},
  PDF = {http://cs-people.bu.edu/bake/uwev/nameval.pdf},
  POSTSCRIPT = {http://cs-people.bu.edu/bake/uwev/nameval.ps.gz},
  ABSTRACT = {We present a procedure to infer a typing for an
                  arbitrary $\lambda$-term $M$ in an intersection-type
                  system that translates into exactly the call-by-name
                  (resp., call-by-value) evaluation of $M$. Our
                  framework is the recently developed System~E which
                  augments intersection types with \emph{expansion
                  variables}. The inferred typing for $M$ is obtained
                  by setting up a unification problem involving both
                  type variables and expansion variables, which we
                  solve with a confluent rewrite system. The inference
                  procedure is \emph{compositional} in the sense that
                  typings for different program components can be
                  inferred in \emph{any} order, and without knowledge
                  of the definition of other program components.
                  Using expansion variables lets us achieve a
                  compositional inference procedure
                  easily. Termination of the procedure is generally
                  undecidable. The procedure terminates and returns a
                  typing iff the input $M$ is normalizing according to
                  call-by-name (resp., call-by-value). The inferred
                  typing is \emph{exact} in the sense that the exact
                  call-by-name (resp., call-by-value) behaviour of $M$
                  can be obtained by a (polynomial) transformation of
                  the typing.  The inferred typing is also
                  \emph{principal} in the sense that any other typing
                  that translates the call-by-name (resp.,
                  call-by-value) evaluation of $M$ can be obtained
                  from the inferred typing for $M$ using a
                  substitution-based transformation.}
}


@TECHREPORT{Bak+Car+Kfo+Wel:BUCS-TR-2004-0xy,
  AUTHOR = {Adam Bakewell and S{\'e}bastien Carlier
                  and A. J. Kfoury and J. B. Wells},
  TITLE = {Exact Intersection Typing Inference
                  and Call-by-Name Evaluation},
  INSTITUTION = {Department of Computer Science, Boston University},
  YEAR = 2004,
  MONTH = DEC,
  NOTE = {Superseded by \cite{Bak+Car+Kfo+Wel:BUCS-TR-2005a}},
  CHURCHREPORT = {yes},
  TYPE = {Technical Report},
  PDF = {http://cs-people.bu.edu/bake/uwev/seti.pdf},
  POSTSCRIPT = {http://cs-people.bu.edu/bake/uwev/seti.ps.gz}
}


@TECHREPORT{Hal+Kfo:BUCS-TR-2004-004,
  AUTHOR = {Joseph J. Hallett and Assaf J. Kfoury},
  TITLE = {Programming Examples Needing Polymorphic Recursion},
  INSTITUTION = {Department of Computer Science, Boston University},
  YEAR = 2004,
  MONTH = JAN,
  CHURCHREPORT = {yes},
  TYPE = {Technical Report},
  NUMBER = {BUCS-TR-2004-004},
  PDF = {http://www.church-project.org/reports/electronic/Hal+Kfo:BUCS-TR-2004-004.pdf},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Hal+Kfo:BUCS-TR-2004-004.ps.gz},
  XPOSTSCRIPT = {http://www.cs.bu.edu/techreports/2004-004-polymorphic-recursion-progams.ps.Z},
  XPDF = {http://www.cs.bu.edu/techreports/pdf/2004-004-polymorphic-recursion-progams.pdf},
  ITRSPAPER = {yes},
  ABSTRACT = {Inferring types for polymorphic recursive function definitions (abbreviated
to {\em polymorphic recursion}) is a recurring topic on the mailing lists
of popular typed programming languages. This is despite the fact that type
inference for polymorphic recursion using $\forall$-types has been proved
undecidable.  This report presents several programming examples involving
polymorphic recursion and determines their typability under various type
systems, including the Hindley-Milner system, an intersection-type system,
and extensions of these two.  The goal of this report is to show that many
of these examples are typable using a system of intersection types as an
alternative form of polymorphism.  By accomplishing this, we hope to lay
the foundation for future research into a decidable intersection-type inference
algorithm.
\par
We do not provide a comprehensive survey of type systems appropriate
for polymorphic recursion, with or without type annotations inserted in the
source language.  Rather, we focus on examples for which types may be
inferred without type annotations, with an emphasis on systems of
intersection-types.}
}


@TECHREPORT{Hal+Kfo:BUCS-TR-2005-031,
  AUTHOR = {Joseph J. Hallett and Assaf J. Kfoury},
  TITLE = {A Formal Semantics For Weak References},
  INSTITUTION = {Department of Computer Science, Boston University},
  YEAR = 2005,
  MONTH = MAY,
  CHURCHREPORT = {yes},
  TYPE = {Technical Report},
  NUMBER = {Hal+Kfo:BUCS-TR-2005-031},
  PDF = {http://www.church-project.org/reports/electronic/Hal+Kfo:BUCS-TR-2005-031.pdf},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Hal+Kfo:BUCS-TR-2005-031.ps.gz},
  XPOSTSCRIPT = {},
  XPDF = {},
  ITRSPAPER = {no},
  ABSTRACT = {A weak reference is a reference to an object that is not
followed by the pointer tracer when garbage collection is called.  That is,
a weak reference cannot prevent
the object it references from being garbage collected.  Weak references
remain a troublesome programming feature largely because there is not an
accepted, precise semantics that describes their behavior (in fact, we
are not aware of any formalization of their semantics).  The
trouble is that weak references allow reachable objects to be garbage
collected, therefore allowing garbage collection to influence the
result of a program.  Despite this difficulty, weak references continue to be
used in practice for reasons related to efficient storage management, and
are included in many popular programming languages (Standard ML, Haskell,
OCaml, and Java).

We give a formal semantics for a calculus called $\weak$ that includes
weak references and is derived from Morrisett, Felleisen, and Harper's
$\gc$.  $\gc$ formalizes the notion of garbage collection by means of a
rewrite rule.  Such a formalization is required to precisely characterize
the semantics of weak references.  However, the inclusion of a
garbage-collection rewrite-rule in a language with {\em weak references}
introduces non-deterministic evaluation, even if the parameter-passing
mechanism is deterministic (call-by-value in our case).  This raises the
question of confluence for our rewrite system.  We discuss
natural restrictions under which our rewrite system is confluent,
thus guaranteeing uniqueness of program result. We define conditions
that allow other garbage collection algorithms to co-exist with our
semantics of weak references.  We also introduce a polymorphic type system
to prove the absence of erroneous program behavior (i.e., the absence of
``stuck evaluation'') and a corresponding type inference algorithm.  We
prove the type system sound and the inference algorithm sound and complete.}
}


@TECHREPORT{Don+Kfo:BUCS-TR-2005-X,
  AUTHOR = {Kevin Donnelly and Assaf J. Kfoury},
  TITLE = {Some Considerations on Formal Semantics For Weak References},
  INSTITUTION = {Department of Computer Science, Boston University},
  YEAR = 2005,
  MONTH = JUL,
  CHURCHREPORT = {yes},
  TYPE = {Technical Report},
  NUMBER = {Don+Kfo:BUCS-TR-2005-X},
  PDF = {http://www.church-project.org/reports/electronic/Don+Kfo:BUCS-TR-2005-X.pdf},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Don+Kfo:BUCS-TR-2005-X.ps.gz},
  XPOSTSCRIPT = {},
  XPDF = {},
  ITRSPAPER = {no},
  ABSTRACT = {Weak references are references that do not prevent the object they point to from being garbage collected.  Most realistic languages, including Java, SML/NJ, and OCaml to name a few, have some facility for programming with weak references.  Weak references are used in implementing idioms like memoizing functions and hash-consing in order to avoid potential memory leaks.

However, the semantics of weak references in many languages are not clearly specified.  Without a formal semantics for weak references it becomes impossible to prove the correctness of implementations making use of this feature.  Previous work by Hallett and Kfoury \cite{HK-weak} extends $\gc$ \cite{Mor+Fel+Har:FPCA-1995}, a language for modeling garbage collection, to $\weak$, a similar language with weak references.

Using this previously formalized semantics for weak references, we consider two issues related to well-behavedness of programs.  Firstly, we provide a new, simpler proof of the well-behavedness of the syntactically restricted fragment of $\weak$ defined in \cite{HK-weak}.  Secondly, we give a natural semantic criterion for well-behavedness much broader than the syntactic restriction, which is useful as principle for programming with weak references.

Furthermore we extend the result, proved in \cite{Mor+Fel+Har:FPCA-1995}, which allows one to use type-inference to collect some reachable objects that are never used.  We prove that this result holds of our language, and we extend this result to allow the collection of weakly-referenced reachable garbage without incurring the computation overhead sometimes associated with collecting weak bindings (e.g. the need to recompute a memoized function).

Lastly we use extend the semantic framework to model the key/value weak references found in Haskell and we prove the Haskell is semantics equivalent to a simpler semantics due to the lack of side-effects in our language.}
}


@TECHREPORT{Don+Hal+Kfo:BUCS-TR-2005-X,
  AUTHOR = {Kevin Donnelly and Joseph J. Hallett and Assaf J. Kfoury},
  TITLE = {Formal Semantics For Weak References},
  INSTITUTION = {Department of Computer Science, Boston University},
  YEAR = 2005,
  MONTH = JUL,
  CHURCHREPORT = {yes},
  TYPE = {Technical Report},
  NUMBER = {Don+Hal+Kfo:BUCS-TR-2005-X},
  PDF = {http://www.church-project.org/reports/electronic/Don+Hal+Kfo:BUCS-TR-2005-X.pdf},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Don+Hal+Kfo:BUCS-TR-2005-X.ps.gz},
  XPOSTSCRIPT = {},
  XPDF = {},
  ITRSPAPER = {no},
  ABSTRACT = {Weak references are references that do not prevent
                  the object they point to from being garbage
                  collected. Many realistic languages, including Java,
                  SML/NJ, and Haskell to name a few, support weak
                  references. However, there is no generally accepted
                  formal semantics for weak references. Without such a
                  formal semantics it becomes impossible to formally
                  prove properties of such a language and the programs
                  written in it.
                  \par
                  We give a formal semantics for a calculus called
                  lambda-weak that includes weak references and is
                  derived from Morrisett, Felleisen, and Harper's
                  lambda-gc. The semantics is used to examine several
                  issues involving weak references. We use the
                  framework to formalize the semantics for the
                  key/value weak references found in
                  Haskell. Furthermore, we consider a type system for
                  the language and show how to extend the earlier
                  result that type inference can be used to collect
                  reachable garbage. In addition we show how to allow
                  collection of weakly referenced garbage without
                  incurring the computational overhead often
                  associated with collecting a weak reference which
                  may be later used. Lastly, we address the
                  non-determinism of the semantics by providing both
                  an effectively decidable syntactic restriction and a
                  more general semantic criterion, which guarantee a
                  unique result of evaluation.}
}


@ARTICLE{Xi:JHOSL-2002,
  AUTHOR = {Hongwei Xi},
  TITLE = {Dependent Types for Program Termination Verification},
  JOURNAL = {Journal of Higher-Order and Symbolic Computation},
  YEAR = 2002,
  MONTH = OCT,
  VOLUME = 15,
  PAGES = {91--131},
  POSTSCRIPT = {http://www.cs.bu.edu/~hwxi/academic/papers/HOSCdmlterm.ps},
  PDF = {http://www.cs.bu.edu/~hwxi/academic/papers/HOSCdmlterm.pdf},
  CHURCHREPORT = {yes},
  ABSTRACT = {
Program termination verification is a challenging research subject of
significant practical importance. While there is already a rich body
of literature on this subject, it is still undeniably a difficult task
to design a termination checker for a realistic programming language
that supports general recursion.  In this paper, we present an
approach to program termination verification that makes use of a form
of dependent types developed in Dependent ML (DML), demonstrating a
novel application of such dependent types to establishing a liveness
property. We design a type system that enables the programmer to
supply metrics for verifying program termination and prove that every
well-typed program in this type system is terminating.  We also
provide realistic examples, which are all verified in a prototype
implementation, to support the effectiveness of our approach to
program termination verification as well as its unobtrusiveness to
programming. The main contribution of the paper lies in the design of
an approach to program termination verification that smoothly combines
types with metrics, yielding a type system capable of guaranteeing
program termination that supports a general form of recursion
(including mutual recursion), higher-order functions, algebraic
datatypes, and polymorphism.
}
}


@INPROCEEDINGS{Xi:SEFM-2003,
  AUTHOR = {Hongwei Xi},
  TITLE = {Facilitating Program Verification with Dependent Types},
  BOOKTITLE = {Proceedings of the International Conference on Software Engineering and Formal Methods},
  YEAR = 2003,
  MONTH = SEP,
  ADDRESS = {Brisbane, Australia},
  PAGES = {72--81},
  POSTSCRIPT = {http://www.cs.bu.edu/~hwxi/academic/papers/sefm03.ps},
  PDF = {http://www.cs.bu.edu/~hwxi/academic/papers/sefm03.pdf},
  CHURCHREPORT = {yes},
  ABSTRACT = {
The use of types in capturing program invariants is overwhelming in
practical programming.  The type systems in languages such as ML and Java
scale convincingly to realistic programs but they are of relatively limited
expressive power. In this paper, we show that the use of a restricted form
of dependent types can enable us to capture many more program invariants
such as memory safety while retaining practical type-checking. The
programmer can encode program invariants with type annotations and then
verify these invariants through static type-checking. Also the type
annotations can serve as informative program documentation, which are
mechanically verified and can thus be fully trusted. We argue with
realistic examples that this restricted form of dependent types can
significantly facilitate program verification as well as program
documentation.
}
}


@INPROCEEDINGS{Chen+Zhu+Xi:PADL-2004,
  AUTHOR = {Chiyan Chen and Dengping Zhu and Hongwei Xi},
  TITLE = {Implementing Cut Elimination: A Case Study of Simulating Dependent Types in {Haskell}},
  BOOKTITLE = {Proceedings of the 6th International Symposium on Practical Aspects of Declarative Languages},
  PUBLISHER = {Springer-Verlag LNCS vol. 3057},
  YEAR = {2004},
  MONTH = {June},
  PAGES = {239-254},
  ADDRESS = {Dallas, TX},
  CHURCHREPORT = {yes},
  POSTSCRIPT = {http://www.cs.bu.edu/~hwxi/academic/papers/CutElim/CutElim.ps},
  PDF = {http://www.cs.bu.edu/~hwxi/academic/papers/CutElim/CutElim.pdf},
  ABSTRACT = {
Gentzen's Hauptsatz -- cut elimination theorem -- in sequent calculi
reveals a fundamental property on logic connectives in various logics such
as classical logic and intuitionistic logic.  In this paper, we implement a
procedure in Haskell to perform cut elimination for intuitionistic sequent
calculus, where we use types to guarantee that the procedure can only
return a cut-free proof of the same sequent when given a proof of a sequent
that may contain cuts.  The contribution of the paper is two-fold.  On
the one hand, we present an interesting (and somewhat unexpected) application
of the current type system of Haskell, illustrating through a concrete
example how some typical use of dependent types can be simulated in
Haskell. On the other hand, we identify several problematic issues with
such a simulation technique and then suggest some approaches to addressing
these issues in Haskell.
}
}


@INPROCEEDINGS{Chen+Shi+Xi:PADL-2004,
  AUTHOR = {Chiyan Chen and Rui Shi and Hongwei Xi},
  TITLE = {A Typeful Approach to Object-Oriented Programming with Multiple Inheritance},
  BOOKTITLE = {Proceedings of the 6th International Symposium on Practical Aspects of Declarative Languages},
  PUBLISHER = {Springer-Verlag LNCS vol. 3057},
  PAGES = {23-38},
  YEAR = {2004},
  MONTH = {June},
  ADDRESS = {Dallas, TX},
  CHURCHREPORT = {yes},
  POSTSCRIPT = {http://www.cs.bu.edu/~hwxi/academic/papers/OBJwMI/OBJwMI.ps},
  PDF = {http://www.cs.bu.edu/~hwxi/academic/papers/OBJwMI/OBJwMI.pdf},
  ABSTRACT = {
The wide practice of objected oriented programming (OOP) in current
software practice is evident. Despite extensive studies on typing
programming objects, it is still undeniably a challenging research task to
design a type system that can satisfactorily account for a variety of
features (e.g., binary methods and multiple inheritance) in OOP. In this
paper, we present a typeful approach to implementing objects that makes use
of a recently introduced notion of guarded datatypes. In particular, we
demonstrate how the feature of multiple inheritance can be supported with
this approach, presenting a simple and general account for multiple
inheritance in a typeful manner.
}
}


@INPROCEEDINGS{Xi:TYPES-2004,
  AUTHOR = {Hongwei Xi},
  TITLE = {Applied Type System (extended abstract)},
  BOOKTITLE = {post-workshop Proceedings of TYPES 2003},
  PUBLISHER = {Springer-Verlag LNCS 3085},
  YEAR = {2004},
  PAGES = {394--408},
  CHURCHREPORT = {yes},
  POSTSCRIPT = {http://www.cs.bu.edu/~hwxi/academic/papers/types03.ps},
  PDF = {http://www.cs.bu.edu/~hwxi/academic/papers/types03.pdf},
  ABSTRACT = {{
The framework Pure Type System (PTS) offers a simple and general
approach to designing and formalizing type systems. However, in the
presence of dependent types, there often exist some acute problems that
make it difficult for PTS to accommodate many common realistic
programming features such as general recursion, recursive types, effects
(e.g., exceptions, references, input/output), etc. In this paper, we
propose a new framework Applied Type System (ATS) to allow for designing
and formalizing type systems that can readily support common realistic
programming features. The key salient feature of ATS lies in a complete
separation between statics, in which types are formed and reasoned about,
and dynamics, in which programs are constructed and evaluated. With this
separation, it is no longer possible for a program to occur in a type as is
otherwise allowed in PTS.  We present not only a formal development of
ATS but also mention some examples in support of using ATS as a
framework to form type systems for practical programming.
}}
}


@ARTICLE{Andrews+etc:JAR-2004,
  AUTHOR = {Peter Andrews and Matthew Bishop and Chad Brown and Sunil Issar and Frank Pfenning and Hongwei Xi},
  TITLE = {ETPS: A System to Help Students to Write Formal Proofs},
  JOURNAL = {Journal of Automated Reasoning},
  VOLUME = {32},
  YEAR = {2004},
  PAGES = {75--92},
  CHURCHREPORT = {yes},
  POSTSCRIPT = {http://www.cs.bu.edu/~hwxi/academic/papers/etps-jar.ps},
  PDF = {http://www.cs.bu.edu/~hwxi/academic/papers/etps-jar.pdf},
  ABSTRACT = {
ETPS (Educational Theorem Proving System) is a program which logic students
and use to write formal proofs in first-order logic or higher-order
logic. It help students to concentrate on the essential logic problems
involved in proving theorems, and automatically checks the proofs.
}
}


@INPROCEEDINGS{Chen+Xi:ICFP-2003,
  AUTHOR = {Chiyan Chen and Hongwei Xi},
  TITLE = {Meta-Programming through Typeful Code Representation},
  BOOKTITLE = {Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming},
  YEAR = 2003,
  MONTH = AUG,
  ADDRESS = {Uppsala, Sweden},
  PAGES = {275--286},
  POSTSCRIPT = {http://www.cs.bu.edu/~hwxi/academic/papers/icfp03.ps},
  PDF = {http://www.cs.bu.edu/~hwxi/academic/papers/icfp03.pdf},
  CHURCHREPORT = {yes},
  ABSTRACT = {
By allowing the programmer to write code that can generate code at
run-time, meta-programming offers a powerful approach to program
construction. For instance, meta-programming can often be employed to
enhance program efficiency and facilitate the construction of generic
programs.  However, meta-programming, especially in an untyped setting, is
notoriously error-prone.  In this paper, we aim at making meta-programming
less error-prone by providing a type system to facilitate the construction
of correct meta-programs.  We first introduce some code constructors for
constructing typeful code representation in which program variables are
replaced with deBruijn indices, and then formally demonstrate how such
typeful code representation can be used to support meta-programming.  The
main contribution of the paper lies in recognition and then
formalization of a novel approach to typed meta-programming that is
practical, general and flexible.
}
}


@INPROCEEDINGS{Chen+Xi:PEPM-2003,
  AUTHOR = {Chiyan Chen and Hongwei Xi},
  TITLE = {Implementing Typeful Program Transformation},
  BOOKTITLE = {Proceedings of ACM SIGPLAN Workshop on Partial Evaluation and Semantics Based Program Manipulation},
  YEAR = {2003},
  MONTH = JUN,
  CHURCHREPORT = {yes},
  ADDRESS = {San Diego, CA},
  POSTSCRIPT = {http://www.cs.bu.edu/~hwxi/academic/papers/pepm03.ps},
  PDF = {http://www.cs.bu.edu/~hwxi/academic/papers/pepm03.pdf},
  ABSTRACT = {The notion of program transformation is ubiquitous in programming language
studies on interpreters, compilers, partial evaluators, etc. In order to
implement a program transformation, we need to choose a representation in
the meta language, that is, the programming language in which we construct
programs, for representing object programs, that is, the programs in the
object language on which the program transformation is to be performed. In
practice, most representations chosen for typed object programs are
typeless in the sense that the type of an object program cannot be
reflected in the type of its representation. This is unsatisfactory as
such typeless representations make it impossible to capture in the type
system of the meta language various invariants in a program transformation
that are related to the types of object programs.  In this paper, we
propose an approach to implementing program transformations that makes use
of a first-order typeful program representation formed in Dependent ML
(DML), where the type of an object program as well as the types of the
free variables in the object program can be reflected in the type of the
representation of the object program. We introduce some programming
techniques needed to handle this typeful program representation, and then
present an implementation of a CPS transform function where the relation
between the type of an object program and that of its CPS transform is
captured in the type system of DML. In a broader context, we claim to have
taken a solid step along the line of research on constructing certifying
compilers.}
}


@INPROCEEDINGS{Xi:SBLP-2003,
  AUTHOR = {Hongwei Xi},
  TITLE = {Dependently Typed Pattern Matching},
  BOOKTITLE = {Proceedings of Simposio Brasileiro de Linguagens de Programacao},
  YEAR = {2003},
  MONTH = MAY,
  ADDRESS = {Ouro Preto, Brazil},
  CHURCHREPORT = {yes},
  POSTSCRIPT = {http://www.cs.bu.edu/~hwxi/academic/papers/sblp03.ps},
  PDF = {http://www.cs.bu.edu/~hwxi/academic/papers/sblp03.pdf},
  ABSTRACT = {The mechanism for declaring datatypes to model data structures in
functional programming languages such as Standard ML and Haskell can
offer both convenience in programming and clarity in code.  With the
introduction of dependent datatypes in DML, the programmer can model
data structures with more accuracy, thus capturing more program
invariants. In this paper, we study some practical aspects of dependent
datatypes that affect both type-checking and compiling pattern
matching.  The results, which have already been tested, demonstrate that
dependent datatype can not only offer various programming benefits but
also lead to performance gains, yielding a concrete case where safer
programs run faster.}
}


@INPROCEEDINGS{Xi:ASIA-PEPM-2002,
  AUTHOR = {Hongwei Xi},
  TITLE = {{Unifying Object-Oriented Programming with Typed Functional Programming}},
  BOOKTITLE = {Proceedings of ASIAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (ASIA-PEPM)},
  YEAR = 2002,
  MONTH = {September},
  PAGES = {117--125},
  ADDRESS = {Aizu-Wakamatsu, Japan},
  CHURCHREPORT = {yes},
  POSTSCRIPT = {http://www.cs.bu.edu/~hwxi/academic/papers/asia-pepm02.ps},
  PDF = {http://www.cs.bu.edu/~hwxi/academic/papers/asia-pepm02.pdf},
  ABSTRACT = {The wide practice of object-oriented programming in current software
construction is evident. Despite extensive studies on typing programming
objects, it is still undeniably a challenging research task to design a
type system for object-oriented programming that is both effective in
capturing program errors and unobtrusive to program construction.  In this
paper, we present a novel approach to typing objects that makes use of a
recently invented notion of guarded dependent datatypes. We show that our
approach can address various difficult issues (e.g., handling ``self''
type, typing binary methods, etc.) in a simple and natural type-theoretical
manner, remedying the deficiencies in many existing approaches to typing
objects.}
}


@INPROCEEDINGS{Taha+Ellner+Xi:EMSOFT-2003,
  AUTHOR = {Walid Taha and Stephan Ellner and Hongwei Xi},
  TITLE = {Generating Imperative, Heap-Bounded Programs in a Functional Setting},
  BOOKTITLE = {Proceedings of the Third International Conference on Embedded Software},
  PUBLISHER = {Springer-Verlag LNCS 2855},
  YEAR = {2003},
  MONTH = {October},
  ADDRESS = {Philadelphia, PA},
  PAGES = {340--355},
  CHURCHREPORT = {yes},
  POSTSCRIPT = {http://www.cs.bu.edu/~hwxi/academic/papers/emsoft03.ps},
  PDF = {http://www.cs.bu.edu/~hwxi/academic/papers/emsoft03.pdf},
  ABSTRACT = {
High-level programming languages offer significant expressivity but provide
little or no guarantees about resource utilization. Resource-bounded
languages provide strong guarantees about the runtime behavior of programs
but often lack mechanisms that allow programmers to write more structured,
modular, and reusable programs. To overcome this basic tension in language
design, this paper advocates taking into account the natural distinction
between the development platform and the deployment platform for
resource-sensitive software.  To illustrate this approach, we develop the
meta-theory for GeHB, a two-level language in which first stage
computations can involve arbitrary resource consumption, but the second
stage can only involve functional programs that do not require new heap
allocations. As an example of a such a second-stage language we use the
recently proposed first-order functional language LFPL. LFPL can be
compiled directly to malloc-free, imperative C code.  We show that all
generated programs in GeHB can be transformed into well-typed LFPL
programs, thus ensuring that the results established for LFPL are directly
applicable to GeHB
}
}


@ARTICLE{Xi:JUCS-2003,
  AUTHOR = {Hongwei Xi},
  TITLE = {Dependently Typed Pattern Matching},
  JOURNAL = {Journal of Universal Computer Science},
  VOLUME = {9},
  NUMBER = {8},
  YEAR = {2003},
  PAGES = {851-872},
  CHURCHREPORT = {yes},
  POSTSCRIPT = {http://www.cs.bu.edu/~hwxi/academic/papers/jucs03.ps},
  PDF = {http://www.cs.bu.edu/~hwxi/academic/papers/jucs03.pdf},
  ABSTRACT = {
The mechanism for declaring datatypes to model data structures in
programming languages such as Standard ML and Haskell can offer both
convenience in programming and clarity in code.  With the introduction of
dependent datatypes in DML, the programmer can model data structures with
more accuracy, thus capturing more program invariants.  In this paper, we
study some practical aspects of dependent datatypes that affect both
type-checking and compiling pattern matching.  The results, which have
already been tested, demonstrate that dependent datatype can not only offer
various programming benefits but also lead to performance gains, yielding a
concrete case where safer programs run faster.
}
}


@INPROCEEDINGS{Zhu+Xi:PADL-2005,
  AUTHOR = {Dengping Zhu and Hongwei Xi},
  TITLE = {Safe Programming with Pointers through Stateful Views},
  BOOKTITLE = {Proceedings of the 7th International Symposium on Practical Aspects of Declarative Languages},
  PUBLISHER = {Springer-Verlag LNCS},
  YEAR = {2005},
  MONTH = {January},
  PAGES = {TBA},
  ADDRESS = {Long Beach, CA},
  CHURCHREPORT = {yes},
  POSTSCRIPT = {http://cs-people.bu.edu/zhudp/pubs/PADL05.ps},
  PDF = {http://cs-people.bu.edu/zhudp/pubs/PADL05.pdf},
  ABSTRACT = {{
The need for direct memory manipulation through pointers is essential in
many applications. However, it is also commonly understood that the use (or
probably misuse) of pointers is often a rich source of program errors.
Therefore, approaches that can effectively enforce safe use of pointers in
programming are highly sought after.  ATS is a programming language with a
type system rooted in a recently developed framework Applied Type System,
and a novel and desirable feature in ATS lies in its support for safe
programming with pointers through a novel notion of {\em stateful
views}. In particular, even pointer arithmetic is allowed in ATS and
guaranteed to be safe by the type system of ATS.  In this paper, we give an
overview of this feature in ATS, presenting some interesting examples based
on a prototype implementation of ATS to demonstrate the practicality of
safe programming with pointer through stateful views.
}}
}


@INPROCEEDINGS{Zhu+Xi:APLAS-2003,
  AUTHOR = {Dengping Zhu and Hongwei Xi},
  TITLE = {A Typeful and Tagless Representation for XML Documents},
  BOOKTITLE = {Proceedings of the First Asian Symposium on Programming Languages and Systems},
  YEAR = 2003,
  MONTH = {November},
  ADDRESS = {Beijing, China},
  PAGES = {89-104},
  CHURCHREPORT = {yes},
  POSTSCRIPT = {http://cs-people.bu.edu/zhudp/pubs/aplas03.ps},
  PDF = {http://cs-people.bu.edu/zhudp/pubs/aplas03.pdf},
  ABSTRACT = {Abstract: When constructing programs to process XML documents, we immediately face
the question as to how XML documents should be represented internally in
the programming language we use.  Currently, most representations for XML
documents are typeless in the sense that the type information of an XML
document cannot be reflected in the type of the representation of the
document (if the representation is assumed to be typed). Though convenient
to construct, a typeless representation for XML documents often makes use
of a large number of representation tags, which not only require some
significant amount of space to store but may also incur numerous run-time
tag checks when the represented documents are processed. Moreover, with a
typeless representation for XML documents, it becomes difficult or even
impossible to statically capture program invariants that are related to the
type information of XML documents. Building upon our recent work on guarded
recursive datatypes, we present an approach to representing XML documents
in this paper that not only allows the type information of an XML document
to be reflected in the type of the representation of the document but also
significantly reduces the need for representation tags that are required in
typeless representations.  With this approach, we become able to process
XML documents in a typeful manner, thus reaping various well-known software
engineering benefits from the presence of types.}
}


@INPROCEEDINGS{Xi+Chen+Chen:POPL-2003,
  AUTHOR = {Hongwei Xi and Chiyan Chen and Gang Chen},
  TITLE = {Guarded Recursive Datatype Constructors},
  BOOKTITLE = {Proceedings of the 30th ACM SIGPLAN Symposium on Principles of Programming Languages},
  YEAR = 2003,
  MONTH = {January},
  ADDRESS = {New Orleans},
  PAGES = {224--235},
  CHURCHREPORT = {yes},
  POSTSCRIPT = {http://www.cs.bu.edu/~hwxi/academic/papers/popl03.ps},
  PDF = {http://www.cs.bu.edu/~hwxi/academic/papers/popl03.pdf},
  ABSTRACT = {Abstract: We introduce a notion of guarded recursive (g.r.) datatype
constructors, generalizing the notion of recursive datatypes in functional
programming languages such as ML and Haskell. We address both theoretical
and pragmatic issues resulted from this generalization. On one hand, we
design a type system to formalize the notion of g.r. datatype constructors
and then prove the soundness of the type system. On the other hand, we
present some significant applications (e.g., implementing objects,
implementing staged computation, etc.) of g.r. datatype constructors,
arguing that g.r. datatype constructors can have far-reaching consequences
in programming. The main contribution of the paper lies in the recognition
and then the formalization of a programming notion that is of both
theoretical interest and practical use.}
}


@UNPUBLISHED{Wel+Plu+Kam:DMP-2003,
  AUTHOR = {J. B. Wells and Detlef Plump and Fairouz Kamareddine},
  TITLE = {Diagrams for Meaning Preservation},
  NOTE = {Long version of \cite{Wel+Plu+Kam:RTA-2003}},
  MONTH = APR,
  YEAR = 2003,
  CHURCHREPORT = {yes},
  PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Wells+Plump+Kamareddine:Diagrams-for-Meaning-Preservation:2003-04-16.pdf},
  ABSTRACT = {This paper presents an abstract framework and
                  multiple diagram-based methods for proving
                  \emph{meaning preservation}, i.e., that all rewrite
                  steps of a rewriting system preserve the meaning
                  given by an operational semantics based on a
                  rewriting strategy.  While previous rewriting-based
                  methods have generally needed the treated rewriting
                  system as a whole to have such properties as, e.g.,
                  \emph{confluence}, \emph{standardization}, and/or
                  \emph{termination} or \emph{boundedness} of
                  \emph{developments}, our methods can work when
                  \emph{all} of these conditions fail, and thus can
                  handle more rewriting systems.  We isolate the new
                  \emph{lift/project with termination} diagram as the
                  key proof idea and show that previous
                  rewriting-based methods (Plotkin's method based on
                  \emph{confluence} and \emph{standardization} and
                  Machkasova and Turbak's method based on distinct
                  \emph{lift} and \emph{project} properties)
                  implicitly use this diagram.  Furthermore, our
                  framework and proof methods help reduce the proof
                  burden substantially by, e.g., supporting separate
                  treatment of partitions of the rewrite steps,
                  needing only \emph{elementary diagrams} for rewrite
                  step interactions, excluding many rewrite step
                  interactions from consideration, needing weaker
                  termination properties, and providing generic
                  support for using developments in combination with
                  any method.}
}


@INPROCEEDINGS{Wel+Plu+Kam:RTA-2003,
  AUTHOR = {J. B. Wells and Detlef Plump and Fairouz Kamareddine},
  TITLE = {Diagrams for Meaning Preservation},
  NOTE = {A long version is \cite{Wel+Plu+Kam:DMP-2003}},
  CROSSREF = {RTA2003},
  PAGES = {88--106},
  CHURCHREPORT = {yes},
  PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Wells+Plump+Kamareddine:Diagrams-for-Meaning-Preservation:RTA-2003.pdf},
  ABSTRACT = {This paper presents an abstract framework and
                  multiple diagram-based methods for proving
                  \emph{meaning preservation}, i.e., that all rewrite
                  steps of a rewriting system preserve the meaning
                  given by an operational semantics based on a
                  rewriting strategy.  While previous rewriting-based
                  methods have generally needed the treated rewriting
                  system as a whole to have such properties as, e.g.,
                  \emph{confluence}, \emph{standardization}, and/or
                  \emph{termination} or \emph{boundedness} of
                  \emph{developments}, our methods can work when
                  \emph{all} of these conditions fail, and thus can
                  handle more rewriting systems.  We isolate the new
                  \emph{lift/project with termination} diagram as the
                  key proof idea and show that previous
                  rewriting-based methods (Plotkin's method based on
                  \emph{confluence} and \emph{standardization} and
                  Machkasova and Turbak's method based on distinct
                  \emph{lift} and \emph{project} properties)
                  implicitly use this diagram.  Furthermore, our
                  framework and proof methods help reduce the proof
                  burden substantially by, e.g., supporting separate
                  treatment of partitions of the rewrite steps,
                  needing only \emph{elementary diagrams} for rewrite
                  step interactions, excluding many rewrite step
                  interactions from consideration, needing weaker
                  termination properties, and providing generic
                  support for using developments in combination with
                  any method.}
}


@MISC{Chen:JLC-2003,
  AUTHOR = {Gang Chen},
  TITLE = {Soundness of Coercion in the Calculus of Constructions },
  CHURCHREPORT = {yes},
  KEYWORDS = {Subtyping, coersion, Calculus of Constructions },
  CHURCHREPORT = {yes},
  XPOSTSCRIPT = {http://www.church-project.org/reports/electronic/Chen:JLC-2003.ps.gz},
  XURL = {http://www.church-project.org/reports/electronic/Chen:JLC-2003.pdf.gz},
  XPDF = {http://www.church-project.org/reports/electronic/Chen:JLC-2003.pdf},
  ABSTRACT = {We present a coercive subtyping system for the calculus of constructions. The proposed system $\lambda C_{\leq}^{co}$ is obtained essentially by adding coercions and $\eta$-conversion to $\lambda C_\leq$\cite{Chen97a}, which is a subtyping extension to the calculus of constructions without coercions. We proved that a coercion $c : A \leq B$ is semantically sound. That is, 1) $c$ is a term of type $A\to B$; 2) $c$ behaves like an identity function. This development follows the spirit of  semantical interpretation of subtyping in \cite{LMS95,LMS98}.},
  NOTE = {To appear in Journal of Logic and Computation}
}


@INPROCEEDINGS{Chen:POPL-2003,
  AUTHOR = {Gang Chen},
  TITLE = {Coercive Subtyping for the Calculus of Constructions
                  (extended abstract) },
  CHURCHREPORT = {yes},
  CROSSREF = {POPL2003},
  KEYWORDS = {Subtyping, coersion, Calculus of Constructions },
  CHURCHREPORT = {yes},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Chen:POPL-2003.ps.gz},
  URL = {http://www.church-project.org/reports/electronic/Chen:POPL-2003.pdf.gz},
  PDF = {http://www.church-project.org/reports/electronic/Chen:POPL-2003.pdf},
  ABSTRACT = {We present a coercive subtyping system for the calculus of
                  constructions. The proposed system $\lambda C_{\leq}^{co}$ is obtained
                  essentially by adding coercions and $\eta$-conversion to
                  $\lambda C_\leq$\cite{Chen97a}, which is a subtyping
                  extension to the calculus of constructions without
                  coercions. Following \cite{LMS95,LMS98}, the coercive
                  subtyping $c : A \leq B$ is understood as a special case
                  of typing in arrow type $c : A \to B$ such that the term
                  $c$ behaves like an identity function. We prove that,
                  with respect to this semantic interpretation, the
                  proposed coercive subtyping system is sound and complete,
                  and that this completeness leads to transitivity
                  elimination.  In addition, we establish the equivalence
                  between $\lambda C_{\leq}^{co}$ and $\lambda C_{\beta \eta}$, this fact implies that
                  $\lambda C_{\leq}^{co}$ has confluence, subject reduction and strong
                  normalization. We propose a formalization of coercion
                  inference problem and present a sound and complete
                  coercion inference algorithm.}
}


@INPROCEEDINGS{Chen:PPDP-2002,
  AUTHOR = {Gang Chen},
  TITLE = {Full Integration of Subtyping and If-expression},
  CROSSREF = {PPDP2002},
  KEYWORDS = {Subtyping, If-expression, Java, Programming Language},
  CHURCHREPORT = {yes},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Chen:PPDP-2002.ps.gz},
  URL = {http://www.church-project.org/reports/electronic/Chen:PPDP-2002.pdf.gz},
  PDF = {http://www.church-project.org/reports/electronic/Chen:PPDP-2002.pdf},
  ABSTRACT = {The combination of full subsumption and conditional
                  expression is a challenging problem, because in such a
                  system, a term might not have a type which is a
                  representative of all types of the term. Therefore, the
                  traditional type checking technique fails. Due to such a
                  difficulty, Java typing rule for if-expression uses only
                  a restricted form of subtyping. In this paper, we propose
                  a type system which includes both of the above mentioned
                  features and enjoys decidable type checking. We also show
                  that the system has the subject reduction property. It is
                  expected that this technique could be used to improve the
                  type system of Java with full subsumption. }
}


@TECHREPORT{Amt+Wel:MPD-2002,
  AUTHOR = {Torben Amtoft and J. B. Wells},
  TITLE = {Mobile Processes with Dependent Communication Types
                  and Singleton Types for Names and Capabilities},
  MONTH = DEC,
  YEAR = 2002,
  INSTITUTION = {Kansas State University, Department of Computing and
                  Information Sciences},
  NUMBER = {2002-3},
  URL = {http://www.cis.ksu.edu/~schmidt/techreport/2002.list.html},
  PDF = {http://www.cis.ksu.edu/~tamtoft/Papers/Amt+Wel:MPwDCT-2002/short.pdf},
  XNOTE = {Torben has replaced the file supposed linked to as
                  KSU CIS TR 2002-3 with a later version which was
                  submitted to SAS '03.  The original KSU CIS TR
                  2002-03 is no longer available!!!  It might be
                  possible to reconstruct something like it via CVS
                  time travel, but it would be a pain.
                  Torben, 02/07/04: the link now again points to
                   the original report!!},
  DARTREPORT = {yes},
  CHURCHREPORT = {yes},
  ABSTRACT = {There are many calculi for reasoning about
                  concurrent communicating processes which have
                  locations and are mobile. Examples include the
                  original Ambient Calculus and its many variants, the
                  Seal Calculus, the MR-calculus, the M-calculus,
                  etc. It is desirable to use such calculi to describe
                  the behavior of mobile agents. It seems reasonable
                  that mobile agents should be able to follow
                  non-predetermined paths and to carry
                  non-predetermined types of data from location to
                  location, collecting and delivering this data using
                  communication primitives. Previous type systems for
                  ambient calculi make this difficult or impossible to
                  express, because these systems (if they handle
                  communication at all) have always globally mapped
                  each ambient name to a type governing the type of
                  values that can be communicated locally or with
                  adjacent locations, and this type can not depend on
                  where the ambient has traveled. \par We present a
                  new type system where there are no global
                  assignments of types to ambient names. Instead, the
                  type of an ambient process $P$ not only indicates
                  what can be locally communicated but also gives an
                  upper bound on the possible ambient nesting shapes
                  of any process $P'$ to which $P$ can evolve, as well
                  as the possible capabilities and names that can be
                  exhibited or communicated at each location. Because
                  these shapes can depend on which capabilities and
                  names are actually communicated, the types support
                  this with explicit dependencies on
                  communication. This system is thus the first type
                  system for an ambient calculus which provides type
                  polymorphism of the kind that is usually present in
                  polymorphic type systems for the
                  $\lambda$-calculus.}
}


@TECHREPORT{Mak+Wel:TIP-2004,
  AUTHOR = {Henning Makholm and J. B. Wells},
  TITLE = {Type Inference for {PolyA}},
  YEAR = 2004,
  MONTH = JAN,
  CHURCHREPORT = {yes},
  DARTREPORT = {yes},
  DISABLEDPDF = {http://www.macs.hw.ac.uk:8080/techreps/docs/files/HW-MACS-TR-0013.pdf},
  PDF = {http://www.macs.hw.ac.uk/DART/reports/D2.3/MW04.pdf},
  INSTITUTION = {Heriot-Watt Univ., School of Math.\ \& Comput.\
                  Sci.},
  NUMBER = {HW-MACS-TR-0013},
  ABSTRACT = {We present an automatic type inference algorithm for
                  PolyA, a type system for Mobile Ambients presented
                  in earlier work by us together with Torben
                  Amtoft.  We present not only a basic inference
                  algorithm, but also several optimizations to it
                  aimed at reducing the size of the inferred
                  types.  The final algorithm has been implemented and
                  verified to work on small examples.  We discuss some
                  small problems that still exist and methods for
                  solving them.}
}


@TECHREPORT{Amt+Mak+Wel:PolyA-2004a,
  AUTHOR = {Torben Amtoft and Henning Makholm and J. B. Wells},
  TITLE = {{PolyA}: True Type Polymorphism for {M}obile
                  {A}mbients},
  YEAR = 2004,
  MONTH = FEB,
  INSTITUTION = {Heriot-Watt Univ., School of Math.\ \& Comput.\
                  Sci.},
  NUMBER = {HW-MACS-TR-0015},
  PDF = {http://www.macs.hw.ac.uk:8080/techreps/docs/files/HW-MACS-TR-0015.pdf},
  CHURCHREPORT = {yes},
  DARTREPORT = {yes},
  NOTE = {A shorter successor is \cite{Amt+Mak+Wel:TCS-2004}},
  ABSTRACT = {Previous type systems for mobility calculi (the
                  original Mobile Ambients, its variants and
                  descendants, e.g., Boxed Ambients and Safe Ambients,
                  and other related systems) offer little support for
                  generic mobile agents.  Previous systems either do
                  not handle communication at all or globally assign
                  fixed communication types to ambient names that do
                  not change as an ambient moves around or interacts
                  with other ambients.  This makes it hard to type
                  examples such as a ``messenger'' ambient that uses
                  communication primitives to collect a message of
                  non-predetermined type and deliver it to a
                  non-predetermined destination.
                  \par
                  In contrast, we present our new type system
                  $\mathsf{PolyA}$.  Instead of assigning communication
                  types to ambient names, $\mathsf{PolyA}$ assigns a
                  type to each process $P$ that gives upper bounds on
                  (1) the possible ambient nesting shapes of any
                  process $P'$ to which $P$ can evolve, (2) the values
                  that may be communicated at each location, and (3)
                  the capabilities that can be used at each
                  location.  Because $\mathsf{PolyA}$ can type generic
                  mobile agents, we believe $\mathsf{PolyA}$ is the
                  first type system for a mobility calculus that
                  provides type polymorphism comparable in power to
                  polymorphic type systems for the
                  $\lambda$-calculus.  $\mathsf{PolyA}$ is easily
                  extended to ambient calculus variants.  A restriction
                  of $\mathsf{PolyA}$ has principal typings.}
}


@INPROCEEDINGS{Amt+Mak+Wel:TCS-2004,
  CHURCHREPORT = {yes},
  DARTREPORT = {yes},
  AUTHOR = {Torben Amtoft and Henning Makholm and J. B. Wells},
  TITLE = {{PolyA}: True Type Polymorphism for {M}obile
                  {A}mbients},
  CROSSREF = {TCS2004},
  PAGES = {591--604},
  PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Amtoft+Makholm+Wells:PolyA:True-Type-Polymorphism-for-Mobile-Ambients:TCS-2004.pdf},
  NOTE = {A more detailed predecessor is
                  \cite{Amt+Mak+Wel:PolyA-2004a}},
  ABSTRACT = {Previous type systems for mobility calculi (the
                  original Mobile Ambients, its variants and
                  descendants, e.g., Boxed Ambients and Safe Ambients,
                  and other related systems) offer little support for
                  generic mobile agents.  Previous systems either do
                  not handle communication at all or globally assign
                  fixed communication types to ambient names that do
                  not change as an ambient moves around or interacts
                  with other ambients.  This makes it hard to type
                  examples such as a ``messenger'' ambient that uses
                  communication primitives to collect a message of
                  non-predetermined type and deliver it to a
                  non-predetermined destination.
                  \par
                  In contrast, we present our new type system
                  $\mathsf{PolyA}$.  Instead of assigning communication
                  types to ambient names, $\mathsf{PolyA}$ assigns a
                  type to each process $P$ that gives upper bounds on
                  (1) the possible ambient nesting shapes of any
                  process $P'$ to which $P$ can evolve, (2) the values
                  that may be communicated at each location, and (3)
                  the capabilities that can be used at each
                  location.  Because $\mathsf{PolyA}$ can type generic
                  mobile agents, we believe $\mathsf{PolyA}$ is the
                  first type system for a mobility calculus that
                  provides type polymorphism comparable in power to
                  polymorphic type systems for the
                  $\lambda$-calculus.  $\mathsf{PolyA}$ is easily
                  extended to ambient calculus variants.  A restriction
                  of $\mathsf{PolyA}$ has principal typings.}
}


@TECHREPORT{Mak+Wel:PolyStar-2004,
  AUTHOR = {Henning Makholm and J. B. Wells},
  TITLE = {Instant Polymorphic Type Systems for Mobile Process
                  Calculi: Just Add Reduction Rules and Close},
  YEAR = 2004,
  MONTH = NOV,
  CHURCHREPORT = {yes},
  DARTREPORT = {yes},
  INSTITUTION = {Heriot-Watt Univ., School of Math.\ \& Comput.\
                  Sci.},
  NUMBER = {HW-MACS-TR-0022},
  XNOTE = {Available at http://www.macs.hw.ac.uk:8080/},
  PDF = {http://www.macs.hw.ac.uk:8080/techreps/docs/files/HW-MACS-TR-0022.pdf},
  NOTE = {A shorter successor is~\cite{Mak+Wel:ESOP-2005}},
  ABSTRACT = {Many different \emph{mobile process calculi} have
                  been invented, and for each some number of type
                  systems has been developed.  Soundness and other
                  properties must be proved separately for each
                  calculus and type system.
                  \par
                  We present the \emph{generic} polymorphic type
                  system Poly$\star$ which works for a wide
                  range of mobile process calculi.  For any calculus
                  satisfying some general syntactic conditions,
                  well-formedness rules for types are derived
                  automatically from the reduction rules and
                  Poly$\star$ works otherwise unchanged.  The
                  derived type system is automatically sound and often
                  more precise than previous type systems for the
                  calculus, due to Poly$\star$'s
                  \emph{spatial polymorphism}.
                  \par
                  We present an implemented type inference algorithm
                  for Poly$\star$ which automatically
                  constructs a typing given a set of reduction rules
                  and a term to be typed.  The generated typings are
                  \emph{principal} with respect to certain natural
                  type shape constraints.}
}


@INPROCEEDINGS{Mak+Wel:ESOP-2005,
  AUTHOR = {Henning Makholm and J. B. Wells},
  TITLE = {Instant Polymorphic Type Systems for Mobile Process
                  Calculi: Just Add Reduction Rules and Close},
  CHURCHREPORT = {yes},
  DARTREPORT = {yes},
  CROSSREF = {ESOP2005},
  PAGES = {389--407},
  NOTE = {A more detailed predecessor is
                  \cite{Mak+Wel:PolyStar-2004}},
  PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Makholm+Wells:Instant-Polymorphic-Type-Systems-for-Mobile-Process-Calculi:ESOP-2005.pdf},
  ABSTRACT = {Many different \emph{mobile process calculi} have
                  been invented, and for each some number of type
                  systems has been developed.  Soundness and other
                  properties must be proved separately for each
                  calculus and type system.  We present the
                  \emph{generic} polymorphic type system
                  Poly$\star$ which works for a wide range of
                  mobile process calculi, including the $\pi$-calculus
                  and Mobile Ambients.  For any calculus satisfying
                  some general syntactic conditions, well-formedness
                  rules for types are derived automatically from the
                  reduction rules and Poly$\star$ works
                  otherwise unchanged.  The derived type system is
                  automatically sound (i.e., has subject reduction)
                  and often more precise than previous type systems
                  for the calculus, due to Poly$\star$'s
                  \emph{spatial polymorphism}.  We present an
                  implemented type inference algorithm for
                  Poly$\star$ which automatically constructs
                  a typing given a set of reduction rules and a term
                  to be typed.  The generated typings are
                  \emph{principal} with respect to certain natural
                  type shape constraints.}
}


@INPROCEEDINGS{Mak+Wel:ICFP-2005,
  AUTHOR = {Henning Makholm and J. B. Wells},
  TITLE = {Type Inference, Principal Typings, and
                  Let-Polymorphism for First-Class Mixin Modules},
  CROSSREF = {ICFP2005},
  CHURCHREPORT = {yes},
  DARTREPORT = {yes},
  PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Makholm+Wells:Type-Inference,-Principal-Typings,-and-Let-Polymorphism-for-First-Class-Mixin-Modules:ICFP-2005.pdf},
  PAGES = {156--167},
  ABSTRACT = {A \emph{mixin module} is a programming abstraction
                  that simultaneously generalizes
                  $\lambda$-abstractions, records, and mutually
                  recursive definitions. Although various mixin module
                  type systems have been developed, no one has
                  investigated \emph{principal typings} or developed
                  \emph{type inference} for first-class mixin modules,
                  nor has anyone added Milner's
                  \emph{let-polymorphism} to such a system.
                  \par
                  This paper proves that typability is NP-complete for
                  the naive approach followed by previous mixin module
                  type systems. Because a $\lambda$-calculus extended
                  with \emph{record concatenation} is a simple
                  restriction of our mixin module calculus, we also
                  prove the folk belief that typability is NP-complete
                  for the naive early type systems for record
                  concatenation.
                  \par
                  To allow feasible type inference, we present
                  \textsf{Martini}, a new system of \emph{simple
                  types} for mixin modules with \emph{principal
                  typings}. \textsf{Martini} is conceptually simple,
                  with no subtyping and a clean and balanced
                  separation between unification-based type inference
                  with type and row variables and constraint solving
                  for safety of linking and field extraction. We have
                  implemented a type inference algorithm and we prove
                  its complexity to be $O(n^2)$, or $O(n)$ given a
                  fixed bound on the number of field
                  labels. (Technically, there is also a factor of
                  $\alpha(n)$, but $\alpha(n)\leq 4$ for
                  $n<10^{10^{100}}$ (a ``googolplex'').) To prove the
                  complexity, we need to present an algorithm for
                  \emph{row unification} that may have been
                  implemented by others, but which we could not find
                  written down anywhere. Because \textsf{Martini} has
                  principal typings, we successfully extend it with
                  Milner's let-polymorphism.}
}


@INPROCEEDINGS{Haa+Wel:ESOP-2003,
  ITRSPAPER = {yes},
  AUTHOR = {Christian Haack and J. B. Wells},
  TITLE = {Type Error Slicing in Implicitly Typed Higher-Order
                  Languages},
  YEAR = 2003,
  CROSSREF = {ESOP2003},
  PAGES = {284--301},
  CHURCHREPORT = {yes},
  NOTE = {Superseded by \cite{Haa+Wel:SCP-2004-v50}},
  DARTREPORT = {yes},
  XDARTREPORT = {not a DART paper, although its journal version is part of a deliverable},
  PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Haack+Wells:Type-Error-Slicing-in-Implicitly-Typed-Higher-Order-Languages:ESOP-2003.pdf},
  ABSTRACT = {Previous methods have generally identified the
                  location of a type error as a particular program
                  point or the program subtree rooted at that
                  point. We present a new approach that identifies the
                  location of a type error as a set of program
                  points (a \emph{slice}) all of which are necessary
                  for the type error. We describe algorithms for
                  finding minimal type error slices for implicitly typed
                  higher-order languages like Standard ML.}
}


@ARTICLE{Haa+Wel:SCP-2004-v50,
  ITRSPAPER = {yes},
  AUTHOR = {Christian Haack and J. B. Wells},
  TITLE = {Type Error Slicing in Implicitly Typed Higher-Order
                  Languages},
  JOURNAL = {Sci.\ Comput.\ Programming},
  DARTREPORT = {yes},
  VOLUME = 50,
  PAGES = {189--224},
  YEAR = 2004,
  PDFTODO = {*** rename this file ***},
  PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Haack+Wells:Type-Error-Slicing-in-Implicitly-Typed-Higher-Order-Languages:SCP-ta.pdf},
  CHURCHREPORT = {yes},
  NOTE = {Supersedes \cite{Haa+Wel:ESOP-2003}},
  DOIHTTP = {http://dx.doi.org/10.1016/j.scico.2004.01.004},
  DOI = {doi:10.1016/j.scico.2004.01.004},
  ABSTRACT = {Previous methods have generally identified the
                  location of a type error as a particular program
                  point or the program subtree rooted at that
                  point. We present a new approach that identifies the
                  location of a type error as a set of program points
                  (a \emph{slice}) all of which are necessary for the
                  type error. We identify the criteria of
                  \emph{completeness} and \emph{minimality} for type
                  error slices. We discuss the advantages of complete
                  and minimal type error slices over previous methods
                  of presenting type errors. We present and prove the
                  correctness of algorithms for finding complete and
                  minimal type error slices for implicitly typed
                  higher-order languages like Standard~ML.}
}


@INPROCEEDINGS{Carlier:ITRS-2002,
  ITRSPAPER = {yes},
  AUTHOR = {S{\'e}bastien Carlier},
  TITLE = {Polar Type Inference with Intersection Types and
                  $\omega$},
  CROSSREF = {ITRS2002},
  POSTSCRIPT = {http://www.macs.hw.ac.uk/~sebc/carlier-ptiio.ps.gz},
  CHURCHREPORT = {yes},
  NOTEREMARK = {The note field is blank to suppress the note field from ITRS2002.},
  NOTE = {},
  ABSTRACT = {We present a type system featuring intersection
                  types and $\omega$, a type constant which is
                  assigned to unused terms.  We exploit and extend the
                  technology of expansion variables from the recently
                  developed System I, with which we believe our system
                  shares many interesting properties, such as strong
                  normalization, principal typings, and compositional
                  analysis.  Our presentation emphasizes a polarity
                  discipline and shows its benefits.  We syntactically
                  distinguish positive and negative types, and give
                  them different interpretations.  We take the point of
                  view that the interpretation of a type is intrinsic
                  to it, and should not change implicitly when it
                  appears at the opposite polarity.  Our system is the
                  result of a process which started with an extension
                  of Trevor Jim's Polar Type System.}
}


@INPROCEEDINGS{Kfo+Was+Wel:ITRS-2002,
  ITRSPAPER = {yes},
  AUTHOR = {Assaf J. Kfoury and Geoff Washburn and J. B. Wells},
  TITLE = {Implementing Compositional Analysis Using
                  Intersection Types With Expansion Variables},
  CROSSREF = {ITRS2002},
  NOTEREMARK = {The note field is blank to suppress the note field from ITRS2002.},
  NOTE = {},
  DARTREPORT = {yes},
  CHURCHREPORT = {yes},
  NONEXISTENTDVI = {http://www.church-project.org/reports/electronic/Kfo+Was+Wel:ITRS-2002.dvi},
  PDF = {http://www.church-project.org/reports/electronic/Kfo+Was+Wel:ITRS-2002.pdf},
  ELSEVIERURLB = {http://www.elsevier.nl/gej-ng/31/29/23/125/51/show/Products/notes/index.htt},
  ELSEVIERURLA = {http://www.elsevier.nl/locate/entcs/volume70.html},
  ABSTRACT = {A program analysis is \emph{compositional} when the analysis
result for a particular program fragment is obtained solely from the
results for its immediate subfragments via some composition operator.  This
means the subfragments can be analyzed independently in any order.  Many
commonly used program analysis techniques (in particular, most abstract
interpretations and most uses of the Hindley/Milner type system) are not
compositional and require the entire text of a program for sound and
complete analysis.  \par System I is a recent type system for the pure
$\lambda$-calculus with intersection types and the new technology of
expansion variables.  System I supports compositional analysis because it
has the \emph{principal typings} property and an algorithm based on the new
technology of $\beta$-unification has been developed that finds these
principal typings.  In addition, for each natural number $k$, typability in
the rank-$k$ restriction of System I is decidable, so a complete and
terminating analysis algorithm exists for the rank-$k$ restriction.  \par
This paper presents new understanding that has been gained from working
with multiple implementations of System I and $\beta$-unification-based
analysis algorithms.  The previous literature on System I presented the
type system in a way that helped in proving its more important theoretical
properties, but was not as easy for implementers to follow as it could be.
This paper provides a presentation of many aspects of System I that should
be clearer as well as a discussion of important implementation issues.}
}


@INPROCEEDINGS{Car+Pol+Wel+Kfo:ESOP-2004,
  ITRSPAPER = {yes},
  CHURCHREPORT = {yes},
  DARTREPORT = {yes},
  AUTHOR = {S{\'e}bastien Carlier and Jeff Polakow and
                  J. B. Wells and A. J. Kfoury},
  TITLE = {{S}ystem {E}: Expansion Variables for Flexible Typing
                  with Linear and Non-linear Types and Intersection
                  Types},
  CROSSREF = {ESOP2004},
  PAGES = {294--309},
  PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Carlier+Polakow+Wells+Kfoury:System-E:ESOP-2004.pdf},
  ALTPDF = {http://www.macs.hw.ac.uk/DART/reports/D2.3/CPWK04.pdf},
  ABSTRACT = {Types are often used to control and analyze computer
                  programs.  Intersection types give a type system
                  great flexibility, but have been difficult to
                  implement.  The $!$ operator, used to distinguish
                  between linear and non-linear types, has good
                  potential for improving tracking of resource usage,
                  but has not been as flexible as one might want and
                  has been difficult to use in compositional
                  analysis.  We introduce System~E, a type system with
                  expansion variables, linear intersection types, and
                  the $!$ type constructor for creating non-linear
                  types.  System~E is designed for maximum flexibility
                  in automatic type inference and for ease of
                  automatic manipulation of type
                  information.  Expansion variables allow postponing
                  the choice of which typing rules to use until later
                  constraint solving gives enough information to allow
                  making a good choice.  System~E removes many
                  limitations and technical difficulties that
                  expansion variables had in the earlier System~I and
                  extends expansion variables to work with $!$ in
                  addition to the intersection type constructor.  We
                  present subject reduction results for call-by-need
                  evaluation and discuss approaches for implementing
                  program analysis in System~E.}
}


@INPROCEEDINGS{Car+Wel:PPDP-2004,
  ITRSPAPER = {yes},
  CHURCHREPORT = {yes},
  DARTREPORT = {yes},
  AUTHOR = {S{\'e}bastien Carlier and J. B. Wells},
  TITLE = {Type Inference with Expansion Variables and
                  Intersection Types in {S}ystem~{E} and an Exact
                  Correspondence with $\beta$-Reduction},
  PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Carlier+Wells:Type-Inference-with-Expansion-Variables-and-Intersection-Types-in-System-E-and-an-Exact-Correspondence-with-Beta-Reduction:PPDP-2004.pdf},
  CROSSREF = {PPDP2004},
  XPAGES = {132--143},
  NOTE = {Completely supersedes \cite{Car+Wel:TIEV-2004}},
  ABSTRACT = {System~E is a recently designed type system for the
                  $\lambda$-calculus with intersection types and
                  \emph{expansion variables}.  During automatic type
                  inference, expansion variables allow postponing
                  decisions about which non-syntax-driven typing rules
                  to use until the right information is available and
                  allow implementing the choices via substitution.
                  \par
                  This paper uses expansion variables in a
                  unification-based automatic type inference algorithm
                  for System~E that succeeds for every
                  $\beta$-normalizable $\lambda$-term.  We have
                  implemented and tested our algorithm and released
                  our implementation publicly.  Each step of our
                  unification algorithm corresponds to exactly one
                  $\beta$-reduction step, and \emph{vice versa}.  This
                  formally verifies and makes precise a step-for-step
                  correspondence between type inference and
                  $\beta$-reduction.  This also shows that type
                  inference with intersection types and expansion
                  variables can, in effect, carry out an arbitrary
                  amount of partial evaluation of the program being
                  analyzed.}
}


@UNPUBLISHED{Car+Wel:AOE-2008,
  ITRSPAPER = {yes},
  CHURCHREPORT = {yes},
  AUTHOR = {S{\'e}bastien Carlier and J. B. Wells},
  TITLE = {The Algebra of Expansion},
  NOTE = {Draft corresponding roughly to an ITRS 2008 workshop
                  talk},
  MONTH = MAR,
  DATE = {2008-03-25},
  YEAR = 2008,
  PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Carlier+Wells:The-Algebra-of-Expansion:2008-03-25.pdf},
  ABSTRACT = {Expansion is an operation on typings (pairs of type
                  environments and result types) in type systems for
                  the $\lambda$-calculus.  Expansion was originally
                  introduced for calculating possible typings of a
                  term in systems with intersection types.
                  Unfortunately, definitions of expansion (even the
                  most modern ones) have been difficult for outsiders
                  to absorb.  This paper aims to clarify expansion and
                  make it more accessible to non-specialists by
                  isolating the pure notion of expansion on its own,
                  independent of type systems and types.  We show how
                  expansion can be seen as a simple algebra on terms
                  with variables, substitutions, composition, and
                  miscellaneous constructors such that the algebra
                  satisfies 8 simple axioms and axiom schemas: the 3
                  standard axioms of a monoid, 4 standard axioms or
                  axiom schemas of substitutions (including one that
                  corresponds to the usual ``substitution lemma''),
                  and 1 axiom schema for expansion itself.  This
                  presentation should help make more accessible to a
                  wider community theory and techniques involving
                  intersection types and type inference with flexible
                  precision.}
}


@INPROCEEDINGS{Tur+Wel:PPDP-2001,
  AUTHOR = {Franklyn Turbak and J. B. Wells},
  TITLE = {Cycle Therapy: A Prescription for Fold and Unfold on
                  Regular Trees},
  CROSSREF = {PPDP2001},
  PAGES = {137--149},
  PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Turbak+Wells:Cycle-Therapy:A-Prescription-for-Fold-and-Unfold-on-Regular-Trees:PPDP-2001.pdf},
  CHURCHREPORT = {yes},
  DOCUMENTURL = {http://www.church-project.org/reports/Tur+Wel:PPDP-2001.html},
  OVERHEADSURL = {http://cs.wellesley.edu/~fturbak/talks/cycle-therapy.pdf},
  OVERHEADSCOMMENT = {to make printable version: {pdf2ps
                  cycle-therapy.{pdf,ps}} then "psnup -b1cm -c
                  -w20.99cm -h29.7cm -W29.7cm -H20.99cm -4
                  cycle-therapy.ps{,-4up}"},
  ABSTRACT = {Cyclic data structures can be tricky to create and
                  manipulate in declarative programming languages.  In
                  a declarative setting, a natural way to view cyclic
                  structures is as denoting \emph{regular} trees,
                  those trees which may be infinite but have only a
                  finite number of distinct subtrees.  This paper shows
                  how to implement the \emph{unfold}
                  (\emph{anamorphism}) operator in both eager and lazy
                  languages so as to create cyclic structures when the
                  result is a regular tree as opposed to merely
                  infinite lazy structures.  The usual \emph{fold}
                  (\emph{catamorphism}) operator when used with a
                  strict combining function on any infinite tree
                  yields an undefined result.  As an alternative, this
                  paper defines and show how to implement a
                  \emph{cycfold} operator with more useful semantics
                  when used with a strict function on cyclic
                  structures representing regular trees.  This paper
                  also introduces an abstract data type
                  (\emph{cycamores}) to simplify the use of cyclic
                  structures representing regular trees in both eager
                  and lazy languages.  Implementions of cycamores in
                  both SML and Haskell are presented.}
}


@PHDTHESIS{Per:PhD-2001,
  AUTHOR = {Santiago M. Pericas-Geertsen},
  TITLE = {XML-Fluent Mobile Ambients},
  INSTITUTION = {{Ph.D. Thesis} Comp.\ Sci.\ Dept., Boston Univ.},
  SCHOOL = {Boston University},
  YEAR = 2001,
  PDF = {http://cs-people.bu.edu/santiago/Papers/Per:PhD-2001.pdf},
  POSTSCRIPT = {http://cs-people.bu.edu/santiago/Papers/Per:PhD-2001.ps},
  CHURCHREPORT = {yes},
  ABSTRACT = {
 The Internet is considered to be among the greatest inventions of the
 twentieth century. Despite its immense importance we, programming language
 designers, have yet to propose a programming language that can exploit a
 network that spans the entire globe.
 In this thesis, we introduce a language for a programming model based on
 XML-speaking mobile agents. The thesis is divided into three parts: the
 first part defines the mobility aspect of the language, the second
 part introduces a typed calculus for manipulating XML documents, and the
 third part proposes a way of integrating these two calculi. The final goal
 is to design a typed language in which computation can be carried out by
 mobile agents exchanging data in the form of XML documents.
 The Ambient Calculus was developed by Cardelli and Gordon as a formal
 framework to study issues of mobility and migrant. In Part I, we consider
 an extension to the Ambient Calculus where ambients are equipped with a set
 of local channels over which processes can communicate. This extension
 incorporates certain features from the Pi-Calculus, such as the ability
 to communicate over higher-order channels, but without violating design
 principles of the Ambient Calculus (e.g., that two processes are unable to
 communicate if located in different administrative domains). For the
 extended calculus, we introduce an appropriate operational semantics and a
 provably sound type system. We conclude this part by showing an encoding
 of the Ambient Calculus into our calculus that is both semantics
 preserving and type preserving.
 XML is a simple and portable way of representing structured data in the
 form of trees.  It is an ideal language for machine-to-machine (or
 peer-to-peer) exchange of data because (i) it is portable, so there is no
 need to worry about things like integer representations (big endian
 vs.~little endian) or string representations (null terminated vs.~fixed
 length) and (ii) structured data is easily represented in the form of
 trees. Interestingly, the ability of XML to represent almost any form of
 structured data is often an important weakness at the same time: for a
 data exchange to be successful, a producer and a consumer must agree on
 the structure of the exchanged documents so that the latter can
 find/extract what it needs.
 This problem can be addressed by the use of a type system. A type
 system is needed in order to keep track of the meta-data (i.e.~data about
 the data) which can be used by a consumer as a guideline for data
 extraction. A number of type systems for XML have been proposed in recent
 years.  Perhaps surprisingly, specially if we look at the evolution of
 programming languages, the use of a type system in XML (as well as in
 languages for manipulating XML documents) is not mandatory.
 Domain-specific languages for XML proposed in the last few years are all,
 with the exception of XDuce, dynamically typed. Experience has showed us that
 statically-typed languages are better suited for real-world applications than
 dynamically-typed ones. Despite requiring more from the programmer's
 perspective (at least in the absence of a type-inference engine) the
 benefits greatly outcast the requirements.  Specifically, the use of a
 statically-typed language ensures that the final product is free of an
 important number of errors (so-called type errors).  In Part II, we
 present the dlcalculus, a statically-typed calculus for manipulating XML
 documents, and show how it can be integrated with existing XML technology
 by means of two algorithms for importing and exporting documents into the
 calculus.}
}


@INPROCEEDINGS{Bawden:POPL-2000,
  AUTHOR = {Alan Bawden},
  TITLE = {First-class Macros Have Types},
  CROSSREF = {POPL2000},
  PAGES = {133--141},
  CHURCHREPORT = {yes},
  DOCUMENTURL = {http://www.linearity.org/bawden/mtt/},
  PDF = {http://www.linearity.org/bawden/mtt/popl00.pdf},
  URL = {http://www.linearity.org/bawden/mtt/popl00.pdf.gz},
  POSTSCRIPT = {http://www.linearity.org/bawden/mtt/popl00.ps.gz},
  ABSTRACT = {In modern Scheme, a macro captures the lexical environment
            where it is defined.  This creates an opportunity for extending
            Scheme so that macros are first-class values.  The key to
            achieving this goal, while preserving the ability to compile
            programs into reasonable code, is the addition of a type
            system.  Many interesting things can be done with first-class
            macros, including the construction of a useful module system in
            which modules are also first-class.}
}


@INPROCEEDINGS{Law+Mai:ESOP-2000,
  AUTHOR = {Julia L. Lawall and Harry G. Mairson},
  TITLE = {Sharing continuations: proofnets for languages with
                  explicit control},
  CROSSREF = {ESOP2000},
  PAGES = {245--259},
  ABSTRACT = {We introduce graph reduction technology that
                  implements functional languages with control, such
                  as Scheme with {\tt call/cc}, where continuations
                  can be manipulated explicitly as values, and can be
                  optimally reduced in the sense of L{\'e}vy. The
                  technology is founded on {\em proofnets} for
                  multiplicative-exponential linear logic, extending
                  the techniques originally proposed by Lamping, where
                  we adapt the continuation-passing style
                  transformation to yield a new understanding of
                  sharable values. Confluence is maintained by
                  returning multiple answers to a (shared)
                  continuation. \par {\em Proofnets} provide a {\em
                  concurrent} version of linear logic proofs,
                  eliminating structurally irrelevant
                  sequentialization, and ignoring asymmetric
                  distinctions between inputs and outputs---dually,
                  expressions and continuations. While Lamping's
                  graphs and their variants encode an embedding of
                  intuitionistic logic into linear logic, our
                  construction implicitly contains an embedding of
                  classical logic into linear logic.\par We propose a
                  family of translations, produced uniformly by
                  beginning with a continuation-passing style
                  semantics for the languages, employing standard
                  codings into proofnets using call-by-value,
                  call-by-name---or hybrids of the two---to locate
                  proofnet {\em boxes}, and converting the proofnets
                  to direct style. The resulting graphs can be reduced
                  simply (cut elimination for linear logic), have a
                  consistent semantics that is preserved by reduction
                  (geometry of interaction, via the so-called {\em
                  context semantics}), and allow shared, incremental
                  evaluation of continuations (optimal reduction).},
  PDF = {http://www.church-project.org/reports/electronic/Law+Mai:ESOP-2000.pdf},
  URL = {http://www.church-project.org/reports/electronic/Law+Mai:ESOP-2000.pdf.gz},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Law+Mai:ESOP-2000.ps.gz},
  CHURCHREPORT = {yes}
}


@PHDTHESIS{Stewart:fortcf,
  AUTHOR = {C. A. Stewart},
  TITLE = {On the formulae-as-types correspondence for
                  classical logic},
  SCHOOL = {Oxford University},
  YEAR = 2000,
  CHURCHREPORT = {yes},
  PDF_A4 = {http://www.church-project.org/reports/electronic/Stewart:fortcf.pdf},
  POSTSCRIPT_A4 = {http://www.linearity.org/cas/thesis/thesis-A4.ps},
  DOCUMENTURL = {http://www.linearity.org/cas/thesis},
  ABSTRACT = {
   The Curry--Howard correspondence states the equivalence between the
   constructions implicit in intuitionistic logic and those described in
   the simply-typed lambda-calculus. It is an insight of great importance
   in theoretical computer science, and is fundamental in modern
   approaches to constructive type theory. The possibility of a similar
   formulae-as-types correspondence for classical logic looks to be a
   seminal development in this area, but whilst promising results have
   been achieved, there does not appear to be much agreement of what is
   at stake in claiming that such a correspondence exists. Consequently
   much work in this area suffers from several weaknesses; in particular
   the status of the new rules needed to describe the distinctively
   classical inferences is unclear.
   We show how to situate the formulae-as-types correspondence within the
   proof-theoretic account of logical semantics arising from the work of
   Michael Dummett and Dag Prawitz, and demonstrate that the
   admissibility of Prawitz's inversion principle, which we argue should
   be strengthened, is essential to the good behaviour of intuitionistic
   logic.
   By regarding the rules which determine the deductive strength of
   classical logic as structural rules, as opposed to the logical rules
   associated with specific logical connectives, we extend Prawitz's
   inversion principle to classical propositional logic, formulated in a
   theory of Parigot's lambda-mu calculus with eta expansions.
   We then provide a classical analogue of a subsystem of Martin-L{\"o}f's
   type theory corresponding to Peano Arithmetic and show its soundness,
   appealing to an extension of Tait's reducibility method. Our treatment
   is the first treatment of induction in classical arithmetic that truly
   falls under the aegis of the formulae-as-types correspondence, as it
   is the first that is consistent with the intensional reading of
   propositional equality.
}
}


@INPROCEEDINGS{Ong+Ste:curhff,
  AUTHOR = {C.-H. L. Ong and C. A. Stewart},
  TITLE = {A {C}urry-{H}oward foundation for functional
                  computation with control},
  PAGES = {215 -- 217},
  CROSSREF = {POPL1997},
  CHURCHREPORT = {yes},
  PDF = {http://www.church-project.org/reports/electronic/Ong+Ste:curhff.pdf},
  URL = {http://www.church-project.org/reports/electronic/Ong+Ste:curhff.pdf.gz},
  XPOSTSCRIPT = {ftp://achilles.linearity.org/pub/cas/popl97.ps},
  DOCUMENTURL = {http://www.linearity.org/cas/abstracts/popl97.html},
  ABSTRACT = {
   We introduce the type theory lambda-mu-v, a call-by-value variant of
   Parigot's lambda-mu calculus, as a Curry-Howard representation theory
   of classical propositional proofs. The associated rewrite system is
   Church-Rosser and strongly normalising, and definitional equality of
   the type theory is consistent, compatible with cut, congruent and
   decidable. The attendant call-by-value programming language mu-PCF is
   obtained from lambda-mu-v by augmenting it by basic arithmetic,
   conditionals and fixpoints. We study the behavioural properties of
   mu-PCF-v and show that, though simple, it is a very general language
   for functional computation with control: it can express all the main
   control constructs such as exceptions and first-class continuations.
   Proof theoretically the dual lambda-mu-v constructs of naming and mu
   abstraction witness the introduction and elimination rules of
   absurdity respectively. Computationally they give succinct expression
   to a kind of generic (forward) `jump' operator, which may be regarded
   as a unifying control construct for functional computation. Our goal
   is that lambda-mu-v and mu-PCF-v respectively should be to functional
   computation with first-class access to the flow of control what
   lambda-calculus and PCF respectively are to pure functional
   programming: lambda-mu-v gives the logical basis via the Curry-Howard
   correspondence, and mu-PCF-v is a prototypical language albeit in a
   purified form.
}
}


@ARTICLE{Amt+Kfo+Per:CL-2002,
  AUTHOR = {Torben Amtoft and Assaf J. Kfoury and Santiago
                  M. Pericas-Geertsen},
  TITLE = {Orderly Communication in the Ambient Calculus},
  JOURNAL = {Computer Languages},
  PUBLISHER = {Elsevier Science},
  YEAR = 2002,
  VOLUME = 28,
  PAGES = {29--60},
  CHURCHREPORT = {yes},
  PDF = {http://www.church-project.org/reports/electronic/Amt+Kfo+Per:CL-2002.pdf},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Amt+Kfo+Per:CL-2002.ps},
  ABSTRACT = {The Ambient Calculus (henceforth, {\bf AC}) was developed by Cardelli
and Gordon as a formal framework to study issues of mobility and
migrant code. We present a type system for {\bf AC} that allows the
type of exchanged data within the same ambient to vary over time.  Our
type system assigns what we call \emph{behaviors} to processes; a
denotational semantics of behaviors is proposed, here called
\emph{trace semantics}, underlying much of the remaining analysis.  We
state and prove a Subject Reduction property for our typed version of
{\bf AC}.  Based on techniques borrowed from finite automata theory,
type checking of fully type-annotated processes is shown to be
decidable.  We show that the typed version of {\bf AC} originally
proposed by Cardelli and Gordon can be naturally embedded into our
typed version of {\bf AC}.}
}


@TECHREPORT{Amt+Con+Dan+Mal:BRICS-2001,
  AUTHOR = {Torben Amtoft and Charles Consel and Olivier Danvy
                  and Karoline Malmkj{\ae}r},
  TITLE = {The Abstraction and Instantiation of String-Matching
                  Programs},
  INSTITUTION = {DAIMI, Department of Computer Science, University of
                  Aarhus},
  YEAR = 2001,
  CHURCHREPORT = {yes},
  TYPE = {Technical Report},
  NUMBER = {BRICS RS-01-12},
  PDF = {http://www.church-project.org/reports/electronic/Amt+Con+Dan+Mal:BRICS-2001.pdf},
  URL = {http://www.church-project.org/reports/electronic/Amt+Con+Dan+Mal:BRICS-2001.pdf.gz},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Amt+Con+Dan+Mal:BRICS-2001.ps.gz},
  ABSTRACT = {We consider a naive, quadratic string matcher testing whether a pattern occurs in a text; we equip it with a cache mediating its access to the
text; and we abstract the traversal policy of the pattern, the cache, and
the text.  We then specialize this abstracted program with respect to a
pattern, using the off-the-shelf partial evaluator Similix.
Instantiating the abstracted program with a left-to-right traversal
policy yields the linear-time behavior of Knuth, Morris and Pratt's
string matcher.  Instantiating it with a right-to-left policy yields the
linear-time behavior of Boyer and Moore's string matcher.},
  MONTH = APR,
  NOTE = {An extended version of an essay which appears in {\em The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones}, editors T. Mogensen and D. Schmidt and I. H Sudborough, Springer LNCS 2566, pp 332--357, 2002.}
}


@TECHREPORT{Amt:BRICS-1999,
  AUTHOR = {Torben Amtoft},
  TITLE = {Partial Evaluation for Constraint-Based Program
                  Analyses},
  INSTITUTION = {BRICS, Dept. of Computer Science, University of
                  Aarhus},
  YEAR = 1999,
  CHURCHREPORT = {yes},
  NUMBER = {BRICS-RS-99-45},
  NOTE = {},
  PDF = {http://www.church-project.org/reports/electronic/Amt:BRICS-1999.pdf},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Amt:BRICS-1999.ps.gz},
  URL = {http://www.church-project.org/reports/electronic/Amt:BRICS-1999.pdf.gz},
  ABSTRACT = {We report on a case study in the application of partial evaluation,
initiated by the desire to
speed up a constraint-based
algorithm for control-flow analysis.
We designed and implemented a dedicated
partial evaluator, able to specialize the analysis
wrt. a given constraint graph and thus remove the interpretive overhead,
and measured it with Feeley's Scheme benchmarks.
Even though the gain turned out to be rather limited,
our investigation yielded valuable feed back in that it
provided a better understanding of the analysis,
leading us to (re)invent an incremental version.
We believe this phenomenon to be a quite frequent
spinoff from using partial evaluation,
since the removal of interpretive overhead
makes the flow of control more explicit and hence
pinpoints sources of inefficiency.
Finally, we observed that partial evaluation
in our case yields such regular, low-level specialized programs
that it begs for runtime code generation.}
}


@UNPUBLISHED{Amt:CauMov-2001,
  AUTHOR = {Torben Amtoft},
  TITLE = {Causal Type System for Ambient Movements},
  NOTE = {Submitted for publication},
  YEAR = 2002,
  CHURCHREPORT = {yes},
  ABSTRACT = {
The Ambient Calculus was developed by Cardelli and Gordon as a formal
framework to study issues of mobility and migrant code. We present a
type system for the calculus, parameterized by
security constraints expressing where a given ambient may reside
and where it may be dissolved.
A subject reduction property then
guarantees that a well-typed process never violates these constraints;
additionally it ensures that communicating subprocesses agree on
their ``topic of conversation''.
Based on techniques
borrowed from finite automata theory, type checking of type-annotated
processes is decidable.
The type system employs a notion of causality in that
processes are assigned ``behaviors''.
This significantly increases the
precision of the analysis and compensates for
the lack of ``co-capabilities'' (an otherwise
increasingly popular extension to the ambient calculus);
also it allows (in contrast to other approaches)
an ambient to hold multiple topics of conversation.
},
  PDF = {http://www.church-project.org/reports/electronic/Amt:CauMov-2001.pdf},
  URL = {http://www.church-project.org/reports/electronic/Amt:CauMov-2001.pdf.gz},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Amt:CauMov-2001.ps.gz}
}


@INPROCEEDINGS{Amt+Kfo+Per:ESOP-2001,
  AUTHOR = {Torben Amtoft and Assaf J. Kfoury and Santiago
                  M. Pericas-Geertsen},
  TITLE = {What are Polymorphically-Typed Ambients?},
  BOOKTITLE = {ESOP 2001, Genova},
  PAGES = {206--220},
  YEAR = 2001,
  CHURCHREPORT = {yes},
  PDF = {http://www.church-project.org/reports/electronic/Amt+Kfo+Per:ESOP-2001.pdf},
  URL = {http://www.church-project.org/reports/electronic/Amt+Kfo+Per:ESOP-2001.pdf.gz},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Amt+Kfo+Per:ESOP-2001.ps.gz},
  EDITOR = {David Sands},
  VOLUME = 2028,
  SERIES = {LNCS},
  MONTH = APR,
  PUBLISHER = {Springer-Verlag},
  NOTE = {This downloadable extended summary is more detailed
                  than the article in the ESOP proceedings. A full
                  report is \cite{Amt+Kfo+Per:PTA-2000}},
  ABSTRACT = {The Ambient Calculus was developed by Cardelli and
Gordon as a formal framework to study issues of mobility and
migrant code. We consider an Ambient Calculus where ambients
transport and exchange programs rather that just inert data. We
propose different senses in which such a calculus can be said to
be \emph{polymorphically typed}, and design accordingly a
\emph{polymorphic} type system for it. Our type system assigns
\emph{types} to embedded programs and what we call
\emph{behaviors} to processes; a denotational semantics of
behaviors is then proposed, here called \emph{trace semantics},
underlying much of the remaining analysis. We state and prove a
Subject Reduction property for our polymorphically-typed
calculus. Based on techniques borrowed from finite automata
theory, type-checking of fully type-annotated processes is shown
to be decidable. Our polymorphically-typed calculus is a
conservative extension of the typed Ambient Calculus originally
proposed by Cardelli and Gordon.}
}


@TECHREPORT{Amt+Kfo+Per:PTA-2000,
  TITLE = {What Are Polymorphically-Typed Ambients?},
  AUTHOR = {Torben Amtoft and Assaf J. Kfoury and Santiago M. Pericas-Geertsen},
  MONTH = DEC,
  YEAR = 2000,
  NUMBER = {BUCS-TR-2000-021},
  INSTITUTION = {Comp.\ Sci.\ Dept., Boston Univ.},
  LONGINSTITUTION = {Computer Science Department, Boston
University},
  ABSTRACT = {The Ambient Calculus was developed by Cardelli and
Gordon as a formal framework to study issues of mobility and
migrant code. We consider an Ambient Calculus where ambients
transport and exchange programs rather that just inert data. We
propose different senses in which such a calculus can be said to
be \emph{polymorphically typed}, and design accordingly a
\emph{polymorphic} type system for it. Our type system assigns
\emph{types} to embedded programs and what we call
\emph{behaviors} to processes; a denotational semantics of
behaviors is then proposed, here called \emph{trace semantics},
underlying much of the remaining analysis. We state and prove a
Subject Reduction property for our polymorphically-typed
calculus. Based on techniques borrowed from finite automata
theory, type-checking of fully type-annotated processes is shown
to be decidable. Our polymorphically-typed calculus is a
conservative extension of the typed Ambient Calculus originally
proposed by Cardelli and Gordon.},
  CHURCHREPORT = {yes},
  PDF = {http://www.church-project.org/reports/electronic/Amt+Kfo+Per:PTA-2000.pdf},
  URL = {http://www.church-project.org/reports/electronic/Amt+Kfo+Per:PTA-2000.pdf.gz},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Amt+Kfo+Per:PTA-2000.ps.gz}
}


@INPROCEEDINGS{Amt+Mul:IpRA-2002,
  AUTHOR = {Torben Amtoft and Robert Muller},
  TITLE = {Inferring Annotated Types for Inter-procedural
                  Register Allocation with Constructor Flattening},
  BOOKTITLE = {The 2003 ACM SIGPLAN International Workshop on Types
                  in Language Design and Implementation (TLDI'03)},
  LOCATION = {New Orleans, Louisiana, USA},
  PAGES = {86--97},
  YEAR = 2003,
  MONTH = JAN,
  PUBLISHER = {{ACM} {P}ress},
  CHURCHREPORT = {yes},
  ABSTRACT = {We introduce an annotated type system for a
compiler intermediate language.  The type system is designed to
support inter-procedural register allocation and the
representation of tuples and variants directly in the register
file.  We present an algorithm for assigning annotations and
prove its soundness with respect to the type system.},
  PDF = {http://www.church-project.org/reports/electronic/Amt+Mul:IpRA-2002.pdf},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Amt+Mul:IpRA-2002.ps}
}


@INPROCEEDINGS{Kfo+Mai+Tur+Wel:ICFP-1999,
  ITRSPAPER = {yes},
  AUTHOR = {Assaf J. Kfoury and Harry G. Mairson and Franklyn
                  A. Turbak and J. B. Wells},
  TITLE = {Relating Typability and Expressibility in
                  Finite-Rank Intersection Type Systems},
  CROSSREF = {ICFP1999},
  PAGES = {90--101},
  ABSTRACT = {We investigate finite-rank intersection type
                  systems, analyzing the complexity of their type
                  inference problems and their relation to the problem
                  of recognizing semantically equivalent
                  terms. Intersection types allow something of type
                  $\tau_1\land\tau_2$ to be used in some places at
                  type $\tau_1$ and in other places at type
                  $\tau_2$. A \emph{finite-rank} intersection type
                  system bounds how deeply the $\land$ can appear in
                  type expressions. Such type systems enjoy strong
                  normalization, subject reduction, and computable
                  type inference, and they support a pragmatics for
                  implementing parametric polymorphism. As a
                  consequence, they provide a conceptually simple and
                  tractable alternative to the impredicative
                  polymorphism of System F and its extensions, while
                  typing many more programs than the Hindley-Milner
                  type system found in ML and Haskell. \par While type
                  inference is computable at every rank, we show that
                  its complexity grows exponentially as rank
                  increases. Let $\mathbf{K}(0,n)=n$ and
                  $\mathbf{K}(t+1,n)=2^{\mathbf{K}(t,n)}$; we prove
                  that recognizing the pure $\lambda$-terms of size
                  $n$ that are typable at rank $k$ is complete for
                  \textsc{dtime}[$\mathbf{K}(k-1,n)$]. We then
                  consider the problem of deciding whether two
                  $\lambda$-terms typable at rank $k$ have the same
                  normal form, generalizing a well-known result of
                  Statman from simple types to finite-rank
                  intersection types. We show that the equivalence
                  problem is
                  {\textsc{dtime}}$[\mathbf{K}(\mathbf{K}(k-1,n),2)]$-complete.
                  This relationship between the complexity of
                  typability and expressiveness is identical in
                  well-known decidable type systems such as simple
                  types and Hindley-Milner types, but seems to fail
                  for System F and its generalizations. The
                  correspondence gives rise to a conjecture that if
                  $\mathcal{T}$ is a predicative type system where
                  typability has complexity $t(n)$ and expressiveness
                  has complexity $e(n)$, then
                  $t(n)=\Omega(\log^{*}e(n))$.},
  DOCUMENTURL = {http://www.church-project.org/reports/Kfo+Mai+Tur+Wel:ICFP-1999.html},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Kfo+Mai+Tur+Wel:ICFP-1999.ps.gz},
  CHURCHREPORT = {yes}
}


@INPROCEEDINGS{Banerjee:ICFP-1997,
  ITRSPAPER = {yes},
  AUTHOR = {Anindya Banerjee},
  TITLE = {A Modular, Polyvariant, and Type-Based Closure
                  Analysis},
  CROSSREF = {ICFP1997},
  PAGES = {1--10},
  ABSTRACT = {We observe that the \textit{principal typing
                  property} of a type system is the enabling
                  technology for \textit{modularity} and
                  \textit{separate compilation}
                  \cite{Jim:MIT-LCS-1995-532}. We use this technology
                  to formulate a modular and polyvariant closure
                  analysis, based on the rank 2 intersection types
                  annotated with control-flow information.\par
                  Modularity manifests itself in a syntax-directed,
                  annotated-type inference algorithm that can analyse
                  \textit{program fragments} containing free
                  variables: a \textit{principal typing} property is
                  used to formalise it. Polyvariance manifests itself
                  in the separation of different behaviours of the
                  same function at its different uses: this is
                  formalised via the rank 2 intersection types. As the
                  rank 2 intersection type discipline types at least
                  all (core) ML programs, our analysis can be used in
                  the separate compilation of such programs.},
  DOCUMENTURL = {http://www.church-project.org/reports/Banerjee:ICFP-1997.html},
  PDF = {http://www.church-project.org/reports/electronic/Banerjee:ICFP-1997.pdf},
  URL = {http://www.church-project.org/reports/electronic/Banerjee:ICFP-1997.pdf.gz},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Banerjee:ICFP-1997.ps.gz},
  CHURCHREPORT = {yes}
}


@TECHREPORT{Jim:RTTS-1995,
  ITRSPAPER = {yes},
  AUTHOR = {Trevor Jim},
  TITLE = {Rank 2 Type Systems and Recursive Definitions},
  INSTITUTION = {Massachusetts Institute of Technology},
  YEAR = 1995,
  NUMBER = {MIT/LCS/TM-531},
  MONTH = NOV,
  PDF = {http://www.church-project.org/reports/electronic/Jim:RTTS-1995.pdf},
  URL = {http://www.church-project.org/reports/electronic/Jim:RTTS-1995.pdf.gz},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Jim:RTTS-1995.ps.gz},
  ABSTRACT = {We demonstrate the pragmatic value of the
                  \emph{principal typing property}, a property
                  distinct from ML's principal type property, by
                  studying a type system with principal typings. The
                  type system is based on rank 2 intersection types
                  and is closely related to ML\@.\par Its principal
                  typing property provides elegant support for
                  separate compilation, including ``smartest
                  recompilation'' and incremental type
                  inference. Moreover, it motivates a new rule for
                  typing recursive definitions that can type some
                  interesting examples of polymorphic recursion.},
  CHURCHREPORT = {yes}
}


@TECHREPORT{Jim:MIT-LCS-1995-532,
  ITRSPAPER = {yes},
  AUTHOR = {Trevor Jim},
  TITLE = {What Are Principal Typings and What Are They Good
                  For?},
  INSTITUTION = {MIT},
  YEAR = 1995,
  TYPE = {Tech.\ memo.},
  NUMBER = {MIT/LCS/TM-532},
  PDF = {http://www.church-project.org/reports/electronic/Jim:MIT-LCS-1995-532.pdf},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Jim:MIT-LCS-1995-532.ps.gz},
  URL = {http://www.church-project.org/reports/electronic/Jim:MIT-LCS-1995-532.pdf.gz},
  ABSTRACT = {We demonstrate the pragmatic value of the
                  \emph{principal typing property}, a property
                  distinct from ML's principal type property, by
                  studying a type system with principal typings. The
                  type system is based on rank 2 intersection types
                  and is closely related to ML\@.\par Its principal
                  typing property provides elegant support for
                  separate compilation, including ``smartest
                  recompilation'' and incremental type inference, and
                  for accurate type error messages. Moreover, it
                  motivates a new rule for typing recursive
                  definitions that can type some interesting examples
                  of polymorphic recursion.},
  CHURCHREPORT = {yes}
}


@INPROCEEDINGS{Kfo+Wel:LICS-1995,
  ITRSPAPER = {yes},
  TITLE = {New Notions of Reduction and Non-Semantic Proofs of
                  $\beta$-Strong Normalization in Typed
                  $\lambda$-Calculi},
  AUTHOR = {A. J. Kfoury and J. B. Wells},
  PAGES = {311--321},
  CROSSREF = {LICS1995},
  COMMENT = {The PDF link is disabled because the PDF file has
                  absolutely horrible and unreadable fonts. Please do
                  not enable it until the fonts are fixed.},
  PDF = {http://www.church-project.org/reports/electronic/Kfo+Wel:LICS-1995.pdf},
  DOCUMENTURL = {http://www.church-project.org/reports/Kfo+Wel:LICS-1995.html},
  URL = {http://www.church-project.org/reports/electronic/Kfo+Wel:LICS-1995.pdf.gz},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Kfo+Wel:LICS-1995.ps.gz},
  SOURCE = {ftp://theory.lcs.mit.edu/pub/meyer/lics.bib},
  CHURCHREPORT = {yes},
  ABSTRACT = {Two notions of reduction for terms of the
                  $\lambda$-calculus are introduced and the question
                  of whether a $\lambda$-term is $\beta$-strongly
                  normalizing is reduced to the question of whether a
                  $\lambda$-term is merely normalizing under one of
                  the notions of reduction.  This gives a method to
                  prove strong $\beta$-normalization for typed
                  $\lambda$-calculi.  Instead of the usual semantic
                  proof style based on Tait's realizability or
                  Girard's ``candidats de r{\'e}ductibilit{\'e}'',
                  termination can be proved using a decreasing metric
                  over a well-founded ordering.  This proof method is
                  applied to the simply-typed $\lambda$-calculus and
                  the system of intersection types, giving the first
                  non-semantic proof for a polymorphic extension of
                  the $\lambda$-calculus.}
}


@INPROCEEDINGS{Wel+Dim+Mul+Tur:TAPSOFT-1997,
  ITRSPAPER = {yes},
  AUTHOR = {J. B. Wells and Allyn Dimock and Robert Muller and
                  Franklyn Turbak},
  TITLE = {A Typed Intermediate Language for Flow-Directed
                  Compilation},
  CROSSREF = {TAPSOFT1997},
  PAGES = {757--771},
  ABSTRACT = {We present a typed intermediate language
                  $\lambda^{\mathrm{CIL}}$ for optimizing compilers
                  for function-oriented and polymorphically typed
                  programming languages (e.g., ML). The language
                  $\lambda^{\mathrm{CIL}}$ is a typed lambda calculus
                  with product, sum, intersection, and union types as
                  well as function types annotated with flow labels. A
                  novel formulation of intersection and union types
                  supports encoding flow information in the typed
                  program representation. This flow information can
                  direct optimization.},
  NOTE = {Superseded by \cite{Wel+Dim+Mul+Tur:JFP-2002-v12n3}},
  COMMENT = {The disabling of the PDF links is disabled as the
                  fonts does not look that bad when printed and PDF
                  provides the best way to ensure that the files are
                  printable under Windows. Please do not disable this
                  diabling without discussing it with me (Peter). The
                  PDF link is disabled because the PDF file has
                  absolutely horrible and unreadable fonts. Please do
                  not enable it until the fonts are fixed.},
  DOCUMENTURL = {http://www.church-project.org/reports/Wel+Dim+Mul+Tur:TAPSOFT-1997.html},
  PDF = {http://www.church-project.org/reports/electronic/Wel+Dim+Mul+Tur:TAPSOFT-1997.pdf},
  URL = {http://www.church-project.org/reports/electronic/Wel+Dim+Mul+Tur:TAPSOFT-1997.pdf.gz},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Wel+Dim+Mul+Tur:TAPSOFT-1997.ps},
  CHURCHREPORT = {yes}
}


@ARTICLE{Wel+Dim+Mul+Tur:JFP-2002-v12n3,
  ITRSPAPER = {yes},
  AUTHOR = {J. B. Wells and Allyn Dimock and Robert Muller and
                  Franklyn Turbak},
  TITLE = {A Calculus with Polymorphic and Polyvariant Flow
                  Types},
  JOURNAL = {J.~Funct.\ Programming},
  YEAR = {2002},
  VOLUME = {12},
  NUMBER = {3},
  MONTH = MAY,
  PAGES = {183--227},
  NOTE = {Supersedes \cite{Wel+Dim+Mul+Tur:TAPSOFT-1997}},
  CHURCHREPORT = {yes},
  DOCUMENTURL = {http://www.church-project.org/reports/Wel+Dim+Mul+Tur:JFP-2002-v12n3.html},
  PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Wells+Dimock+Muller+Turbak:A-Calculus-with-Polymorphic-and-Polyvariant-Flow-Types:JFP-2002-v12n3.pdf},
  ABSTRACT = {We present $\lambda^{\mathrm{CIL}}$, a typed
                  $\lambda$-calculus which serves as the foundation
                  for a typed intermediate language for optimizing
                  compilers for higher-order polymorphic programming
                  languages.  The key innovation of
                  $\lambda^{\mathrm{CIL}}$ is a novel formulation of
                  intersection and union types and flow labels on both
                  terms and types.  These \emph{flow types} can encode
                  polyvariant control and data flow information within
                  a polymorphically typed program representation. Flow
                  types can guide a compiler in generating customized
                  data representations in a strongly typed setting.
                  Since $\lambda^{\mathrm{CIL}}$ enjoys confluence,
                  standardization, and subject reduction properties,
                  it is a valuable tool for reasoning about programs
                  and program transformations.}
}


@INPROCEEDINGS{Dim+Mul+Tur+Wel:ICFP-1997,
  ITRSPAPER = {yes},
  AUTHOR = {Allyn Dimock and Robert Muller and Franklyn Turbak
                  and J. B. Wells},
  TITLE = {Strongly Typed Flow-Directed Representation
                  Transformations},
  CROSSREF = {ICFP1997},
  PAGES = {11--24},
  ABSTRACT = {We present a new framework for transforming data
                  representations in a strongly typed intermediate
                  language. Our method allows both value producers
                  (sources) and value consumers (sinks) to support
                  multiple representations, automatically inserting
                  any required code. Specialized representations can
                  be easily chosen for particular source/sink
                  pairs. The framework is based on these techniques:
                  \begin{enumerate} \item \emph{Flow annotated types}
                  encode the ``flows-from'' (source) and ``flows-to''
                  (sink) information of a flow graph. \item
                  \emph{Intersection and union types} support (a)
                  encoding precise flow information, (b) separating
                  flow information so that transformations can be well
                  typed, (c) automatically reorganizing flow paths to
                  enable multiple representations. \end{enumerate} As
                  an instance of our framework, we provide a function
                  representation transformation that encompasses both
                  closure conversion and inlining. Our framework is
                  adaptable to data other than functions.},
  COMMENT = {The disabling of the PDF links is disabled as the fonts does not look that bad when printed and PDF provides the best way to ensure that the files are printable under Windows.  Please do not disable this diabling without discussing it with me (Peter).

The PDF link is disabled because the PDF file has absolutely horrible and unreadable fonts.  Please do not enable it until the fonts are fixed.},
  URL = {http://www.church-project.org/reports/electronic/Dim+Mul+Tur+Wel:ICFP-1997.pdf.gz},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Dim+Mul+Tur+Wel:ICFP-1997.ps.gz},
  DOCUMENTURL = {http://www.church-project.org/reports/Dim+Mul+Tur+Wel:ICFP-1997.html},
  CHURCHREPORT = {yes}
}


@INPROCEEDINGS{Tur+Dim+Mul+Wel:CPPFT-1997,
  ITRSPAPER = {yes},
  AUTHOR = {Franklyn Turbak and Allyn Dimock and Robert Muller
                  and J. B. Wells},
  TITLE = {Compiling with Polymorphic and Polyvariant Flow
                  Types},
  CROSSREF = {TIC1997},
  ABSTRACT = {Optimizing compilers for function-oriented and
                  object-oriented languages exploit type and flow
                  information for efficient implementation. Although
                  type and flow information (both control and data
                  flow) are inseparably intertwined, compilers usually
                  compute and represent them separately. Partially,
                  this has been a result of the usual polymorphic type
                  systems using $\forall$ and $\exists$ quantifiers,
                  which are difficult to use in combination with flow
                  annotations. \par In the Church Project, we are
                  experimenting with intermediate languages that
                  integrate type and flow information into a single
                  {\em flow type} framework. This integration
                  facilitates the preservation of flow and type
                  information through program transformations. In this
                  paper we describe $\lambda^{\mathrm{CIL}}$, an
                  intermediate language supporting polymorphic types
                  and polyvariant flow information and describe its
                  application in program optimiziation. We are
                  experimenting with this intermediate language in a
                  flow and type-directed compiler for a functional
                  language. The types of $\lambda^{\mathrm{CIL}}$
                  encode flow information (1) via labels that
                  approximate sources and sinks of values and (2) via
                  intersection and union types, finitary versions of
                  universal and existential types that support type
                  polymorphism and (in combination with the labels)
                  polyvariant flow analysis. Accurate flow types
                  expose opportunities for a wide range of optimizing
                  program transformations.},
  COMMENT = {The disabling of the PDF links is disabled as the fonts does not look that bad when printed and PDF provides the best way to ensure that the files are printable under Windows.  Please do not disable this diabling without discussing it with me (Peter).

The PDF link is disabled because the PDF file has absolutely horrible and unreadable fonts.  Please do not enable it until the fonts are fixed.},
  DOCUMENTURL = {http://www.church-project.org/reports/Tur+Dim+Mul+Wel:CPPFT-1997.html},
  URL = {http://www.church-project.org/reports/electronic/Tur+Dim+Mul+Wel:CPPFT-1997.pdf.gz},
  POSTSCRIPT = {http://www.cs.bc.edu/~muller/TIC97/Turbak.ps.gz},
  CHURCHREPORT = {yes},
  NOTE = {},
  XNOTE = {note field must be blank to prevent getting
                  crossref's note!}
}


@INPROCEEDINGS{Dim+Wes+Mul+Tur+Wel+Con:TIC-2000,
  ITRSPAPER = {yes},
  AUTHOR = {Allyn Dimock and Ian Westmacott and Robert Muller
                  and Franklyn Turbak and J. B. Wells and Jeffrey
                  Considine},
  TITLE = {Space Issues in Compiling with Intersection and
                  Union Types},
  CROSSREF = {TIC2000},
  CHURCHREPORT = {yes},
  DOCUMENTURL = {http://www.church-project.org/reports/Dim+Wes+Mul+Tur+Wel+Con:TIC-2000.html},
  ABSTRACT = {The CIL compiler for core Standard ML compiles whole
                  programs using the CIL typed intermediate language
                  with flow labels and intersection and union
                  types.  Flow labels embed flow information in the
                  types and intersection and union types support
                  precise polyvariant type and flow information,
                  without the use of type-level abstraction or
                  quantification.
                  \par
                  Compile-time representations of CIL types and terms
                  are potentially large compared to those for similar
                  types and terms in systems based on quantified
                  types.  The listing-based nature of intersection and
                  union types, together with flow label annotations on
                  types, contribute to the size of CIL types.  The CIL
                  term representation duplicates portions of the
                  program where intersection types are introduced and
                  union types are eliminated.  This duplication makes
                  it easier to represent type information and to
                  introduce multiple representation conventions, but
                  incurs a compile-time space cost.
                  \par
                  This paper presents empirical data on the
                  compile-time space costs of using CIL.  These costs
                  can be made tractable using standard hash-consing
                  techniques.  Surprisingly, the duplicating nature of
                  CIL has acceptable compile-time space performance in
                  practice on the benchmarks and flow analyses that we
                  have investigated.  Increasing the precision of flow
                  analysis can significantly reduce compile-time space
                  costs.  There is also preliminary evidence that the
                  flow information encoded in CIL's type system can
                  effectively guide data customization.},
  NOTE = {Superseded by~\cite{Dim+Wes+Mul+Tur+Wel+Con:TIC-2000-LNCS}}
}


@INPROCEEDINGS{Dim+Wes+Mul+Tur+Wel+Con:TIC-2000-LNCS,
  ITRSPAPER = {yes},
  AUTHOR = {Allyn Dimock and Ian Westmacott and Robert Muller
                  and Franklyn Turbak and J. B. Wells and Jeffrey
                  Considine},
  TITLE = {Program Representation Size in an Intermediate
                  Language with Intersection and Union Types},
  CROSSREF = {TIC2000LNCS},
  PAGES = {27--52},
  CHURCHREPORT = {yes},
  DOCUMENTURL = {http://www.church-project.org/reports/Dim+Wes+Mul+Tur+Wel+Con:TIC-2000-LNCS.html},
  XPDF = {http://www.church-project.org/reports/electronic/Dim+Wes+Mul+Tur+Wel+Con:TIC-2000-LNCS.pdf.gz},
  XPOSTSCRIPT = {http://www.church-project.org/reports/electronic/Dim+Wes+Mul+Tur+Wel+Con:TIC-2000-LNCS.ps.gz},
  XNOTE = {Supersedes~\cite{Dim+Wes+Mul+Tur+Wel+Con:TIC-2000}},
  ABSTRACT = {The CIL compiler for core Standard ML compiles whole
                  programs using the CIL typed intermediate language
                  with flow labels and intersection and union
                  types.  Flow labels embed flow information in the
                  types and intersection and union types support
                  precise polyvariant type and flow information,
                  without the use of type-level abstraction or
                  quantification.
                  \par
                  Compile-time representations of CIL types and terms
                  are potentially large compared to those for similar
                  types and terms in systems based on quantified
                  types.  The listing-based nature of intersection and
                  union types, together with flow label annotations on
                  types, contribute to the size of CIL types.  The CIL
                  term representation duplicates portions of the
                  program where intersection types are introduced and
                  union types are eliminated.  This duplication makes
                  it easier to represent type information and to
                  introduce multiple representation conventions, but
                  incurs a compile-time space cost.
                  \par
                  This paper presents empirical data on the
                  compile-time space costs of using CIL.  These costs
                  can be made tractable using standard hash-consing
                  techniques.  Surprisingly, the duplicating nature of
                  CIL has acceptable compile-time space performance in
                  practice on the benchmarks and flow analyses that we
                  have investigated.  Increasing the precision of flow
                  analysis can significantly reduce compile-time space
                  costs.  There is also preliminary evidence that the
                  flow information encoded in CIL's type system can
                  effectively guide data customization.}
}


@TECHREPORT{Dim+Wes+Mul+Tur+Wel+Con:TIC-2000-TR,
  ITRSPAPER = {yes},
  AUTHOR = {Allyn Dimock and Ian Westmacott and Robert Muller
                  and Franklyn Turbak and J. B. Wells and Jeffrey
                  Considine},
  TITLE = {Program Representation Size in an Intermediate
                  Language with Intersection and Union Types},
  MONTH = MAR,
  YEAR = 2001,
  INSTITUTION = {Comp.\ Sci.\ Dept., Boston Univ.},
  LONGINSTITUTION = {Computer Science Department, Boston University},
  NUMBER = {BUCS-TR-2001-02},
  NOTE = {This is a version of \cite{Dim+Wes+Mul+Tur+Wel+Con:TIC-2000-LNCS}
                  extended with an appendix describing the CIL typed intermediate
                  language.},
  CHURCHREPORT = {yes},
  PDF = {http://www.cs.bu.edu/techreports/pdf/2001-002-program-representation-size.pdf},
  PDFREMARK = {non-scalable fonts!},
  POSTSCRIPT = {http://www.cs.bu.edu/techreports/ps/2001-002-program-representation-size.ps},
  ABSTRACT = {The CIL compiler for core Standard ML compiles whole
                  programs using a novel typed intermediate language
                  (TIL) with intersection and union types and flow
                  labels on both terms and types.  The CIL term
                  representation duplicates portions of the program
                  where intersection types are introduced and union
                  types are eliminated.  This duplication makes it
                  easier to represent type information and to
                  introduce customized data representations.  However,
                  duplication incurs compile-time space costs that are
                  potentially much greater than are incurred in TILs
                  employing type-level abstraction or quantification.
                  In this paper, we present empirical data on the
                  compile-time space costs of using CIL as an
                  intermediate language.  The data shows that these
                  costs can be made tractable by using sufficiently
                  fine-grained flow analyses together with standard
                  hash-consing techniques.   The data also suggests
                  that non-duplicating formulations of intersection
                  (and union) types would not achieve significantly
                  better space complexity.}
}


@INPROCEEDINGS{Dim+Wes+Mul+Tur+Wel:ICFP-2001,
  ITRSPAPER = {yes},
  AUTHOR = {Allyn Dimock and Ian Westmacott and Robert Muller
                  and Franklyn Turbak and J. B. Wells},
  XPDLI01TITLE = {Flow-Based Function Customization in the Presence of
                   Representation Pollution},
  TITLE = {Functioning without Closure: Type-Safe Customized
                  Function Representations for {S}tandard {ML}},
  CROSSREF = {ICFP2001},
  COMMENT = {change documenturl when this is added as church paper},
  OLDDOCUMENTURL = {http://www.macs.hw.ac.uk/~jbw/papers/#Dim+Wes+Mul+Tur+Wel:ICFP-2001},
  DOCUMENTURL = {http://www.church-project.org/reports/Dim+Wes+Mul+Tur+Wel:ICFP-2001.html},
  PDF = {http://www.church-project.org/reports/electronic/Dim+Wes+Mul+Tur+Wel:ICFP-2001.pdf},
  URL = {http://www.church-project.org/reports/electronic/Dim+Wes+Mul+Tur+Wel:ICFP-2001.pdf.gz},
  CHURCHREPORT = {yes},
  ABSTRACT = {The CIL compiler for core Standard ML compiles
                  whole SML programs using a novel typed intermediate
                  language that supports the generation of type-safe
                  customized data representations. In this paper, we
                  present empirical data comparing the relative
                  efficacy of several different customization
                  strategies for function representations. We develop
                  a cost model to interpret dynamic counts of
                  operations required for each strategy. One of our
                  results is data showing that compiling with a
                  function representation strategy that makes
                  customization decisions based on the presence or
                  absence of free variables of a function gives a 26\%
                  improvement over a uniform closure representation.
                  We also present data on the relative effectiveness
                  of various representation pollution removal
                  strategies.  We find that for the types of
                  representation pollution detected by our compiler,
                  pollution removal rarely provides any additional
                  benefit for the  representation strategies and
                  benchmarks considered.},
  PAGES = {14--25},
  ISBN = {1-58113-415-0}
}


@INPROCEEDINGS{Kfo+Wel:POPL-1999,
  ITRSPAPER = {yes},
  AUTHOR = {Assaf J. Kfoury and J. B. Wells},
  TITLE = {Principality and Decidable Type Inference for
                  Finite-Rank Intersection Types},
  CROSSREF = {POPL1999},
  PAGES = {161--174},
  DOCUMENTURL = {http://www.church-project.org/reports/Kfo+Wel:POPL-1999.html},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Kfo+Wel:POPL-1999.ps.gz},
  ACMURLA = {http://portal.acm.org/citation.cfm?id=292540.292556&coll=portal&dl=ACM&CFID=3866787&CFTOKEN=29489829},
  ACMURLB = {http://doi.acm.org/10.1145/292540.292556},
  CHURCHREPORT = {yes},
  NOTE = {Superseded by \cite{Kfo+Wel:TCSB-2004-v311n1-3}},
  ABSTRACT = {Principality of typings is the property that for
                  each typable term, there is a typing from which all
                  other typings are obtained via some set of
                  operations. Type inference is the problem of finding
                  a typing for a given term, if possible. We define an
                  intersection type system which has principal typings
                  and types exactly the strongly normalizable
                  $\lambda$-terms. More interestingly, every
                  finite-rank restriction of this system (using
                  Leivant's first notion of rank) has principal
                  typings and also has decidable type inference. This
                  is in contrast to System~F where the finite rank
                  restriction for every finite rank at 3 and above has
                  neither principal typings nor decidable type
                  inference. This is also in contrast to earlier
                  presentations of intersection types where the status
                  (decidable or undecidable) of these properties is
                  unknown for the finite-rank restrictions at 3 and
                  above. Furthermore, the notion of principal typings
                  for our system involves only one operation,
                  substitution, rather than several operations (not
                  all substitution-based) as in earlier presentations
                  of principality for intersection types (without rank
                  restrictions). In our system the earlier notion of
                  \emph{expansion} is integrated in the form of
                  \emph{expansion variables}, which are subject to
                  substitution as are ordinary variables. A
                  unification-based type inference algorithm is
                  presented using a new form of unification,
                  $\beta$-unification.}
}


@ARTICLE{Kfo+Wel:TCSB-2004-v311n1-3,
  ITRSPAPER = {yes},
  CHURCHREPORT = {yes},
  DARTTODO = {Mention this.},
  AUTHOR = {Assaf J. Kfoury and J. B. Wells},
  TITLE = {Principality and Type Inference for Intersection
                  Types Using Expansion Variables},
  JOURNAL = {Theoret.\ Comput.\ Sci.},
  VOLUME = {311},
  NUMBER = {1--3},
  PAGES = {1--70},
  XNUMBERNOTE = {Elsevier refers to "issues" 1--3, not "number"},
  YEAR = {2004},
  DOI = {doi:10.1016/j.tcs.2003.10.032},
  SCIENCEDIRECT = {http://authors.elsevier.com/sd/article/S0304397503005772},
  TCSREF = {TCS4942},
  DOCUMENTURL = {http://www.church-project.org/reports/Kfo+Wel:TCSB-2004-v311n1-3.html},
  PDF = {http://www.church-project.org/reports/electronic/Kfo+Wel:TCSB-2004-v311n1-3.pdf},
  NOTE = {Supersedes \cite{Kfo+Wel:POPL-1999}.
                  For omitted proofs, see the longer
                  report \cite{Kfo+Wel:PTI-2003}},
  ABSTRACT = {Principality of typings is the property that for
                  each typable term, there is a typing from which all
                  other typings are obtained via some set of
                  operations. Type inference is the problem of finding
                  a typing for a given term, if possible. We define an
                  intersection type system which has principal typings
                  and types exactly the strongly normalizable
                  $\lambda$-terms. More interestingly, every
                  finite-rank restriction of this system (using
                  Leivant's first notion of rank) has principal
                  typings and also has decidable type inference. This
                  is in contrast to System~F where the finite rank
                  restriction for every finite rank at 3 and above has
                  neither principal typings nor decidable type
                  inference. Furthermore, the notion of principal typings
                  for our system involves only one operation,
                  substitution, rather than several operations (not
                  all substitution-based) as in earlier presentations
                  of principality for intersection types (without rank
                  restrictions). In our system the earlier notion of
                  \emph{expansion} is integrated in the form of
                  \emph{expansion variables}, which are subject to
                  substitution as are ordinary variables. A
                  unification-based type inference algorithm is
                  presented using a new form of unification,
                  $\beta$-unification.}
}


@UNPUBLISHED{Kfo+Wel:PTI-2003,
  AUTHOR = {Assaf J. Kfoury and J. B. Wells},
  TITLE = {Principality and Type Inference for Intersection
                  Types Using Expansion Variables},
  CHURCHREPORT = {yes},
  DARTTODO = {Mention this.},
  PDF = {http://www.church-project.org/reports/electronic/Kfo+Wel:PTI-2003.pdf.gz},
  NOTE = {Supersedes \cite{Kfo+Wel:POPL-1999}},
  MONTH = AUG,
  YEAR = 2003,
  ABSTRACT = {Principality of typings is the property that for
                  each typable term, there is a typing from which all
                  other typings are obtained via some set of
                  operations. Type inference is the problem of finding
                  a typing for a given term, if possible. We define an
                  intersection type system which has principal typings
                  and types exactly the strongly normalizable
                  $\lambda$-terms. More interestingly, every
                  finite-rank restriction of this system (using
                  Leivant's first notion of rank) has principal
                  typings and also has decidable type inference. This
                  is in contrast to System~F where the finite rank
                  restriction for every finite rank at 3 and above has
                  neither principal typings nor decidable type
                  inference. Furthermore, the notion of principal typings
                  for our system involves only one operation,
                  substitution, rather than several operations (not
                  all substitution-based) as in earlier presentations
                  of principality for intersection types (without rank
                  restrictions). In our system the earlier notion of
                  \emph{expansion} is integrated in the form of
                  \emph{expansion variables}, which are subject to
                  substitution as are ordinary variables. A
                  unification-based type inference algorithm is
                  presented using a new form of unification,
                  $\beta$-unification.}
}


@INPROCEEDINGS{Wells:ICALP-2002,
  ITRSPAPER = {yes},
  AUTHOR = {J. B. Wells},
  TITLE = {The Essence of Principal Typings},
  CROSSREF = {ICALP2002},
  DOCUMENTURL = {http://www.church-project.org/reports/Wells:ICALP-2002.html},
  PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Wells:The-Essence-of-Principal-Typings:ICALP-2002.pdf},
  DARTREPORT = {yes},
  CHURCHREPORT = {yes},
  PAGES = {913--925},
  SPRINGERURL = {http://link.springer.de/link/service/series/0558/bibs/2380/23800913.htm},
  ABSTRACT = {Let $S$ be some type system.  A \emph{typing} in $S$
                  for a typable term $M$ is the collection of all of
                  the information other than $M$ which appears in the
                  final judgement of a proof derivation showing that
                  $M$ is typable.  For example, suppose there is a
                  derivation in $S$ ending with the judgement
                  $A\vdash{M}\mathrel{:}{\tau}$ meaning that $M$ has
                  result type $\tau$ when assuming the types of free
                  variables are given by $A$.  Then $(A,\tau)$ is a
                  typing for $M$.
                  \par
                  A \emph{principal typing} in $S$ for a term $M$ is a
                  typing for $M$ which somehow represents all other
                  possible typings in $S$ for $M$.  It is important not
                  to confuse this notion with the weaker notion of
                  \emph{principal type} often mentioned in connection
                  with the Hindley/Milner type system.  Previous
                  definitions of principal typings for specific type
                  systems have involved various syntactic operations
                  on typings such as \emph{substitution} of types for
                  type variables, \emph{expansion}, \emph{lifting},
                  etc.
                  \par
                  This paper presents a new general definition of
                  principal typings which does not depend on the
                  details of any particular type system.  This paper
                  shows that the new general definition correctly
                  generalizes previous system-dependent definitions.
                  This paper explains why the new definition is the
                  right one.  Furthermore, the new definition is used
                  to prove that certain polymorphic type systems using
                  $\forall$-quantifiers, namely System F and the
                  Hindley/Milner system, do not have principal
                  typings.}
}


@UNPUBLISHED{Wells:EPT-2002,
  ITRSPAPER = {yes},
  AUTHOR = {J. B. Wells},
  TITLE = {The Essence of Principal Typings},
  DOCUMENTURL = {http://www.church-project.org/reports/Wells:EPT-2002.html},
  PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Wells:The-Essence-of-Principal-Typings:slightly-longer.pdf},
  DARTREPORT = {yes},
  CHURCHREPORT = {yes},
  YEAR = 2002,
  NOTE = {A longer version of \cite{Wells:ICALP-2002} with a
                  3-page appendix with extra proofs, a page of extra
                  discussion of non-related work, and other minor
                  changes},
  ABSTRACT = {Let $S$ be some type system.  A \emph{typing} in $S$
                  for a typable term $M$ is the collection of all of
                  the information other than $M$ which appears in the
                  final judgement of a proof derivation showing that
                  $M$ is typable.  For example, suppose there is a
                  derivation in $S$ ending with the judgement
                  $A\vdash{M}\mathrel{:}{\tau}$ meaning that $M$ has
                  result type $\tau$ when assuming the types of free
                  variables are given by $A$.  Then $(A,\tau)$ is a
                  typing for $M$.
                  \par
                  A \emph{principal typing} in $S$ for a term $M$ is a
                  typing for $M$ which somehow represents all other
                  possible typings in $S$ for $M$.  It is important not
                  to confuse this notion with the weaker notion of
                  \emph{principal type} often mentioned in connection
                  with the Hindley/Milner type system.  Previous
                  definitions of principal typings for specific type
                  systems have involved various syntactic operations
                  on typings such as \emph{substitution} of types for
                  type variables, \emph{expansion}, \emph{lifting},
                  etc.
                  \par
                  This paper presents a new general definition of
                  principal typings which does not depend on the
                  details of any particular type system.  This paper
                  shows that the new general definition correctly
                  generalizes previous system-dependent definitions.
                  This paper explains why the new definition is the
                  right one.  Furthermore, the new definition is used
                  to prove that certain polymorphic type systems using
                  $\forall$-quantifiers, namely System F and the
                  Hindley/Milner system, do not have principal
                  typings.}
}


@ARTICLE{Wel+Haa:IAC-ta,
  ITRSPAPER = {yes},
  DARTTODO = {Mention this.},
  AUTHOR = {J. B. Wells and Christian Haack},
  TITLE = {Branching Types},
  JOURNAL = {Inform.\ {\&} Comput.},
  YEAR = {200X},
  XVOLUME = {},
  XNUMBER = {},
  XPAGES = {},
  XMONTH = {},
  PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Wells+Haack:Branching-Types:2002-08-18.pdf},
  NOTE = {Completely supersedes \cite{Wel+Haa:ESOP-2002}.  Accepted
                  subject to revisions},
  CHURCHREPORT = {yes},
  ABSTRACT = {Although systems with intersection types have many
                  unique capabilities, there has never been a fully
                  satisfactory explicitly typed system with
                  intersection types.  We introduce and prove the basic
                  properties of $\lambda^{\mathrm{B}}$, a typed
                  $\lambda$-calculus with \emph{branching types} and
                  types with quantification over \emph{type selection
                  parameters}.  The new system $\lambda^{\mathrm{B}}$ is an
                  explicitly typed system with the same expressiveness
                  as a system with intersection types.  Typing
                  derivations in $\lambda^{\mathrm{B}}$ use branching types to
                  squash together what would be separate parallel
                  derivations in earlier systems with intersection
                  types.}
}


@INPROCEEDINGS{Wel+Haa:ESOP-2002,
  ITRSPAPER = {yes},
  AUTHOR = {J. B. Wells and Christian Haack},
  TITLE = {Branching Types},
  CROSSREF = {ESOP2002},
  PAGES = {115--132},
  DOCUMENTURL = {http://www.church-project.org/reports/Wel+Haa:ESOP-2002.html},
  PDF = {http://www.macs.hw.ac.uk/~jbw/papers/Wells+Haack:Branching-Types:ESOP-2002.pdf},
  SPRINGERURL = {http://link.springer.de/link/service/series/0558/bibs/2305/23050115.htm},
  CHURCHREPORT = {yes},
  NOTE = {Completely superseded by \cite{Wel+Haa:IAC-ta}},
  ABSTRACT = {Although systems with intersection types have many
                  unique capabilities, there has never been a fully
                  satisfactory explicitly typed system with
                  intersection types. We introduce $\lambda^{\mathrm{B}}$ with \emph{branching types} and types which are
                  quantified over \emph{type selectors} to provide an
                  explicitly typed system with the same expressiveness
                  as a system with intersection types. Typing
                  derivations in $\lambda^{\mathrm{B}}$ effectively
                  squash together what would be separate parallel
                  derivations in earlier systems with intersection
                  types.}
}


@TECHREPORT{Wells:TUFE-1996,
  AUTHOR = {J. B. Wells},
  TITLE = {Typability is Undecidable for {F}+Eta},
  INSTITUTION = {Comp.\ Sci.\ Dept., Boston Univ.},
  YEAR = 1996,
  NUMBER = {96-022},
  TYPE = {Tech.\ Rep.},
  MONTH = MAR,
  DOCUMENTURL = {http://www.church-project.org/reports/Wells:TUFE-1996.html},
  POSTSCRIPT = {http://www.cs.bu.edu/techreports/1996-022-f+eta-typability-undecidable.ps.gz},
  CHURCHREPORT = {yes},
  ABSTRACT = {System F is the well-known polymorphically-typed
                  $\lambda$-calculus with
                  universal quantifiers (``$\forall$'').
                  F+$\eta$ is System F extended with the eta rule,
                  which says that if term $M$ can be given type $\tau$
                  and $M$ $\eta$-reduces to $N$, then $N$ can also be
                  given the type $\tau$.
                  Adding the eta rule to System F is equivalent to
                  adding the subsumption rule using the subtyping
                  (``containment'') relation that Mitchell defined and
                  axiomatized.
                  The subsumption rule says that if $M$ can be given
                  type $\tau$ and $\tau$ is a subtype of type
                  $\sigma$, then $M$ can be given type $\sigma$.
                  Mitchell's subtyping relation involves no extensions
                  to the syntax of types, i.e., no bounded
                  polymorphism and no supertype of all types, and is
                  thus unrelated to the system $\mathrm{F}_\leq$
                  (``F-sub'').
                  \par
                  Typability for F+$\eta$ is the problem of
                  determining for any term $M$ whether there is any
                  type $\tau$ that can be given to it using the type
                  inference rules of F+$\eta$.
                  Typability has been proven undecidable for System
                  F (without the eta rule), but the decidability of
                  typability has been an open problem for F+$\eta$.
                  Mitchell's subtyping relation has recently been
                  proven undecidable, implying the undecidability of
                  ``type checking'' for F+$\eta$.
                  This paper reduces the problem of subtyping to the
                  problem of typability for F+$\eta$, thus proving the
                  undecidability of typability.
                  The proof methods are similar in outline to those
                  used to prove the undecidability of typability for
                  System F, but the fine details differ greatly.}
}

@COMMENT{{PeterhasdroppedthenextentryasaChurchreportinfavorofWells:APAL-1999-v98-no-notebelow.Thishasbeendoneafter2unrespondede-mailstotheauthor.PleasecontactPeterbeforeturningitintoaChurchReport.}}


@ARTICLE{Wells:APAL-1999-v98-no-note,
  AUTHOR = {J. B. Wells},
  TITLE = {Typability and Type Checking in {S}ystem {F} Are
                  Equivalent and Undecidable},
  JOURNAL = {Ann.\ Pure Appl.\ Logic},
  VOLUME = 98,
  NUMBER = {1--3},
  YEAR = 1999,
  PAGES = {111--156},
  CHURCHREPORT = {yes},
  DOCUMENTURL = {http://www.church-project.org/reports/Wells:APAL-1999-v98-no-note.html},
  POSTSCRIPT = {http://www.macs.hw.ac.uk/~jbw/papers/f-undecidable-APAL.ps.gz},
  XNOTE = {Supersedes \cite{Wells:LICS-1994}},
  ABSTRACT = {Girard and Reynolds independently invented System~F
                  (a.k.a.\ the second-order polymorphically typed
                  lambda calculus) to handle problems in logic and
                  computer programming language design, respectively.
                  Viewing F in the \emph{Curry style}, which
                  associates types with untyped lambda terms, raises
                  the questions of \emph{typability} and \emph{type
                  checking}.  Typability asks for a term whether there
                  exists some type it can be given.  Type checking
                  asks, for a particular term and type, whether the
                  term can be given that type.  The decidability of
                  these problems has been settled for restrictions and
                  extensions of F and related systems and complexity
                  lower-bounds have been determined for typability in
                  F, but this report is the first to resolve whether
                  these problems are decidable for System~F.
                  \par
                  This report proves that type checking in F is
                  undecidable, by a reduction from
                  \emph{semi-unification}, and that typability in F is
                  undecidable, by a reduction from type checking.
                  Because there is an easy reduction from typability
                  to type checking, the two problems are equivalent.
                  The reduction from type checking to typability uses
                  a novel method of constructing lambda terms that
                  simulate arbitrarily chosen type environments.  All
                  of the results also hold for the $\lambda
                  I$-calculus.}
}


@TECHREPORT{Wells:UMSR-1995,
  AUTHOR = {J. B. Wells},
  TITLE = {The Undecidability of {Mitchell's} Subtyping
                  Relation},
  INSTITUTION = {Comp.\ Sci.\ Dept., Boston Univ.},
  YEAR = 1995,
  MONTH = DEC,
  DOCUMENTURL = {http://www.church-project.org/reports/Wells:UMSR-1995.html},
  POSTSCRIPT = {http://www.cs.bu.edu/ftp/pub/jbw/types/subtyping-undecidable.ps.gz},
  POSTSCRIPTB = {http://www.cs.bu.edu/techreports/ps/1995-019-subtyping-undecidable.ps.gz},
  REMARK = {Doesn't have tech report number in the actual paper.},
  TYPE = {Tech.\ Rep.},
  NUMBER = {95-019},
  CHURCHREPORT = {yes},
  ABSTRACT = {Mitchell defined and axiomatized a subtyping
                  relationship (also known as \emph{containment},
                  \emph{coercibility}, or \emph{subsumption}) over the
                  types of System F (with ``$\to$'' and
                  ``$\forall$'').  This subtyping relationship is quite
                  simple and does not involve bounded
                  quantification.  Tiuryn and Urzyczyn quite recently
                  proved this subtyping relationship to be
                  undecidable.  This paper supplies a new
                  undecidability proof for this subtyping
                  relationship.  First, a new syntax-directed
                  axiomatization of the subtyping relationship is
                  defined.  Then, this axiomatization is used to prove
                  a reduction from the undecidable problem of
                  \emph{semi-unification} to subtyping.  The
                  undecidability of subtyping implies the
                  undecidability of \emph{type checking} for System F
                  extended with Mitchell's subtyping, also known as
                  ``F plus eta''.}
}


@UNPUBLISHED{Kfoury:TTTR-1996,
  AUTHOR = {Assaf J. Kfoury},
  TITLE = {A Linearization of the Lambda-Calculus},
  NOTE = {A refereed version
                  is~\cite{Kfoury:JLC-2000-v10n3}. This version was
                  presented at the Glasgow Int'l School on Type Theory
                  \& Term Rewriting},
  PDF = {http://www.church-project.org/reports/electronic/Kfoury:TTTR-1996.pdf},
  URL = {http://www.church-project.org/reports/electronic/Kfoury:TTTR-1996.pdf.gz},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Kfoury:TTTR-1996.ps.gz},
  YEAR = 1996,
  MONTH = SEP,
  CHURCHREPORT = {yes},
  ABSTRACT = {We embed the standard $\lambda$-calculus, denoted $\Lambda$,
                  into two larger $\lambda$-calculi,
                  denoted $\Lambda^\land$ and $\&\Lambda^\land$.
                  The standard notion of $\beta$-reduction for $\Lambda$
                  corresponds to two new notions of reduction,
                  $\beta^{\land}$ for $\Lambda^\land$ and
                  $\&\beta^{\land}$ for $\&\Lambda^\land$. A distinctive
                  feature of our new calculus $\Lambda^\land$
                  (resp., $\&\Lambda^\land$) is that, in every function
                  application, an argument is used at most once (resp.,
                  exactly once) in the body of the function. We establish
                  various connections between the three notions of reduction,
                  $\beta$, $\beta^{\land}$ and  $\&\beta^{\land}$. As a
                  consequence, we provide an alternative framework to study
                  the relationship between $\beta$-weak normalization and
                  $\beta$-strong normalization, and give a new proof of the
                  oft-mentioned equivalence between $\beta$-strong
                  normalization of standard $\lambda$-terms and typability in
                  a system of ``intersection types''. },
  COMMENT = {The funny order of things in the note is to work
                  around the way BibTeX would really screw up the
                  meaning by putting ", 1996" after the note, implying
                  falsely that the year has something to do with the
                  note.}
}


@ARTICLE{Kfoury:JLC-2000-v10n3,
  ITRSPAPER = {yes},
  AUTHOR = {Assaf J. Kfoury},
  TITLE = {A Linearization of the Lambda-Calculus},
  CROSSREF = {JLC-2000-v10n3},
  PAGES = {411--436},
  DOCUMENTURL = {http://www.church-project.org/reports/Kfoury:JLC-2000-v10n3.html},
  PDF = {http://www.church-project.org/reports/electronic/Kfoury:JLC-2000-v10n3.pdf},
  URL = {http://www.church-project.org/reports/electronic/Kfoury:JLC-2000-v10n3.pdf.gz},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Kfoury:JLC-2000-v10n3.ps.gz},
  CHURCHREPORT = {yes},
  ABSTRACT = {We embed the standard $\lambda$-calculus, denoted $\Lambda$,
                  into two larger $\lambda$-calculi,
                  denoted $\Lambda^\land$ and $\&\Lambda^\land$.
                  The standard notion of $\beta$-reduction for $\Lambda$
                  corresponds to two new notions of reduction,
                  $\beta^{\land}$ for $\Lambda^\land$ and
                  $\&\beta^{\land}$ for $\&\Lambda^\land$. A distinctive
                  feature of our new calculus $\Lambda^\land$
                  (resp., $\&\Lambda^\land$) is that, in every function
                  application, an argument is used at most once (resp.,
                  exactly once) in the body of the function. We establish
                  various connections between the three notions of reduction,
                  $\beta$, $\beta^{\land}$ and  $\&\beta^{\land}$. As a
                  consequence, we provide an alternative framework to study
                  the relationship between $\beta$-weak normalization and
                  $\beta$-strong normalization, and give a new proof of the
                  oft-mentioned equivalence between $\beta$-strong
                  normalization of standard $\lambda$-terms and typability in
                  a system of ``intersection types''. }
}


@UNPUBLISHED{Kfoury:TTTR-1996a,
  ITRSPAPER = {yes},
  AUTHOR = {Assaf J. Kfoury},
  TITLE = {Beta-Reduction as Unification},
  NOTE = {A refereed extensively edited version
                  is~\cite{Kfoury:Rasiowa-memorial}.  This preliminary version was
                  presented at the Helena Rasiowa Memorial Conference},
  YEAR = {1996},
  MONTH = JUL,
  CHURCHREPORT = {yes},
  PDF = {http://www.church-project.org/reports/electronic/Kfoury:TTTR-1996a.pdf},
  URL = {http://www.church-project.org/reports/electronic/Kfoury:TTTR-1996a.pdf.gz},
  ABSTRACT = {We define a new unification problem, which we call
    {\em $\beta$-unification} and which can be used to characterize
    the $\beta$-strong normalization of terms in the
    $\lambda$-calculus. We prove the undecidability
    of $\beta$-unification, its connection with the system
    of intersection types, and several of its basic
    properties.}
}


@INCOLLECTION{Kfoury:Rasiowa-memorial,
  ITRSPAPER = {yes},
  AUTHOR = {Assaf J. Kfoury},
  TITLE = {Beta-Reduction as Unification},
  YEAR = 1999,
  BOOKTITLE = {Logic, Algebra, and Computer Science (H. Rasiowa
                  Memorial Conference, December 1996), Banach Center
                  Publication, Volume 46},
  PAGES = {137--158},
  PUBLISHER = {Springer-Verlag},
  EDITOR = {D. Niwinski},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Kfoury:Rasiowa-memorial.ps.gz},
  PDF = {http://www.church-project.org/reports/electronic/Kfoury:Rasiowa-memorial.pdf},
  URL = {http://www.church-project.org/reports/electronic/Kfoury:Rasiowa-memorial.pdf.gz},
  DOCUMENTURL = {http://www.church-project.org/reports/Kfoury:Rasiowa-memorial.html},
  NOTE = {Supersedes~\cite{Kfoury:TTTR-1996a} but omits a few proofs included in the
          latter},
  ABSTRACT = {We define a new unification problem, which we call
    {\em $\beta$-unification} and which can be used to characterize
    the $\beta$-strong normalization of terms in the
    $\lambda$-calculus. We prove the undecidability
    of $\beta$-unification, its connection with the system
    of intersection types, and several of its basic
    properties.},
  CHURCHREPORT = {yes}
}


@ARTICLE{Bug+Per:IAC-2000,
  AUTHOR = {Michele Bugliesi and Santiago M. Pericas-Geertsen},
  TITLE = {Type Inference for variant object types},
  JOURNAL = {Inform.\ {\&} Comput.},
  YEAR = 2000,
  PDF = {http://cs-people.bu.edu/santiago/Papers/Bug+Per:TR-2000.pdf},
  POSTSCRIPT = {http://cs-people.bu.edu/santiago/Papers/Bug+Per:TR-2000.ps},
  XURL = {http://cs-people.bu.edu/santiago/Papers/Bug+Per:TR-2000.pdf},
  CHURCHREPORT = {yes},
  ABSTRACT = { Existing type systems for object calculi are based
                  on invariant subtyping. Subtyping invariance is
                  required for soundness of static typing in the
                  presence of method overrides, but it is often in the
                  way of the expressive power of the type
                  system. Flexibility of static typing can be
                  recovered in different ways: in first-order systems,
                  by the adoption of object types with
                  \textit{variance annotations}, in second-order
                  systems by resorting to \textit{Self types}. Type
                  inference is known to be P-complete for first-order
                  systems of finite and recursive object types, and
                  NP-complete for a restricted version of Self
                  types. The complexity of type inference for systems
                  with variance annotations is yet unknown. This paper
                  presents a new object type system based on the
                  notion of \textem{Split types}, a form of object
                  types where every method is assigned two types,
                  namely, an update type and a select type. The
                  subtyping relation that arises for Split types is
                  \textem{variant} and, as a result, subtyping can be
                  performed both in \textem{width} and in
                  \textem{depth}. The new type system generalizes all
                  the existing first-order type systems for objects,
                  including systems based on variance
                  annotations. Interestingly, the additional
                  expressive power does not affect the complexity of
                  the type inference problem, as we show by presenting
                  an O(n^3) inference algorithm.}
}


@INPROCEEDINGS{Bug+Per:FOOL-2000,
  AUTHOR = {Michele Bugliesi and Santiago M. Pericas-Geertsen},
  TITLE = {Depth Subtyping and Type Inference for Object
                  Calculi},
  CROSSREF = {FOOL2000},
  YEAR = 2000,
  PDF = {http://cs-people.bu.edu/santiago/Papers/Bug+Per:EA-FOOL-2000.pdf},
  XURL = {http://cs-people.bu.edu/santiago/Papers/Bug+Per:EA-FOOL-2000.pdf},
  ABSTRACT = {We present a new type system based on the notion of
                  Split types. In this system, every method is
                  assigned two types, namely, an update type and a
                  select type. We show that the system of Split types
                  is strictly more powerful than the system of
                  recursive types and that type inference remains
                  decidable and feasible. We include a number of
                  interesting examples not typable with recursive
                  types that are typable with Split types. In
                  particular, we demonstrate that the subtyping
                  relation needed to encode the \lambda-calculus into
                  the Abadi and Cardelli's \varsigma-calculus
                  holds. We also present a polynomial-time algorithm
                  that infers Split types and show that it is sound
                  and complete with respect to the type system. We
                  conclude our presentation by relating the typing
                  power of Split types to the typing power of other
                  systems, such as, the system of recursive types with
                  variance annotations and the system of Self types.},
  CHURCHREPORT = {yes}
}


@INPROCEEDINGS{Kfo+Per:LICS-1999,
  TITLE = {Type Inference for Recursive Definitions},
  AUTHOR = {Assaf J. Kfoury and Santiago M. Pericas-Geertsen},
  PAGES = {119--128},
  YEAR = 1999,
  CROSSREF = {LICS1999},
  PDF = {http://cs-people.bu.edu/santiago/Papers/Kfo+Per:EA-LICS-1999.pdf},
  POSTSCRIPT = {http://cs-people.bu.edu/santiago/Papers/Kfo+Per:EA-LICS-1999.ps},
  XURL = {http://cs-people.bu.edu/santiago/Papers/Kfo+Per:EA-LICS-1999.pdf},
  ABSTRACT = {We consider type systems that combine universal types,
                  recursive types, and object types. We study type inference
                  in these systems under a rank restriction, following
                  Leivant's notion of rank.
                  To motivate our work, we present several examples showing
                  how our systems can be used to type programs encountered
                  in practice.
                  We show that type inference in the rank-k system is decidable
                  for k <= 2 and undecidable for k >= 3.
                  (Similar results based on different techniques are known
                  to hold for System F, without recursive types and object
                  types.) Our undecidability result is obtained by a reduction
                  from a particular adaptation (which we call "regular") of
                  the semi-unification problem and whose undecidability is,
                  interestingly, obtained by methods totally different
                  from those used in the case of standard (or finite)
                  semi-unification.},
  CHURCHREPORT = {yes}
}


@TECHREPORT{Kfo+Per:TIRD-1999,
  TITLE = {Type Inference for Recursive Definitions},
  AUTHOR = {Assaf J. Kfoury and Santiago M. Pericas-Geertsen},
  POSTSCRIPT = {http://cs-people.bu.edu/santiago/Papers/Kfo+Per:TR-1999.ps},
  PDF = {http://cs-people.bu.edu/santiago/Papers/Kfo+Per:TR-1999.pdf},
  XURL = {http://cs-people.bu.edu/santiago/Papers/Kfo+Per:TR-1999.pdf},
  YEAR = 1999,
  INSTITUTION = {Comp.\ Sci.\ Dept., Boston Univ.},
  LONGINSTITUTION = {Computer Science Department, Boston University},
  NOTE = {Expanded full report of \cite{Kfo+Per:LICS-1999}},
  ABSTRACT = {We consider type systems that combine universal types,
                  recursive types, and object types. We study type inference
                  in these systems under a rank restriction, following
                  Leivant's notion of rank.
                  To motivate our work, we present several examples showing
                  how our systems can be used to type programs encountered
                  in practice.
                  We show that type inference in the rank-k system is decidable
                  for k <= 2 and undecidable for k >= 3.
                  (Similar results based on different techniques are known
                  to hold for System F, without recursive types and object
                  types.) Our undecidability result is obtained by a reduction
                  from a particular adaptation (which we call "regular") of
                  the semi-unification problem and whose undecidability is,
                  interestingly, obtained by methods totally different
                  from those used in the case of standard (or finite)
                  semi-unification.},
  CHURCHREPORT = {yes}
}


@INPROCEEDINGS{Amt+Tur:Faithful-ESOP-2000,
  ITRSPAPER = {yes},
  TITLE = {Faithful Translations between Polyvariant Flows and Polymorphic Types},
  AUTHOR = {Torben Amtoft and Franklyn Turbak},
  CROSSREF = {ESOP2000},
  PAGES = {26--40},
  PDF = {http://www.church-project.org/reports/electronic/Amt+Tur:Faithful-ESOP-2000.pdf},
  URL = {http://www.church-project.org/reports/electronic/Amt+Tur:Faithful-ESOP-2000.pdf.gz},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Amt+Tur:Faithful-ESOP-2000.ps.gz},
  DOCUMENTURL = {http://www.church-project.org/reports/Amt+Tur:Faithful-ESOP-2000.html},
  ABSTRACT = {Recent work has shown equivalences between
                  various type systems and flow logics.
                  Ideally, the translations upon which such
                  equivalences are based should be {\em faithful}
                  in the sense that information is not lost in
                  round-trip translations from flows to types and back
                  or from types to flows and back. Building on the work of
                  Nielson \& Nielson and of Palsberg \& Pavlopoulou,
                  we present the first faithful translations between
                  a class of finitary polyvariant flow analyses
                  and a type system supporting polymorphism
                  in the form of intersection and union types.
                     Additionally,
                  our flow/type correspondence solves several
                  open problems posed by Palsberg \& Pavlopoulou:
                   (1) it expresses call-string based polyvariance
                  (such as k-CFA) as well as argument based polyvariance;
                   (2) it enjoys a subject reduction property
                  for flows as well as for types; and
                   (3) it supports a flow-oriented perspective
                  rather than a type-oriented one.},
  CHURCHREPORT = {yes}
}


@TECHREPORT{Amt+Tur:Faithful-TR-2000,
  ITRSPAPER = {yes},
  TITLE = {Faithful Translations between Polyvariant Flows and Polymorphic Types},
  AUTHOR = {Torben Amtoft and Franklyn Turbak},
  YEAR = 2000,
  INSTITUTION = {Comp.\ Sci.\ Dept., Boston Univ.},
  LONGINSTITUTION = {Computer Science Department, Boston University},
  NUMBER = {BUCS-TR-2000-01},
  PDF = {http://www.church-project.org/reports/electronic/Amt+Tur:Faithful-TR-2000.pdf},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Amt+Tur:Faithful-TR-2000.ps},
  ABSTRACT = {Recent work has shown equivalences between
                  various type systems and flow logics.
                  Ideally, the translations upon which such
                  equivalences are based should be {\em faithful}
                  in the sense that information is not lost in
                  round-trip translations from flows to types and back
                  or from types to flows and back. Building on the work of
                  Nielson \& Nielson and of Palsberg \& Pavlopoulou,
                  we present the first faithful translations between
                  a class of finitary polyvariant flow analyses
                  and a type system supporting polymorphism
                  in the form of intersection and union types.
                     Additionally,
                  our flow/type correspondence solves several
                  open problems posed by Palsberg \& Pavlopoulou:
                   (1) it expresses call-string based polyvariance
                  (such as k-CFA) as well as argument based polyvariance;
                   (2) it enjoys a subject reduction property
                  for flows as well as for types; and
                   (3) it supports a flow-oriented perspective
                  rather than a type-oriented one.},
  NOTE = {Expanded full report of \cite{Amt+Tur:Faithful-ESOP-2000}. To appear Fall 2000, but a \emph{DRAFT} version is available.},
  CHURCHREPORT = {yes}
}


@INPROCEEDINGS{Mac+Tur:Link-time-ESOP-2000,
  TITLE = {A Calculus for Link-time Compilation},
  AUTHOR = {Elena Machkasova and Franklyn A. Turbak},
  CROSSREF = {ESOP2000},
  PAGES = {260--274},
  CHURCHREPORT = {yes},
  PDF = {http://www.church-project.org/reports/electronic/Mac+Tur:Link-time-ESOP-2000.pdf},
  URL = {http://www.church-project.org/reports/electronic/Mac+Tur:Link-time-ESOP-2000.pdf.gz},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Mac+Tur:Link-time-ESOP-2000.ps.gz}
}


@TECHREPORT{Mac+Tur:Link-time-TR-2000,
  TITLE = {A Calculus for Link-time Compilation},
  AUTHOR = {Elena Machkasova and Franklyn Turbak},
  YEAR = 2000,
  INSTITUTION = {Comp.\ Sci.\ Dept., Boston Univ.},
  LONGINSTITUTION = {Computer Science Department, Boston University},
  NOTE = {Expanded full report of
                  \cite{Mac+Tur:Link-time-ESOP-2000}},
  CHURCHREPORT = {yes}
}


@PHDTHESIS{neergaard-capld-2004,
  AUTHOR = {M{\o}ller Neergaard, Peter},
  TITLE = {Complexity Aspects of Programming Language Design---From Logspace to Elementary Time via Proofnets and Intersection Types},
  SCHOOL = {Brandeis University},
  YEAR = 2004,
  MONTH = OCT,
  ABSTRACT = {More than being just a tool for expressing algorithms, a
well-designed programming language allows the user to express her
ideas efficiently.  The design choices, however, affect the efficiency
of the algorithms written in the languages.  It is therefore important
to understand how such choices effect the expressibility of
programming languages.  The dissertation approaches this problem from
two different angles.  
\par
The dissertation presents what appears to be the first resource
independent characterization of the \textsc{logspace}-computable
\emph{functions}.  This is done in the form of a \emph{function
algebra}~BC$^{\mbox{-}}_{\varepsilon}$ that is sound and complete for
\textsc{logspace}.  BC$^{\mbox{-}}_{\varepsilon}$ provides insights
into restricting recursion that might be useful to provide
compile-time guarantees on resource bounds.  Furthermore, by
comparison with work by Bellantoni and Cook, it highlights linearity
as a potential distinction between~\textsc{logspace}\ and
\textsc{ptime}.
\par
The dissertation also formalizes how successful type inference
fundamentally depends on the \emph{amnesia} of the type system: the
fact that the type system forgets information about the program.
\emph{Intersection type systems} without \emph{idempotency} provides
an exact analysis where all information is retained.  The dissertation
shows that in such intersection type systems, normalization is
equivalent to type inference in \emph{every single case}.  Time bounds
on type inference and normalization are thus identical and doing
compile-time type inference is useless.
\par 
The latter part reveals that \emph{expansion variables} proposed for
type inference are closely related to the boxes already known from the
\emph{linear logic} technology of \emph{proofnets}.  This hithertho
unknown connection between the two technologies suggests fruitful
contributions between the two fields. Moreover, it extends and
formalizes a previously known connection between intersection types
and proofnets.},
  PDF = {http://www.linearity.org/turtle/down/pmn-dissertation.pdf},
  PMNWWW = {dissertation},
  CHURCHREPORT = {yes}
}


@ARTICLE{neergaard-jfp-ta,
  AUTHOR = {M{\o}ller Neergaard, Peter},
  TITLE = {A Bargain for Intersection Types: A Simple Strong Normalization Proof},
  JOURNAL = {J.~Funct.\ Programming},
  NOTE = {To appear},
  PMNWWW = {journal},
  CHURCHREPORT = {yes},
  PDF = {http://www.church-project.org/reports/electronic/neergaard-jfp-ta.pdf},
  URL = {http://www.church-project.org/reports/electronic/neergaard-jfp-ta.pdf.gz},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/neergaard-jfp-ta.ps.gz},
  ABSTRACT = {This pearl gives a discount proof of the folklore theorem that every
  strongly $\beta$-normalizing $\lambda$-term is typable with an
  intersection type.  (We consider typings that do not use the empty
  intersection~$\omega$ which can type any term.) The proof uses the
                  perpetual  reduction
  strategy which finds a longest path.  This is a simplification over existing proofs that
  consider any longest reduction path.  The choice of reduction
  strategy avoids the need for weakening or strengthening of type derivations.  The proof
  becomes a bargain because it works for more intersection type
  systems, while being simpler than existing proofs.}
}


@TECHREPORT{Neergaard-brtcl-2004,
  AUTHOR = {M{\o}ller Neergaard, Peter},
  TITLE = {{BC$^{\textrm{-}}_\epsilon$}: A Recursion-Theoretic Characterization of \textsc{logspace}},
  INSTITUTION = {Brandeis University},
  YEAR = 2004,
  MONTH = MAR,
  NOTE = {Preliminary version},
  CHURCHREPORT = {yes},
  ABSTRACT = {We present {BC$^{\textrm{-}}_\epsilon$} which is a function algebra that is sound and
  complete for \textsc{logspace}.  It is based on the novel
  recursion-theoretic principle of generalized recursion where the
  step length of primitive recursion can be varied at each step.  This
  allows elegant representations of functions like logarithm and
  division.   Unlike characterizations found in the literature, it is
  noticeable that there does not appear to be a way to represent pairs
  in the algebra.\par
  The soundness proof uses a simulation based on ``computational
  amnesia'' where, analogously to tail recursion optimization, a
  recursive call replaces its own activation record.  Even though the
  call is not necessarily tail, we recover the full recursion by
  repeatedly restarting the computation.},
  PDF = {http://www.church-project.org/reports/electronic/Neergaard-brtcl-2004.pdf},
  URL = {http://www.church-project.org/reports/electronic/Neergaard-brtcl-2004.pdf.gz},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Neergaard-brtcl-2004.ps.gz},
  PMNWWW = {techreport}
}


@INPROCEEDINGS{neergaard-aplas-2004,
  AUTHOR = {M{\o}ller Neergaard, Peter},
  TITLE = {A Functional Language for Logarithmic Space},
  CROSSREF = {APLAS2004},
  PAGES = {311--326},
  DOI = {http://www.springerlink.com/(qe2jbx55cx2ecx55i0bnjp45)/app/home/contribution.asp?referrer=parent&backto=issue,21,29;journal,667,3858;linkingpublicationresults,1:105633,1},
  ABSTRACT = {%
More than being just a tool for expressing algorithms, a well-designed
programming language allows the user to express her ideas efficiently.
The design choices however effect the efficiency of the algorithms
written in the languages.  It is therefore important to understand how
such choices effect the expressibility of programming languages.
\par 
The paper pursues the very low complexity programs by presenting a
first-order function algebra~\textrm{BC}$^{\textrm{-}}_\varepsilon$
that captures exactly \textsc{logspace}, the functions computable in
logarithmic space.  This gives insights into the expressiveness of
recursion.
\par 
The important technical features of
\textrm{BC}$^{\textrm{-}}_{\varepsilon}$ are (1) a separation of
variables into safe and normal variables where recursion can only be
done over the latter; (2) linearity of the recursive call; and
(3) recursion with a variable step length (course-of-value
  recursion). Unlike formulations of \textsc{logspace} via Turing
machines, \textrm{BC}$^{\textrm{-}}_{\varepsilon}$ makes no references
to outside resource measures, e.g., the size of the memory used.
This appears to be the first such characterization of
\textsc{logspace}-computable functions (not just predicates).
\par 
The proof that all \textrm{BC}$^{\textrm{-}}_{\varepsilon}$-programs can
be evaluated in \textsc{logspace} is of separate interest to
programmers: it trades space for time and evaluates recursion with at
most one recursive call without a call stack.},
  CHURCHREPORT = {yes},
  PMNWWW = {conference},
  PDF = {http://www.church-project.org/reports/electronic/neergaard-aplas-2004.pdf},
  URL = {http://www.church-project.org/reports/electronic/neergaard-aplas-2004.pdf.gz},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/neergaard-aplas-2004.ps.gz},
  COPYRIGHT = {\copyright\ Springer-Verlag; Appears in the
\begin{rawhtml}\end{rawhtml}Lecture Notes in Computer Science\begin{rawhtml}\end{rawhtml} series}
}


@MASTERSTHESIS{Neergaard-WSNK-1999,
  CROSSREF = {Neergaard:WSNK-1999},
  PDF_A4 = {http://www.church-project.org/reports/electronic/Neergaard-WSNK-1999.pdf},
  URL_A4 = {http://www.church-project.org/reports/electronic/Neergaard-WSNK-1999.pdf.gz},
  POSTSCRIPT_A4 = {http://www.church-project.org/reports/electronic/Neergaard-WSNK-1999.ps.gz},
  ABSTRACT = {The thesis studies certain aspects of normalisation
                  in the lambda-calculus. It begins with a study of
                  the notions conservation and uniform
                  normalisation. Conservation means that infinite
                  reduction paths are preserved under
                  reduction. Uniform normalisation means that the term
                  can either not be reduced to a normal form, or that
                  all ways of reducing the term will eventually lead
                  to a normal form. \par The classical conservation
                  theorem for Lambda I has been formulated using
                  either of the notions conservation and uniform
                  normalisation. The reason for the indistinctness in
                  the formulation of the conservation theorem is that
                  Lambda I is closed under beta-reduction, which in
                  Lambda I does not erase subterms. In this situation
                  uniform normalisation implies conservation, and
                  conservation also implies uniform
                  normalisation. However, when turning to erasing
                  reductions the distinction becomes important as
                  conservation no longer implies uniform
                  normalisation. This insight is elaborated in a new
                  technique for finding uniformly normalising subsets
                  of a lambda-calculus. The technique uses a
                  combination of a syntactic and a semantic criterion
                  and it is applied in several ways:
                  \begin{itemize}\item The technique is used to find a
                  new uniformly normalising subset of the basic
                  lambda-calculus. This uniformly normalising subset
                  includes some terms with erasing redexes, so-called
                  Kr-redexes. \item The technique is also used in a
                  typed setting to find a uniformly normalising subset
                  of the typed lambda-calculus Lambda M corresponding
                  to minimal first-order logic through the
                  Curry-Howard isomorphism. \item This uniformly
                  normalising subset is used to infer strong
                  normalisation from weak normalisation for Lambda
                  M. This is a non-trivial extension of techniques
                  developed recently by S{\o}rensen and Xi to infer
                  strong normalisation from weak normalisation of the
                  same notion of reduction. \end{itemize}Furthermore,
                  the thesis considers the type system of classical
                  first-order logic, which allows typing of exception
                  handling. An analysis concludes that it is not
                  possible to make a direct extension of the technique
                  by S{\o}rensen and Xi to this system.},
  CHURCHREPORT = {yes},
  PMNWWW = {report},
  URL = {http://www.linearity.org/turtle/reports/Neergaard-WSNK-1999.html}
}


@MASTERSTHESIS{Neergaard:WSNK-1999,
  AUTHOR = {M{\o}ller Neergaard, Peter},
  TITLE = {Weak and Strong Normalization, $\mathbf{K}$-redexes,
                  and First-Order Logic},
  SCHOOL = {{DIKU}},
  YEAR = 1999,
  ADDRESS = AUG,
  NOTE = {DIKU Technical Report 99/11},
  XPOSTSCRIPT = {ftp://ftp.diku.dk/diku/semantics/papers/D-399.ps.gz}
}

@COMMENT{{HERESTARTSKAMAREDDINE'SARTICLES}}

@COMMENT{{ExplicitSubstitutions}}

@COMMENT{{Logic}}

@COMMENT{{Higher-OrderUnification}}

@COMMENT{{TypesandLambda}}

@COMMENT{{Termination}}

@COMMENT{{BOOKS}}

@COMMENT{{EDITEDVOLUMES}}


@ARTICLE{JLC-2000-v10n3,
  AUTHOR = {},
  TITLE = {},
  JOURNAL = {J.~Logic Comput.},
  YEAR = 2000,
  EDITOR = {Fairouz Kamareddine and Jan Willem Klop},
  XEDITOR = {"editor" field is not used by BibTeX style for
                  "article"!!!},
  PUBLISHER = {Oxford University Press},
  XEDITOR = {"publisher" field is not used by BibTeX style for
                  "article"!!!},
  VOLUME = 10,
  NUMBER = 3,
  NOTE = {Special issue on Type Theory and Term Rewriting. Kamareddine and Klop (editors)}
}

@COMMENT{{HEREENDSKAMAREDDINE'SARTICLES}}


@ARTICLE{Nee-Sor-IAC-2002-v178n1,
  CROSSREF = {Nee+Sor:IAC-ta},
  PMNWWW = {journal},
  CHURCHREPORT = {yes},
  ABSTRACT = {For a notion of reduction in a $\lambda$-calculus
                  one can ask whether a term satisfies
                  \emph{conservation} and \emph{uniform
                  normalization}. Conservation means that single-step
                  reductions of the term preserve infinite reduction
                  paths from the term. Uniform normalization means
                  that either the term will have no reduction paths
                  leading to a normal form, or all reduction paths
                  will lead to a normal form. \par In the classical
                  \emph{conservation theorem} for $\Lambda^I$ the
                  distinction between the two notions is not clear:
                  uniform normalization implies conservation, and
                  conservation also implies uniform normalization. The
                  reason for this is that $\Lambda^I$ is closed under
                  reduction, due to the fact that reductions never
                  erase terms in $\Lambda^I$. More generaly for
                  non-erasing reductions, the two notions are
                  equivalent on a set closed under reduction. However,
                  when turning to erasing reductions the distinction
                  becomes important as conservation no longer implies
                  uniform normalization. \par This paper presents a
                  new technique for finding uniformly normalizing
                  subsets of a $\lambda$-calculus. This is done by
                  combining a syntactic and a semantic criterion. The
                  technique is demonstrated by several
                  applications. The technique is used to present a new
                  uniformly normalizing subset of the pure
                  $\lambda$-calculus; this subset is a superset
                  of~$\Lambda^I$ and thus contains erasing
                  $\mathbf{K}$-redexes. The technique is also used to
                  prove strong normalization from weak normalization
                  of the simply typed $\lambda$-calculus extended with
                  pairs; this is an extension of techniques developed
                  recently by S{\o}rensen and Xi. Before presenting
                  the technique the paper presents a simple proof of a
                  slightly weaker form of the characterization of
                  perpetual redexes by Bergstra and Klop; this is a
                  stepping for the later applications of the
                  technique.},
  COPYRIGHT = {\copyright{}This paper is Copyright Elsevier.},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Nee-Sor-IAC-2002-v178n1.ps.gz},
  PDF = {http://www.church-project.org/reports/electronic/Nee-Sor-IAC-2002-v178n1.pdf},
  URL = {http://www.church-project.org/reports/electronic/Nee-Sor-IAC-2002-v178n1.pdf.gz}
}


@ARTICLE{Nee+Sor:IAC-ta,
  AUTHOR = {M{\o}ller Neergaard, Peter  and Morten Heine
                  B[j{\o}rnlund] S{\o}rensen},
  TITLE = {Conservation and Uniform Normalization in
                  $\lambda$-calculi with Erasing Reductions},
  JOURNAL = {Information and Computation},
  VOLUME = 178,
  NUMBER = 1,
  PAGES = {149--179},
  MONTH = OCT,
  YEAR = 2002
}


@INPROCEEDINGS{Nee-Mai-LIS-ICC02,
  AUTHOR = {M{\o}ller Neergaard, Peter and Harry G. Mairson},
  TITLE = {{LAL} Is Square: Representation and Expressiveness
                  in Light Affine Logic},
  CROSSREF = {ICC2002},
  CHURCHREPORT = {yes},
  PMNWWW = {conference},
  ABSTRACT = {We focus on how the choice of input-output
                  representation has a crucial impact on the
                  expressiveness of so-called ``logics of polynomial
                  time.'' Our analysis illustrates this dependence in
                  the context of \emph{Light Affine Logic} (LAL),
                  which is both a restricted version of Linear Logic,
                  and a primitive functional programming language with
                  restricted sharing of arguments. By slightly
                  relaxing representation conventions, we derive
                  doubly-exponential expressiveness bounds for this
                  ``logic of polynomial time.'' We emphasize that
                  \emph{squaring} is the unifying idea that relates
                  upper bounds on cut elimination for LAL with lower
                  bounds on representation. Representation issues
                  arise in the simulation of
                  \textsc{dtime}$(2^{2^n})$, where we construct a {\em
                  uniform family} of proof-nets encoding Turing
                  Machine; specifically, the dependence on $n$ only
                  affects the number of enclosing {\em boxes.} A
                  related technical improvement is the simulation of
                  \textsc{dtime}$(n^k)$ in depth~$O(\log k)$ LAL
                  proof-nets. The resulting upper bounds on cut
                  elimination then satisfy the properties of a
                  \emph{first-class} polynomial Turing Machine
                  simulation, where there is a fixed polynomial
                  slowdown in the simulation of any polynomial
                  computation.},
  PDF = {http://www.church-project.org/reports/electronic/Nee+Mai:LIS-ICC02.pdf},
  URL = {http://www.church-project.org/reports/electronic/Nee+Mai:LIS-ICC02.pdf.gz},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Nee+Mai:LIS-ICC02.ps}
}


@UNPUBLISHED{Nee-Mai-how-light-is-safe-rec,
  CROSSREF = {Nee-Mai-how-light-is-safe-rec-LICS03},
  ABSTRACT = {We investigate the simulation of Bellantoni and
                  Cook's function algebra BC by Girard's Light Linear
                  Logic LAL (as amended by Asperti). Both of these
                  languages characterize exactly the polynomial time
                  functions. Given a $\textsc{ptime}$ function $f$
                  described in BC program $\phi_f$, how can we
                  translate $\phi_f$ into LAL? \par The best known
                  translation, due to Murawski and Ong, compiles only
                  the \emph{linear} fragment $\textsc{bc}^-$, where
                  \emph{safe variables} cannot be shared. We show that
                  this fragment can be evaluated in
                  $\textsc{logspace}$. Next, we prove that extensions
                  of their approach to the full BC algebra, as well as
                  any translation that interprets integers and
                  primitive recursion via their standard, System
                  F-inspired inductive type coding, cannot provide a
                  correct translation into LAL. Finally, we provide a
                  correct translation, based on generalizing Turing
                  machine simulations into an SECD compiler, realized
                  in LAL. We further elaborate this translation so
                  that it is compositional on the BC combinators.},
  PDF = {http://www.church-project.org/reports/electronic/Nee-Mai-how-light-is-safe-rec.pdf},
  URL = {http://www.church-project.org/reports/electronic/Nee-Mai-how-light-is-safe-rec.pdf.gz},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Nee-Mai-how-light-is-safe-rec.ps},
  CHURCHREPORT = {yes},
  PMNWWW = {conference}
}


@UNPUBLISHED{Nee-Mai-how-light-is-safe-rec-LICS03,
  AUTHOR = {M{\o}ller Neergaard, Peter and Harry G. Mairson},
  TITLE = {How Light is Safe Recursion? {T}ranslations Between
                  Logics of Polynomial Time},
  NOTE = {Unpublished note},
  YEAR = 2003
}


@INPROCEEDINGS{Nee-Mai-icfp-2004,
  ITRSPAPER = {yes},
  AUTHOR = {M{\o}ller Neergaard, Peter and Harry G. Mairson},
  TITLE = {Types, Potency, and Idempotency: {W}hy Nonlinearity
                  and Amnesia Make a Type System Work},
  ABSTRACT = {Useful type inference must be faster than normalization.
  Otherwise, you could check safety conditions by running the program.
  We analyze the relationship between bounds on normalization and type
  inference.  We show how the success of type inference is
  fundamentally related to the \emph{amnesia} of the type system: the
  \emph{nonlinearity} by which all instances of a variable are
  constrained to have the same type.
\par  
  Recent work on \emph{intersection types} has advocated their
  usefulness for static analysis and modular compilation.  We analyze
  system~$\mathbb{I}$ (and some instances of its descendant, system~E), an
  intersection type system with a type inference algorithm.  Because
  system~$\mathbb{I}$ lacks \emph{idempotency}, each occurrence of a variable
  requires a distinct type.  Consequently, type inference is
  equivalent to normalization in \emph{every single case}, and time
  bounds on type inference and normalization are identical.  Similar
  relationships hold for other intersection type systems without
  idempotency.
\par  
  The analysis is founded on an investigation of the relationship
  between \emph{linear logic} and intersection types.  We show a lockstep
  correspondence between normalization and type inference.  The latter
  shows the promise of intersection types to facilitate static analyses
  of varied granularity, but also belies an immense challenge: to add
  amnesia to such analysis without losing all of its benefits.},
  CROSSREF = {ICFP2004},
  CHURCHREPORT = {yes},
  PDF = {http://www.church-project.org/reports/electronic/Nee-Mai-icfp-2004.pdf},
  URL = {http://www.church-project.org/reports/electronic/Nee-Mai-icfp-2004.pdf.gz},
  POSTSCRIPT = {http://www.church-project.org/reports/electronic/Nee-Mai-icfp-2004.ps},
  PMNWWW = {conference},
  COPYRIGHT = {\copyright{}ACM, 2004. This is the author's version of
                  the work. It is posted here by permission of ACM for
                  your personal use. Not for redistribution. The
                  definitive version was published in {ACM SIGPLAN
                  Notices}, Volume~39, Issue~9 (September 2004)},
  DOI = {http://portal.acm.org/citation.cfm?doid=1016850.1016871}
}


@UNPUBLISHED{Nee-Mai-rank-bnd-inter-ta,
  AUTHOR = {M{\o}ller Neergaard, Peter and Harry G. Mairson},
  TITLE = {Rank Bounded Intersection: Types, Potency, and
                  Idempotency},
  ABSTRACT = { Intersection type systems realize a \emph{finite
                  polymorphism} where different types for a term are
                  itemized explicitly. We analyze System~$\mathbb{I}$,
                  a rank-bounded intersection type system where
                  intersection is not \emph{associative, commutative,}
                  or \emph{idempotent} (ACI), but includes a
                  substitution mechanism employing {\em expansion
                  variables} that facilitates modular program
                  composition and flow analysis. This type system is
                  used in a prototype intersection type compiler for
                  the Church project. We prove that the problem of
                  type inference is exactly as hard as the problem of
                  normalization: the worst-case cost of both is an
                  elementary function, where the iterated exponential
                  depends on the rank. The key to these results is
                  that simply-typed terms must be linear without ACI,
                  but have the usual nonelementary power with
                  ACI. Further, type inference is \emph{always}
                  synonymous with normalization: the cost of computing
                  the principal typing of any term is exactly the cost
                  of computing its normal form. These results do not
                  hold when AC, and particularly I, is added.},
  NOTE = {This paper is obsolete and has been replaced with \cite{Nee-Mai-icfp-2004}},
  YEAR = 2003,
  CHURCHREPORT = {yes}
}

@COMMENT{{Bookswhicharecollectionsofarticlesmustgoattheendofthefile}}

@COMMENT{{PeterM\ollerNeergaard:thesettingofpmn-ask-for-x-symbolisaddedformysaketoavoidmessingupthebibliographywheneditinginemacs.Thesettingofindent-tabs-modeisforeverybodytohelpavoidunnecessarychangesthatcauseCVSconfusion.LocalVariables:pmn-ask-for-x-symbol:0indent-tabs-mode:nilEnd:Consideralsosettingbibtex-filestoconferences.bib.}}

@COMMENT{{Donotaddentriesotherthancrossreftargetsatendoffile.Donotaddanyentriesafterthispoint.}}


@PROCEEDINGS{APLAS2004,
  TITLE = {Prog.\ Lang.\ and
                  Systems: 2nd Asian Symp.\ ({APLAS} 2004)},
  BOOKTITLE = {Prog.\ Lang.\ and
                  Systems: 2nd Asian Symp.\ ({APLAS} 2004)},
  XADDRESS = {Taipei, Taiwan},
  YEAR = 2004,
  MONTH = NOV,
  KEY = {AP{\relax LAS} '04},
  SERIES = {LNCS},
  PUBLISHER = {Springer-Verlag},
  VOLUME = 3302
}


@PROCEEDINGS{ESOP2000,
  TITLE = {Programming Languages \& Systems, 9th European Symp.\ Programming},
  BOOKTITLE = {Programming Languages \& Systems, 9th European Symp.\ Programming},
  KEY = {ES{\relax OP} '00},
  YEAR = 2000,
  SERIES = {LNCS},
  VOLUME = 1782,
  PUBLISHER = {Springer-Verlag},
  XEDITOR = {G. Smolka},
  TOTALPAGES = 442,
  XMONTH = MAR # {/} # APR,
  XPUBLISHER = {Springer-Verlag Berlin and Heidelberg GmbH & Co. KG},
  ISBN = {3-540-67262-1},
  XADDRESS = {Berlin, Germany},
  DATE = {2000-03-28/---31},
  XNOTE = {held as part of ETAPS 2000}
}


@PROCEEDINGS{ESOP2002,
  TITLE = {Programming Languages \& Systems, 11th European Symp.\ Programming},
  BOOKTITLE = {Programming Languages \& Systems, 11th European Symp.\ Programming},
  KEY = {ES{\relax OP} '02},
  YEAR = 2002,
  SERIES = {LNCS},
  VOLUME = 2305,
  PUBLISHER = {Springer-Verlag},
  TOTALPAGES = {***},
  DATE = {2002-04-08/---12},
  XPUBLISHER = {Springer-Verlag Berlin and Heidelberg GmbH & Co. KG},
  XADDRESS = {Grenoble, France},
  XNOTE = {held as part of ETAPS 2002},
  XEDITOR = {Le M{\'e}tayer, Daniel},
  ISBN = {3-540-43363-5}
}


@PROCEEDINGS{ESOP2003,
  TITLE = {Programming Languages \& Systems, 12th European Symp.\ Programming},
  BOOKTITLE = {Programming Languages \& Systems, 12th European Symp.\ Programming},
  KEY = {ES{\relax OP} '03},
  YEAR = 2003,
  SERIES = {LNCS},
  VOLUME = 2618,
  PUBLISHER = {Springer-Verlag},
  XDATE = {2003-04-07/---11},
  XPUBLISHER = {Springer-Verlag Berlin and Heidelberg GmbH & Co. KG},
  XADDRESS = {Warsaw, Poland},
  XNOTE = {held as part of ETAPS 2003},
  XEDITOR = {Pierpaolo Degano},
  ISBN = {3-540-00886-1}
}


@PROCEEDINGS{ESOP2004,
  TITLE = {Programming Languages \& Systems, 13th European Symp.\ Programming},
  BOOKTITLE = {Programming Languages \& Systems, 13th European Symp.\ Programming},
  KEY = {ES{\relax OP} '04},
  YEAR = 2004,
  SERIES = {LNCS},
  VOLUME = 2986,
  PUBLISHER = {Springer-Verlag},
  XDATE = {2004-03-29/--04-02},
  XPUBLISHER = {Springer-Verlag Berlin and Heidelberg GmbH & Co. KG},
  XADDRESS = {Barcelona, Spain},
  XNOTE = {held as part of ETAPS 2004},
  XEDITOR = {David Schmidt},
  ISBN = {3-540-21313-9}
}


@PROCEEDINGS{ESOP2005,
  TITLE = {Programming Languages \& Systems, 14th European Symp.\ Programming},
  BOOKTITLE = {Programming Languages \& Systems, 14th European Symp.\ Programming},
  KEY = {ES{\relax OP} '05},
  YEAR = 2005,
  SERIES = {LNCS},
  VOLUME = 3444,
  PUBLISHER = {Springer-Verlag},
  XDATE = {2005-04-04/---08},
  XPUBLISHER = {Springer-Verlag Berlin and Heidelberg GmbH & Co. KG},
  XADDRESS = {Edinburgh, Scotland},
  XNOTE = {held as part of ETAPS 2005},
  XEDITOR = {Mooly Sagiv},
  ISBN = {3-540-25435-8},
  DOI = {10.1007/b107380}
}


@PROCEEDINGS{FOOL2000,
  TITLE = {Proc.\ Seventh Workshop on Foundations of Object-Oriented Languages},
  YEAR = 2000,
  KEY = {FO{\relax OL} '00},
  BOOKTITLE = {Proc.\ Seventh Workshop on Foundations of Object-Oriented Languages},
  ADDRESS = {Boston, Mass., U.S.A.}
}


@PROCEEDINGS{ICALP2002,
  TITLE = {Proc.\ 29th Int'l Coll.\ Automata, Languages, and Programming},
  BOOKTITLE = {Proc.\ 29th Int'l Coll.\ Automata, Languages, and Programming},
  SERIES = {LNCS},
  PUBLISHER = {Springer-Verlag},
  VOLUME = 2380,
  YEAR = 2002,
  DATE = {2002-07-08/---13},
  XADDRESS = {Malaga, Spain},
  ISBN = {3-540-43864-5}
}


@PROCEEDINGS{ICC2002,
  TITLE = {Proc.\ Workshop on Implicit Computational Complexity},
  MONTH = JUL,
  YEAR = 2002,
  KEY = {ICC '02},
  BOOKTITLE = {Proc.\ Workshop on Implicit Computational Complexity},
  XPUBLISHER = {DIKU},
  XADDRESS = {Copenhagen, Denmark}
}


@PROCEEDINGS{ICFP1997,
  TITLE = {Proc.\ 1997 Int'l Conf.\ Functional Programming},
  YEAR = 1997,
  KEY = {IC{\relax FP} '97},
  BOOKTITLE = {Proc.\ 1997 Int'l Conf.\ Functional Programming},
  PUBLISHER = {ACM Press},
  XADDRESS = {Amsterdam, The Netherlands},
  XMONTH = JUN # {~9--11},
  DATE = {1997-06-09/---11},
  ISBN = {0-89791-918-1},
  XISSN = {0362-1340},
  XSERIES = {ACM SIGPLAN Notices},
  XVOLUME = {32(8) (August 1997)},
  XORGANIZATION = {ACM}
}


@PROCEEDINGS{ICFP1999,
  TITLE = {Proc.\ 1999 Int'l Conf.\ Functional Programming},
  YEAR = 1999,
  KEY = {IC{\relax FP} '99},
  BOOKTITLE = {Proc.\ 1999 Int'l Conf.\ Functional Programming},
  PUBLISHER = {ACM Press},
  XADDRESS = {Paris, France},
  XMONTH = SEP # {~27--29},
  DATE = {1999-09-27/---29},
  ISBN = {1-58113-111-9},
  XORGANIZATION = {ACM}
}


@PROCEEDINGS{ICFP2001,
  TITLE = {Proc.\ 6th Int'l Conf.\ Functional Programming},
  YEAR = 2001,
  KEY = {IC{\relax FP} '01},
  BOOKTITLE = {Proc.\ 6th Int'l Conf.\ Functional Programming},
  PUBLISHER = {ACM Press},
  XADDRESS = {Firenze, Italy},
  XMONTH = SEP # {~3--5},
  XORGANIZATION = {ACM},
  ISBN = {1-58113-415-0}
}


@PROCEEDINGS{ICFP2004,
  TITLE = {Proc.\ 9th Int'l Conf.\ Functional Programming},
  MONTH = SEP,
  YEAR = 2004,
  KEY = {IC{\relax FP} '04},
  BOOKTITLE = {Proc.\ 9th Int'l Conf.\ Functional Programming},
  PUBLISHER = {ACM Press},
  XADDRESS = {Snowbird, Utah, USA},
  XORGANIZATION = {ACM}
}


@PROCEEDINGS{ICFP2005,
  TITLE = {Proc.\ 10th Int'l Conf.\ Functional Programming},
  MONTH = SEP,
  YEAR = 2005,
  KEY = {IC{\relax FP} '05},
  BOOKTITLE = {Proc.\ 10th Int'l Conf.\ Functional Programming},
  PUBLISHER = {ACM Press},
  XADDRESS = {Tallinn, Estonia},
  XEDITOR = {Olivier Danvy and Benjamin C. Pierce},
  XORGANIZATION = {ACM},
  DATE = {2005-09-26/---28},
  ISBN = {1-59593-064-7}
}


@PROCEEDINGS{ITRS2002,
  XEDITOR = {Steffen van Bakel},
  TITLE = {Proceedings of the 2nd Workshop on Intersection Types and Related Systems},
  BOOKTITLE = {Proceedings of the 2nd Workshop on Intersection Types and Related Systems},
  KEY = {IT{\relax RS} '02},
  REMARK = {*****FIX THIS ENTRY*****},
  EVENTDATE = {2002-07-26},
  PUBLICATIONDATE = {2003-02},
  YEAR = 2002,
  ELSEVIERURL = {http://www.elsevier.nl/locate/entcs/volume70.html},
  NOTE = {The ITRS '02 proceedings appears as vol.\ 70, issue 1 of \emph{Elec.\ Notes in Theoret.\ Comp.\ Sci.}, 2003-02},
  ISBN = {0-444-51407-4}
}


@PROCEEDINGS{LICS1995,
  TITLE = {Proc.\ 10th Ann.\ {IEEE} Symp.\ Logic in Comput. Sci.},
  BOOKTITLE = {Proc.\ 10th Ann.\ {IEEE} Symp.\ Logic in Comput. Sci.},
  XADDRESS = {San Diego, CA, U.S.A.},
  XMONTH = JUN,
  XMONTH = JUN # {~26--29,},
  KEY = {LI{\relax CS} '95},
  XDAYS = {26--29},
  DATE = {1995-06-26/---29},
  YEAR = 1995,
  XPUBLISHER = {IEEE Comput.\ Soc.\ Press},
  XORGANIZATION = {The IEEE Computer Society's Technical Committee on
               Mathematical Foundations of Computing},
  ISBN = {0-8186-7050-9},
  COMMENT = {IEEE Computer Society Press Order Number PR07050;
                  IEEE Catalog Number 95CH35768; ISBN 0-8186-7050-9;
                  ISSN Number 1043-6871},
  SOURCE = {ftp://theory.lcs.mit.edu/pub/meyer/lics.bib}
}


@PROCEEDINGS{LICS1999,
  TITLE = {Proc.\ 14th Ann.\ {IEEE} Symp.\ Logic in Comput. Sci.},
  YEAR = 1999,
  KEY = {LI{\relax CS} '99},
  BOOKTITLE = {Proc.\ 14th Ann.\ {IEEE} Symp.\ Logic in Comput. Sci.},
  XADDRESS = {Trento, Italy},
  MONTH = JUL,
  XPUBLISHER = {IEEE Comput.\ Soc.\ Press}
}


@PROCEEDINGS{POPL1997,
  TITLE = {Conf.\ Rec.\ POPL '97: 24th {ACM} Symp.\ Princ.\ of\ Prog.\ Langs.},
  BOOKTITLE = {Conf.\ Rec.\ POPL '97: 24th {ACM} Symp.\ Princ.\ of\ Prog.\ Langs.},
  YEAR = 1997,
  XORGANIZATION = {ACM},
  KEY = {PO{\relax PL} '97},
  XADDRESS = {Paris, France},
  XPUBLISHER = {ACM Press},
  XMONTH = {15--17 } # JAN
}


@PROCEEDINGS{POPL1999,
  TITLE = {Conf.\ Rec.\ POPL '99: 26th {ACM} Symp.\ Princ.\ of\ Prog.\ Langs.},
  BOOKTITLE = {Conf.\ Rec.\ POPL '99: 26th {ACM} Symp.\ Princ.\ of\ Prog.\ Langs.},
  YEAR = 1999,
  XORGANIZATION = {ACM},
  KEY = {PO{\relax PL} '99},
  XADDRESS = {San Antonio, Texas, USA},
  XPUBLISHER = {ACM Press},
  XMONTH = JAN,
  DATE = {1999-01-20/---22},
  ISBN = {1-58113-095-3}
}


@PROCEEDINGS{POPL2000,
  TITLE = {Conf.\ Rec.\ POPL '00: 27th {ACM} Symp.\ Princ.\ of\ Prog.\ Langs.},
  BOOKTITLE = {Conf.\ Rec.\ POPL '00: 27th {ACM} Symp.\ Princ.\ of\ Prog.\ Langs.},
  YEAR = 2000,
  XORGANIZATION = {ACM},
  KEY = {PO{\relax PL} '00},
  XADDRESS = {Boston, Massachusetts, USA},
  XPUBLISHER = {ACM Press},
  XMONTH = JAN
}


@PROCEEDINGS{POPL2003,
  TITLE = {Conf.\ Rec.\ POPL '03: 30th {ACM} Symp.\ Princ.\ of\ Prog.\ Langs.},
  BOOKTITLE = {Conf.\ Rec.\ POPL '03: 30th {ACM} Symp.\ Princ.\ of\ Prog.\ Langs.},
  YEAR = 2003,
  XORGANIZATION = {ACM},
  KEY = {PO{\relax PL} '03},
  XADDRESS = {Louisiana, USA},
  XPUBLISHER = {ACM Press},
  XMONTH = JAN
}


@PROCEEDINGS{PPDP2001,
  TITLE = {Proc.\ 3rd Int'l Conf.\ Principles \& Practice Declarative Programming},
  YEAR = 2001,
  KEY = {PP{\relax DP} '01},
  BOOKTITLE = {Proc.\ 3rd Int'l Conf.\ Principles \& Practice Declarative Programming},
  XPUBLISHER = {ACM Press},
  XADDRESS = {Firenze, Italy},
  MONTH = {5--7~} # SEP,
  ISBN = {1-58113-388-X}
}


@PROCEEDINGS{PPDP2002,
  TITLE = {Proc.\ 4rd Int'l Conf.\ Principles \& Practice Declarative Programming},
  YEAR = 2002,
  KEY = {PP{\relax DP} '02},
  BOOKTITLE = {Proc.\ 4rd Int'l Conf.\ Principles \& Practice Declarative Programming},
  PUBLISHER = {ACM Press},
  XADDRESS = {Pittsburgh, PA, US},
  XPUBLISHER = {ACM Press}
}


@PROCEEDINGS{PPDP2004,
  TITLE = {Proc.\ 6th Int'l Conf.\ Principles \& Practice Declarative Programming},
  YEAR = 2004,
  KEY = {PP{\relax DP} '04},
  BOOKTITLE = {Proc.\ 6th Int'l Conf.\ Principles \& Practice Declarative Programming},
  XADDRESS = {Verona, IT},
  XPUBLISHER = {ACM Press},
  ISBN = {1-58113-819-9}
}


@PROCEEDINGS{RTA2003,
  TITLE = {Rewriting Techniques \& Applications, 14th Int'l Conf., RTA 2003},
  BOOKTITLE = {Rewriting Techniques \& Applications, 14th Int'l Conf., RTA 2003},
  KEY = {RTA '03},
  PUBLISHER = {Springer-Verlag},
  VOLUME = 2706,
  SERIES = {LNCS},
  XADDRESS = {Valencia, Spain},
  DATE = {2003-06-09/---11},
  XMONTH = JUN,
  YEAR = 2003,
  ISBN = {3-540-40254-3}
}


@PROCEEDINGS{TCS2004,
  TITLE = {IFIP TC1 3rd Int'l Conf.\ Theoret.\ Comput.\ Sci.\ (TCS '04)},
  BOOKTITLE = {IFIP TC1 3rd Int'l Conf.\ Theoret.\ Comput.\ Sci.\ (TCS '04)},
  KEY = {TCS '04},
  XEDITOR = {Jean-Jacques Levy and Ernst W. Mayr and John C. Mitchell},
  XADDRESS = {Toulouse, France},
  XMONTH = AUG # { 23--26},
  YEAR = {2004},
  ISBN = {1-4020-8140-5},
  PUBLISHER = {Kluwer Academic Publishers}
}


@PROCEEDINGS{TAPSOFT1997,
  TITLE = {Proc.\ 7th Int'l Joint Conf.\ Theory \& Practice
                      of Software Development},
  YEAR = 1997,
  KEY = {TA{\relax PS}OFT '97},
  BOOKTITLE = {Proc.\ 7th Int'l Joint Conf.\ Theory \& Practice
                      of Software Development},
  MAYBEBOOKTITLE = {TAPSOFT' 97, Theory and Practice of Software
                  Development, 7th International Joint Conference CAAP/FASE},
  VOLUME = 1214,
  SERIES = {LNCS},
  XPUBLISHER = {Springer-Verlag},
  XADDRESS = {Lille, France},
  XMONTH = APR,
  XXMONTH = APR # {~14--18,},
  DATE = {1997-04-14/---18},
  TOTALPAGES = 884,
  XXPUBLISHER = {Springer-Verlag Berlin and Heidelberg GmbH & Co. KG},
  ISBN = {3-540-62781-2},
  XNOTE = {TAPSOFT consists of Trees in Algebra in Programming
                  (CAAP) and Formal Approaches in Software Engineering
                  (FASE)}
}


@PROCEEDINGS{TIC1997,
  TITLE = {Proc.\ First Int'l Workshop on Types in Compilation},
  YEAR = 1997,
  KEY = {TIC '97},
  BOOKTITLE = {Proc.\ First Int'l Workshop on Types in Compilation},
  XEDITOR = {R. Muller},
  XPUBLISHER = {Boston College},
  XORGANIZATION = {ACM SIGPLAN},
  XADDRESS = {Amsterdam, The Netherlands},
  MONTH = JUN,
  XMONTH = JUN # {~8,},
  DATE = {1997-06-08},
  XNOTE = {Boston College Computer Science Department Technical
                  Report BCCS-97-03},
  NOTE = {The printed TIC '97 proceedings is Boston Coll.\ Comp.\
                  Sci.\ Dept.\ Tech.\ Rep.\ BCCS-97-03.  The individual
                  papers are available at
                  http://www.cs.bc.edu/{\~{}}muller/TIC97/ or
                  http://oak.bc.edu/{\~{}}muller/TIC97/}
}


@PROCEEDINGS{TIC2000,
  TITLE = {Preliminary Proceedings of the Third Workshop on Types in Compilation (TIC 2000)},
  YEAR = 2000,
  KEY = {TIC '00},
  BOOKTITLE = {Preliminary Proceedings of the Third Workshop on Types in Compilation (TIC 2000)},
  XADDRESS = {Montr{\'e}al, Canada},
  XMONTH = {21~} # SEP,
  DATE = {2000-09-21},
  NOTE = {Carnegie Mellon Univ.\ tech.\ report CMU-CS-00-161}
}


@PROCEEDINGS{TIC2000LNCS,
  TITLE = {Types in Compilation, Third Int'l Workshop, TIC 2000},
  YEAR = 2001,
  KEY = {TIC '00},
  BOOKTITLE = {Types in Compilation, Third Int'l Workshop, TIC 2000},
  SERIES = {LNCS},
  VOLUME = 2071,
  PUBLISHER = {Springer-Verlag},
  XEDITOR = {R. Harper},
  ISBN = {3-540-42196-3},
  COMMENT = {My best guess as to the actual publication date is
                  2001-06-13, because that appears as the "online
                  publication" date on an associated web page.}
}

@COMMENT{{PeterM\ollerNeergaard:thesettingofpmn-ask-for-x-symbolisaddedformysaketoavoidmessingupthebibliographywheneditinginemacs.Thesettingofindent-tabs-modeisforeverybodytohelpavoidunnecessarychangesthatcauseCVSconfusion.LocalVariables:pmn-ask-for-x-symbol:0indent-tabs-mode:nilEnd:}}


This file has been generated by bibtex2html 1.61
 

This page is maintained by Peter Møller Neergaard. Autogenerated on Saturday July 26 2008.