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 Poll
