Lexically-scoped higher-order programming languages require closures for
procedures. Typical implementations create a closure for every procedure and a
variable slot for every free variable. This entails substantial overhead. In
this talk, I will present a novel compile-time analysis and code-generation
strategy that significantly reduces the number of procedures that need
closures and the number of variables that need slots, resulting in faster code.
Hancock is a language for processing large volumes of data. Within AT&T, Hancock generated code is in use for various marketing and fraud applications that involve analyzing the daily call records from AT&T's network. Soon, it will be used for other kinds of data...
The changes that allowed Hancock to evolve from an application-specific language into a domain-specific language are the subject of this talk. I will begin with a brief description of the applications we are targeting, and the motivation for Hancock. The bulk of the talk will cover the abstractions that Hancock provides programmers, and how these have been generalized to new kinds of data.
Joint work with Kathleen Fisher, Anne Rogers, and Dan Bonachea.
Since XML became popular, several XML processing lanuages have been proposed. However, because most of them are untyped, it is not as easy as it might be to write correct programs. We present here a preliminary design for a statically typed programming language XDuce for XML processing. Our language features regular expression types. Regular expression types are similar in spirit to DTDs; however, our type system additionally supports a powerful notion of type compatibility (a.k.a. type equivalence and subtyping). In this talk, we present how we can use regular expression types with type compatibility for writing programs to manipulate XML data in a substantially flexible way. Nevertheless, our type system detects many silly mistakes statically. Despite the powerfulness of type compatibility, we can define it in a very simple and intuitive way. We have implemented a prototype typechecker and interpreter for XDuce. Our experience writing several small applications supports our claim on the flexibility and robustness. Also, despite the high computational complexity of the subtyping problem, our experience using the implementation indicates that we can decide it quickly in typical cases.
In this talk, I will describe links, a low-level calculus designed to serve as an intermediate representation in compilers for class-based object-oriented languages. The calculus fills two roles. First, its primitives can express a wide range of class-based object-oriented language features, such as class construction and various forms of method dispatch. Second, it allows the compiler to specify class linking directly in links. The calculus can model the class systems of Moby, OCaml, and Loom, where subclasses may be derived from unknown base classes, or just-in-time linking schemes like that of Java, where an application loads and links classes dynamically.
This work is in collaboration with John Reppy and Jon Riecke.
We present a technique to implement type-safe garbage collectors by combining existing type systems used for compiling type-safe languages. We adapt the type systems used in region inference and intensional type analysis to construct a safe stop-and-copy garbage collector for higher-order polymorphic languages. Rather than using region inference as the primary method of storage management, we show how it can be used to implement a garbage collector which is provably safe. We also introduce a new region calculus with non-nested object life-times which is significantly simpler than previous calculi. Our approach also formalizes more of the interface between garbage collectors and code generators. The efficiency of our safe collectors are algorithmically competitive with unsafe collectors.
TinkerType is a framework for compact and modular description of formal systems (type systems, operational semantics, logics, etc.). A family of related systems is broken down into a set of clauses --- individual inference rules --- and a set of features controlling the inclusion of clauses in particular systems. Dependency relations on both clauses and features and a simple form of ``judgement signatures'' are used to check the consistency of the generated systems.
As an application, we present a substantial repository of typed lambda-calculi, including systems with subtyping, polymorphism, type operators and kinding, computational effects, and dependent and recursive types. The repository describes both declarative and algorithmic aspects of the systems, and can be used with our tool, the TinkerType Assembler, to generate calculi either in the form of typeset collections of inference rules or as executable ML typecheckers.