Mitchell Wand
[Semantics
at NU
| College of Computer Science
| Northeastern University]
Mon 7/6/98
Erik Meijer, Utrecht University, will present:
Haskell as an ActiveX Scripting Engine
ABSTRACT:
Microsoft's ActiveX Scripting Architecture is a set of standard COM interfaces that defines a language independent protocol for connecting a scripting engine to a host application. Microsoft provides standard scripting engine implementations for JScript and VBScript to script standard scripting hosts such as Internet Explorer and the Windows Scripting Host.
Based on Yale-Nottingham Hugs, we have implemented HaskellScript, a scripting engine for the purely functional language Haskell. In this talk we discuss HaskellScript, including implementation features and design decisions, and we will give numerous examples of how to use HaskellScript for client-side web scripting and automating application such as Word, Excel, and Visio. In particular we will compare the implementation of the "Nervous Text" applet written in HaskellScript to ones written in Java and JavaScript, and show how Haskell-specific features such as monads and list-comprehension make it possible to come up with a concise solution.
Wed, 7/1/98
Greg Sullivan will present
"Typechecking and Modules for Multimethods", by Craig Chambers and Gary T. Leavens, (TOPLAS, Nov. 1995)
Abstract: Two major obstacles hindering the wider acceptance of multi-methods are concerns over the lack of encapsulation and modularity and the absence of static typechecking in existing multi-method-based languages. This paper addresses both of these problems. We present a polynomial-time static typechecking algorithm that checks the conformance, completeness, and consistency of a group of method implementations with respect to declared message signatures. This algorithm improves on previous algorithms by handling separate type and inheritance hierarchies, abstract classes, and graph-based method lookup semantics. We also present a module system that enables independently-developed code to be fully encapsulated and statically typechecked on a per-module basis. To guarantee that potential conflicts between independently-developed modules have been resolved, a simple well-formedness condition on the modules comprising a program is checked at link-time. The typechecking algorithm and module system are applicable to a range of multi-method-based languages, but the paper uses the Cecil language as a concrete example of how they can be applied.
Wed, 5/27/98
Allyn Dimock will continue "Single and Loving It" (with recapitulation for those who weren't there on 5/13).
Abstract of Abstract:
In standard control-flow analyses for higher-order languages, a single abstract binding for a variable represents a set of exact bindings, and a single abstract reference cell represents a set of exact reference cells. While such analyses provide useful may-alias information, they are unable to anser must-alias questions about variables and cells, as these questions ask about equality of specific bindings and references.
In this paper, we present a novel program analysis for higher-order languages that answers must-alias questions.
Must-alias information facilitates various program optimizations such as lightweight closure conversion. In addition, must-alias information permits analyses to perform strong updates on abstract reference cells known to be single.
Wed, 5/20/98
Will Clinger will present his paper "Proper tail recursion and space efficiency." (PLDI 98)
Abstract:
The IEEE/ANSI standard for Scheme requires implementations to be properly tail recursive. This ensures that portable code can rely upon the space efficiency of continuation-passing style and other idioms. On its face, proper tail recursion concerns the efficiency of procedure calls that occur within a tail context. When exmined closely, proper tail recursion also depends upon the fact that garbage collection can be asymptotically more space-efficient than Algol-like stack allocation.
This paper offers a formal and implementation-independent defintion of proper tail recursion for Scheme. It also shows how an entire family of reference implementations can be used to characterize safe-for-space properties, and proves the asymptotic inequalities that hold between them.
The paper is available.
Wed, 5/13/98
SPECIAL DOUBLE-HEADER:
Will Clinger will present: "Set Constraints for Destructive Array Update Optimization" by Wand and Clinger. This is a preview of his ICCL98 presentation.
Allyn Dimock will present "Single and Loving It: Must-Alias Analysis for Higher-Order Languages" by Jagannathan, Thiemann, Weeks, and Wright. (POPL98)
Abstract of Abstract:
In standard control-flow analyses for higher-order languages, a single abstract binding for a variable represents a set of exact bindings, and a single abstract reference cell represents a set of exact reference cells. While such analyses provide useful may-alias information, they are unable to anser must-alias questions about variables and cells, as these questions ask about equality of specific bindings and references.
In this paper, we present a novel program analysis for higher-order languages that answers must-alias questions.
Must-alias information facilitates various program optimizations such as lightweight closure conversion. In addition, must-alias information permits analyses to perform strong updates on abstract reference cells known to be single.
We will meet in 107 CN from 10 to 12, as usual.
Wed, 4/29/98
Will Clinger will talk about numerical benchmarks, mostly for functional and higher order programming languages, using material from five sources:
Jeffrey Mark Siskind's EM benchmarks, recently posted to comp.lang.ml, comp.lang.functional, comp.lang.scheme, and comp.lang.lisp.
Hartel, Feeley, et al. Benchmarking implementations of functional languages with "Pseudoknot", a float-intensive benchmark. Journal of Functional Programming 6(4), pages 621-655, 1996.
Hammes, Sur, and B\:ohm. On the effectiveness of functional language features: NAS benchmark FT. Journal of Functional Programming 7(1), pages 113-124, 1997.
Andrew Appel. Intensional equality ;-) for continuations. ACM SIGPLAN Notices 31(2), pages 55-57, February 1996.
William Kahan. The baleful effect of computer languages and benchmarks upon applied mathematics, physics and chemistry. The John von Neumann Lecture at the 45th annual meeting of SIAM, Stanford, 15 July 1997.
Wed, 4/22/98
Patrik Jansson, Chalmers Institute (Sweden)
Polytypic Programming
Many functions have to be written over and over again for different datatypes, either because datatypes change during the development of programs, or because functions with similar functionality are needed on different datatypes. Examples of such functions are pretty printers, pattern matchers, equality functions, unifiers, rewriting functions, etc. Such functions are called polytypic functions. A polytypic function is a function that is defined by induction on the structure of user-defined datatypes. This talk introduces polytypic functions, shows how to construct and reason about polytypic functions and says a few words about the implementation of the polytypic programming system PolyP.
PolyP extends a functional language (a subset of Haskell) with a construct for writing polytypic functions. The extended language type checks definitions of polytypic functions, and infers the types of all other expressions. Programs in the extended language are translated to Haskell.
Wed, 4/1/98
John Kalamatianos (ECE) Temporal-based Procedure Reordering for Improved Instruction Cache Performance
As the gap between memory and processor performance continues to grow, it becomes increasingly important to exploit cache memory effectively. Both hardware and software techniques can be used to better utilize the cache. Hardware solutions focus on organization, while most software solutions investigate how to best layout a program on the available memory space.
In this talk we present a new link-time code reordering algorithm targeted at reducing the frequency of misses in the cache. Past work has focused on eliminated first generation cache conflicts (i.e., conflicts between a procedure, and any of its immediate callers or callees) based on calling frequencies. In this work we exploit procedure-level temporal interaction, using a structure called a Conflict Miss Graph (CMG). In the CMG every edge weight is an approximation of the worst-case number of misses two competing procedures can inflict upon one another. We use the ordering implied by the edge weights to apply color-based mapping and eliminate conflict misses between procedures lying either in the same or in different call chains.
Using programs taken from SPEC 95, Gnu applications, and C++ applications, we have been able to improve upon previous algorithms, reducing the number of instruction cache conflicts by 20% on average compared to the best procedure reordering algorithm.
Wed, 3/4/98
Mitch Wand will present "A Formal Basis for Architectural Connection" by Allen and Garlan (TOESEM, 7/97)
Condensed Abstract:
We present a formal approach to one aspect of archtiectural design: the interactions among components. The key idea is to define architectural connectors as explicit semantic entities. These are specified as a collection of protocols that characterize each of the participant roles in an interaction and how these roles interact. We provide a formal semantics and show how this leads to a system in which architectural compatibility can be checked in a way analogous to type-checking in programming languages.
Wed, 2/25/98
Allyn Dimock will present Mossin's "Exact Flow Analysis" (SAS '97)
Abstract:
We present a flow analysis based on annotated types. The analysis is exact in the following sense: if the analysis predicts a redex, then there exist a reduction sequence (using standard reduction plus context propagation rules) such that this redex will be reduced. The precision is accomplished using intersection typing.
It follows that the analysis is non-elementary recursive - more surprisingly, the analysis is decidable. We argue that the specification of such an analysis provides a good starting point for developing new flow analyses and an important benchmark against which other flow analyses can be compared. Furthermore, we believe that the methods employed for stating and proving exactness are of independent interest: they provide methods for reasoning about the precision of program analyses.
Wed, 2/18/98
John Ramsdell will present "The Tail-Recursive SECD Machine"
Abstract
A tail recursive implementation of a programming language allows the execution of an iterative computation in constant space, even if the iterative computation is described by a syntactically recursive procedure. With a tail recursive implementation, iteration can be expressed using the ordinary procedure call mechanics, so that special iteration constructs are useful only as abbreviations.
The standard which specifies some programming languages requires implementations that are tail recursive. With these languages, a new style of programming is available which relies on the fact that implementations have this property. Given the importance of tail recursion in these languages, it is distressing that every standard simply requires tail recursive implementations without defining the requirement.
In this talk, I will present two versions of an abstract machine for Landin's functional programming language ISWIM. One of the two machines is tail recursive and a comparison between the two will show the essence of tail recursion.
An automated correctness proof of both abstract machines has been performed using the Boyer-Moore Theorem Prover. The correctness proof for the tail recursive abstract machine suggests how to define part of the tail recursion requirement for real programming languages. A soon to be released revision of the Scheme Programming Language standard will contain text defining its tail recursion requirement, which was motivated by this work. The talk will conclude with a description of the requirement and how it was motivated by the correctness proof.
Paper: The Tail Recursive SECD Machine
URL: http://www.ccs.neu.edu/home/ramsdell/papers/trsecd.ps.gz
Wed, 2/11/98
Ali Ozmez will present "Linear Subtransitive Control-Flow Analysis" by Heintze & MacAllister (PLDI '97).
Wed, 2/4/98
Lars Hansen will present "The Measured Cost of Copying Garbage Collection Mechanisms," by Michael W. Hicks, Jonathan T. Moore, and Scott M. Nettles (ICFP 1997, p 292-305)
We examine the costs and benefits of a variety of copying garbage collection mechanisms across multiple architectures and programming languages. Our study covers both low-level object representation and copying issues as well as the mechanisms needed to support more advanced techniques such as generational collection, large object spaces, and type-segregated areas.
In general, we found that careful implementation of GC mechanisms can have a significant benefit. For a simple collector, we measured improvements of as much as 95%. We then found that while the addition of advanced features can have a sizeable overhead (up to 15%), the net benefit is quite positive, resulting in additional gains of up to 42%. We also found that results varied depending upon the platform and language. Machine characteristics such as cache arrangements, instruction set (RISC/CISC), and register pool were important. For different languages, average object size seemed to be most important.
[I will include a short overview of the basics of copying GC in the talk, so attendees should not worry about not being up on their GC algorithms.]
Wed, 1/7/98
Ali Ozmez will present:
Linear-time Subtransitive Control-Flow Analysis by Heintze and McAllester (PLDI '97)
Abstract:
We present a linear-time algorithm for bounded-type programs that builds a directed graph whose transitive closure gives exactly the results of the standard (cubic-time) Control-Flow Analysis algorithm. Our algorithm can be used to list all function calls from all call sites in (optimal) quadratic time. More importantly, it can be used to give linear-time algorithms for CFA-consuming applications such as: effects analysis, k-limited CFA, and called-once analysis.
Wed 12/3
Johan Ovlinger will present "Three Approaches to Type Parameterization in Java"
This will summarize three papers on this subject: Pizza (by Odersky and Wadler), the Myers-Bank-Liskov proposal (both in POPL 97) and the Ageson-Freund-Mitchell proposal (OOPSLA 97).
Wed 11/19
Mira Mezini will present "Variation-Oriented Programming: Beyond Classes and Inheritance"
Abstract:
In my work I argue that the basic mechanisms of object-oriented languages, classes and inheritance, while perfectly enabling software to be organized in a way that allows incremental modeling of new kinds of abstractions, do not suffice when other kinds of behavior variations are needed. Variations that depend on factors, such as the internal state of objects, perspectives or aspects, application requirements, or characteristics of the environment, are not as properly modeled with classes and inheritance alone. For this reason, a new language model called Rondo is proposed. It enriches the design space of object-oriented languages with more powerful mechanisms that enable Rondo software to be more robust in terms of extensibility and reusability.
We will meet in 107 CN from 1000 til 1200, as usual.
Wed 11/12
Harry Mairson will present his paper: "Parallel beta reduction is not elementary recursive" (POPL '98, joint work with Andrea Asperti).
Condensed abstract:
We analyze the inherent complexity of implementing Levy's notion of optimal evaluation for the lambda-calculus, where similar redexes are contracted in one step via ``parallel beta-reduction.'' We prove that the cost of parallel beta-reduction is not bounded by any Kalmar-elementary recursive function. Not merely do we establish that the parallel beta-step cannot be a unit-cost operation, we demonstrate that the time complexity of implementing a sequence of $n$ parallel beta-steps is not bounded as $O(2^n)$, $O(2^{2^n})$, $O(2^{2^{2^n}})$, or in general, $O(K_p(n))$ where $K_p(n)$ is a fixed stack of $p$ 2s with an $n$ on top.
The POPL98 version can be retrieved at the URL: http://www.cs.brandeis.edu/~mairson/Papers/am97-abs.ps.gz
We will meet in 107 CN from 1000 til 1200, as usual.
Wed 10/29/97
Arthur Nunes will continue his presentation on "Compilation and Equivalence of Imperative Objects", by Andy Gordon, Paul Hankin, and S. Lassen. We had only a brief introduction on 10/22, so newcomers can probably catch up.
Condensed abstract:
We adopt the untyped imperative object calculus of Abadi and Cardelli as a minimal setting which to study problems of compilation and program equivalence that arise when compiling object-oriented languages... Our first result is a direct proof of the correctness of compilation to a stack--based abstract machine via a small-step decompilation algorithm. Our second result is that contextual requivalence of objects coincides with a form of Mason and Talcott's CIU equivalence; the latter provises a tractable means of establishing operational equivalences. Finally, we prove correct an algorithm, used in our prototype compiler, for statically resolving method offsets. This is the first study of correctness of an object-oriented abstract machine, and of operational equivalence for the imperative object calculus.
For NU users, the paper is available at /home/wand/people/gordon/imperative-objects.ps .
Wed 10/8/97
Allyn Dimock will present "From Polyvariant Flow Information to Intersection and Union Types" by Jens Palsberg and Christina Pavlopoulu (POPL 98)
Condensed Abstract:
Many polyvariant program analyses have been studied in the 1990s... The idea of polyvariance is to analyze functions more than once and thereby obtain better precision for each call site. In this paper we present the first formal relationship between polyvariant analysis and standard notions of type. We present a parameterized flow analysis and prove that if a program can be safety-checked by a finitary instantiation of the flow analysis, then it can also be typed in a type system with intersection types, union types, subtyping, and recursive types, but no polymorphism.
Wed 10/1/97
*** OPENING MEETING ***
We will have short presentations on open problems and projects from me, Will, and maybe others.
We'll deal with scheduling problems, etc; hopefully we can continue with our traditional Wednesday morning meeting time.
And of course we'll get some folks signed up to give talks. I've got a whole new stratum on the top of the Book of Sand, in case anyone is looking for things to present.