[Semantics
at NU
| College of Computer Science
| Northeastern University]
NU Programming Languages Seminar Wednesday, 31 May 2000, 10:00 - noon 149 Cullinane Hall, Northeastern University (building 9 on the map at http://www.neu.edu/maps/maps.html)
Norman Ramsey (Harvard University) will present
C--: A Single Intermediate Language That Supports Multiple Implementations of Exceptions
(joint work with Simon Peyton Jones, Microsoft Research)
Abstract:
Many compilers have been written that translate high-level languages to C. This technique eases portability, but C makes it difficult to provide efficient implementations of some features of modern languages, e.g., proper tail calls, accurate garbage collection, and efficient exception dispatch. C-- is a language designed expressly to act as a compiler-target language, and to approach the ease of generating C while approaching the performance of custom code generators.
This talk focuses on mechanisms that enable C-- to express the four best known techniques for implementing exceptions, all within a single, uniform framework. These mechanisms include annotations on call sites, variations on procedure returns, and weak continuations that do not outlive their contexts of origin. Our approach clarifies the design space of exception-handling techniques, and it allows a single optimizer to handle a variety of implementation techniques. Our ultimate goal is to allow a source-language compiler the freedom to choose its exception-handling policy, while encapsulating the architecture-dependent mechanisms and their optimization in an implementation of C-- that can be used by compilers for many source languages.
NU Programming Languages Seminar Wednesday, 17 May 2000, 10:00 - noon 149 Cullinane Hall, Northeastern University (building 9 on the map at http://www.neu.edu/maps/maps.html)
Paul C. Attie will present his work on A Formal Model for Dynamic Computation
Abstract:
We present a formal model for defining and reasoning about agent systems. An agent is an autonomous software entity, which cooperates with other agents in carrying out delegated tasks. Agent systems are ``dynamic'' in two senses: (1) agents are created and destroyed as computation proceeds, and (2) agents change ``location.'' Our model provides for both kinds of dynamism. We provide explicit ``create'' and ``destroy'' operations, and we model mobility by allowing an agent to dynamically change its external interface. We give a precise semantics for create and destroy operations, and also for the concurrent composition of two (or more) agent systems. Our model also provides a precise notion of projection onto a subsystem, which is usually lacking in models based on process algebraic approaches such as the pi-calculus.
We present a notion of simulation relation from one agent system to another, which can be used to verify that one agent system correctly refines another. We present an example specification and implementation of a simple agent system, along with the simulation relation which shows that the implementation correctly refines the specification.
NU Programming Languages Seminar Wednesday, 15 March 2000, 10:00 - noon 149 Cullinane Hall, Northeastern University (building 9 on the map at http://www.neu.edu/maps/maps.html)
Torben Amtoft will report on Behaviour Analysis for Validating Communication Patterns [This is joint work with Flemming Nielson and Hanne Riis Nielson, reported in {Software Tools for Technology Transfer 2(1):13--28, 1998}]
The communication patterns of concurrent programs can be expressed succinctly using behaviours; these can be viewed as a kind of causal constraints or as a kind of process algebra terms. We present a system that infers behaviours from a useful fragment of Concurrent ML programs; it is based on previously developed theoretical results on annotated type and effect systems and forms the core of a prototype available on the Internet (http://www.daimi.au.dk/~bra8130/TBAcml/TBA_CML.html). By means of a case study, used as a benchmark in the literature, we shall see that the prototype facilitates the validation of certain safety conditions for reactive programs, and even pinpoints a subtle bug in a formally developed program.
NU Programming Languages Seminar Wednesday, 1 March 2000, 10:00 - noon To be continued 8 March, 10:00 - noon 149 Cullinane Hall, Northeastern University (building 9 on the map at http://www.neu.edu/maps/maps.html)
Mitch Wand will explain Howe's Method.
Abstract:
In operational semantics, the most obvious notion of equivalence between programs is "gives the same answer". Unfortunately, this notion only makes sense for whole programs, when what one really wants is a notion of equivalence between expressions: "you can substitute one for the other in any program and never tell the difference". This notion is called "contextual equivalence". It is often the case that for a sufficiently clever notion of "same", "gives the same answer" is the same as contextual equivalence. But proving this is hard, and often involves hairy domain theory. In 1989, Doug Howe introduced a purely syntactic method for showing results like this. Howe's method is extremely flexible, so it can be modified for a variety of contexts. We will present Howe's method and show how it can be used in a simple interesting context: the lazy lambda calculus. With luck, we will finish in four hours what Abramsky spent his entire thesis doing.
NU Programming Languages Seminar Wednesday, 23 February 2000, 10:00 - noon 149 Cullinane Hall, Northeastern University (building 9 on the map at http://www.neu.edu/maps/maps.html)
Will Clinger will finish his presentation of the Xi and Harper paper described below by covering the treatment of sum types, giving a sketch of the proof of soundness, and providing as many examples as time permits.
A Dependently Typed Assembly Language Hongwei Xi and Robert Harper
Abstract: We present a dependently typed assembly language (DTAL) in which the type system supports the use of a restricted form of dependent types, reaping some benefits of dependent types at assembly level. DTAL overcomes several significant limitations in recently proposed low-level languages including Java bytecode language and a typed assembly language, which prevent them from handling certain important compiler optimizations such as run-time array bound check elimination. We also mention a compiler which generates code in DTAL from compiling some high-level programs.
NU Programming Languages Seminar Wednesday, 16 February 2000, 10:00 - noon 149 Cullinane Hall, Northeastern University (building 9 on the map at http://www.neu.edu/maps/maps.html)
Please note that, due to a scheduling conflict, we will meet on Wednesdays throughout the rest of this month and March.
Will Clinger will present
A Dependently Typed Assembly Language Hongwei Xi and Robert Harper
Abstract: We present a dependently typed assembly language (DTAL) in which the type system supports the use of a restricted form of dependent types, reaping some benefits of dependent types at assembly level. DTAL overcomes several significant limitations in recently proposed low-level languages including Java bytecode language and a typed assembly language, which prevent them from handling certain important compiler optimizations such as run-time array bound check elimination. We also mention a compiler which generates code in DTAL from compiling some high-level programs.
NU Programming Languages Seminar Tuesday, 8 February 2000 10:00 - noon at 149 Cullinane Hall, Northeastern University
Igor Siveroni will present
Data Flow Analysis is Model Checking of Abstract Interpretations David A. Schmidt
Abstract: This expository paper simplifies and clarifies Steffen's depiction of data flow analysis (d.f.a.) as model checking: By employing abstract interpretation (a.i.) to generate program traces and by utilyzing Kozen's modal mu-calculus to express trace properties, we express in simplest possible terms that a d.f.a. is a model check of a program's a.i. trace. In particular, the classic flow equations for bit-vector-based d.f.a.s reformat trivially into modal mu-calculus formulas. A surprising consequence is that two of the classical d.f.a.s are exposed as unsound; this problem is analyzed and simply repaired. In the process of making the above discoveries, we clarify the relationship between a.i. and d.f.a. in terms of the often-misunderstood notion of collecting semantics and we highlight how the research areas of flow analysis, abstract interpretation, and model checking have grown together.
The Northeastern University Programming Languages Seminar will feature four guest presentations on Monday, 24 January, followed by a fifth presentation on Tuesday the 25th. All of these presentations will be given in room 149 of Cullinane Hall at Northeastern ( Cullinane Hall is building 9 on the map that is available online at http://www.neu.edu/maps/maps.html ).
Full abstracts appear below the schedule of talks.
Monday, 24 January, 9:00 - 10:30 am: Ran Rinat, Tel-Aviv University, will present his "Flexible Subclassing in Statically-Typed Object-Oriented Languages"
Monday, 24 January, 10:30 - 12:00: Nick Benton and Andrew Kennedy, Microsoft Research, Cambridge, UK, will present their talk titled "A Note on Exceptional Syntax"
Monday, 24 January, 1:00 - 2:30 pm: Zhe Yang, New York University, will present his ESOP '99 paper co-authored by Olivier Danvy: "An Operational Investigation of the CPS Hierarchy"
Monday, 24 January, 2:30 - 4:00 pm: Bernd Brobauer, BRICS, University of Aarhus, with present his PEPM '00 paper co-authored by Zhe Yang: "The Second Futamura Projection for Type-directed Partial Evaluation"
Tuesday, 25 January, 9:00 - 10:30 am: Greg Sullivan, MIT AI Lab, will present his "Operationally-based Models of Higher-order Imperative Programming Languages"
ABSTRACTS:
Flexible Subclassing in Statically-Typed Object-Oriented Languages Ran Rinat, Tel-Aviv University
In the leading commercial statically-typed OO languages (namely Java and C++) one cannot override the type of a field or the signature of a method in a subclass. This is unfortunate because the need for such change often arises in practice. For example, if we have a "person" class with a field "physician" of type "Doctor", then in a subclass "child", we might want to specialize that field to "Pediatrician".
Supporting this feature in a type-safe language along with "subclass polymorphism" (that is, an instance of a subclass is acceptable where the type of objects created by the class itself is required) turns out to be a difficult problem. The language Eiffel, for example, supports this, but it causes typechecking problems there. Much research has been conducted on this issue during the last decade. After presenting the problem in more detail, the talk will mention some of the approaches proposed to deal with it (multi-methods, matching, precise typing, virtual types), and then concentrate on matching and its recent generalization to the full covariance problem (generalized matching).
Only knowledge of the basic concepts of OOP will be assumed.
A Note on Exceptional Syntax Nick Benton and Andrew Kennedy, Microsoft Research, Cambridge UK
From the points of view of proof-theory, programming pragmatics and operational semantics, the syntactic construct used for exception handling in many programming languages, and in much theoretical work on exceptions, has subtly undesirable features. We propose and discuss a more well-behaved construct.
An operational investigation of the CPS hierarchy Olivier Danvy and Zhe Yang, ESOP'99 To be presented by: Zhe Yang, New York University
We explore the hierarchy of control induced by successive transformations into continuation-passing style (CPS) in the presence of ``control delimiters'' and ``composable continuations''. Specifically, we investigate the structural operational semantics associated with the CPS hierarchy.
To this end, we characterize an operational notion of continuation semantics. We relate it to the traditional CPS transformation and we use it to account for the control operator ${\bf shift}$ and the control delimiter ${\bf reset}$ operationally. We then transcribe the resulting continuation semantics in ML, thus obtaining a native and modular implementation of the entire hierarchy. We illustrate it with several examples, the most significant of which is layered monads.
The second Futamura projection for type-directed partial evaluation Bernd Grobauer and Zhe Yang, PEPM'00 To be presented by: Bernd Grobauer, BRICS, University of Aarhus
The second Futamura projection describes the automatic generation of non-trivial generating extensions by applying a partial evaluator to itself. We derive an ML implementation of the second Futamura projection for Type-Directed Partial Evaluation (TDPE). Due to the differences between `traditional', syntax-directed partial evaluation and TDPE, this derivation involves several conceptual and technical steps. These include a suitable formulation of the second Futamura projection and techniques for using TDPE to specialize type-indexed programs. In the context of the second Futamura projection, we also compare and relate TDPE with conventional offline partial evaluation.
We demonstrate our technique with several examples, including compiler generation for Tiny, a prototypical imperative language.
Operationally-Based Models of Higher-Order Imperative Programming Languages Greg Sullivan, MIT AI Lab
We present a typed metalanguage with support for higher-order functions, a global store, and input-output. An operational, small-step semantics is given for the metalanguage, with the operations on the global store and for I/O restricted to continuation passing style. We develop, based solely on the operational semantics, a theory of term equivalence in the metalanguage, notably an Extensionality Theorem (also known as a context lemma). By considering equivalence classes of operationally equivalent metalanguage terms, we construct a term model which we then use as the target for denotational semantics of imperative programming languages. As an in-depth application of our methods, we prove correct a number of source-to-source transformations used in a compiler for Scheme.
Tuesday, 7 December 1999 10:00 - noon, room 149 Cullinane Hall
Greg Sullivan will complete his presentation of the HOOTS99 preliminary version of "Monads, Effects, and Transformations", by Nick Benton and Andrew Kennedy of Microsoft Research Ltd (UK).
Afterwards, we will ask those who attended OOPSLA '99 to tell us about the high points of that conference.
Abstract for "Monads, Effects, and Transformations":
We define a typed compiler intermediate language, MIL-lite, which incorporates computational types refined with effect information. We characterise MIL-lite observational congruence by using Howe's method to prove a ciu theorem for the language in terms of a termination predicate defined directly on the term. We then define a logical predicate which captures an observable version of the intended meaning of each of our effect annotations. Having proved the fundamental theorem for this predicate, we use it with the ciu theorem to validate a number of effect-based transformations performed by the MLj compiler for Standard ML.
Tuesday, 30 November 1999 10:00 - noon, room 149 Cullinane Hall
Greg Sullivan will present the HOOTS99 preliminary version of "Monads, Effects, and Transformations", by Nick Benton and Andrew Kennedy of Microsoft Research Ltd (UK). The final version of this paper will be published in Electronic Notes in Theoretical Computer Science.
Abstract:
We define a typed compiler intermediate language, MIL-lite, which incorporates computational types refined with effect information. We characterise MIL-lite observational congruence by using Howe's method to prove a ciu theorem for the language in terms of a termination predicate defined directly on the term. We then define a logical predicate which captures an observable version of the intended meaning of each of our effect annotations. Having proved the fundamental theorem for this predicate, we use it with the ciu theorem to validate a number of effect-based transformations performed by the MLj compiler for Standard ML.
Wednesday, 17 November 1999 10:00 - noon, room 149 Cullinane Hall
This week our programming language seminar will feature Igor Siveroni presenting his PhD thesis proposal on "Correctness of Analysis-based Program Transformations of Functional Languages". Siveroni's advisor is Mitch Wand.
Abstract:
Realistic compilers for imperative or functional languages include a variety of optimisations based on program analyses. The presence and identification of certain invariants in the behaviour of a program provides the opportunity to generate ``better'' code without affecting the meaning of the initial program. Program transformations exploit this fact. The job of the compiler is to safely detect these invariants (semantic properties) and to systematically use this information in the generation of improved code.
Proving the correctness of analysis-based program transformations can be done by first proving that the program analysis is sound (the information computed by the analysis satisfies some useful semantic property) and by proving that the transformation, given sound information, preserves the meaning of the initial program. We find in the literature that most correctness proofs are based solely on analysis specifications. This approach has the disadvantage that it ties the transformation to the analysis and neglects the importance of semantic properties as the main justification for program transformations.
The goal of this research is to show that we can prove the correctness of program transformations based only on semantic properties, regardless of the type of analysis used. In order to do this, we will provide a framework that allows us to give clear and useful definitions of these properties. The proposed research will concentrate on the possibilities of that framework by working on different types of program transformations and by providing program analysis specifications derived from the initial definitions.
Wednesday, 10 November 1999 10:00 - noon, room 149 Cullinane Hall
After a week off for OOPSLA, we will continue with our grand opening, this time on a Wednesday. If you are unable to come to this meeting, but would like to express your preference for Tuesday or Wednesday meetings of the programming languages seminar (from ten o'clock until noon), please send email to will@ccs.neu.edu.
OPENING MEETING. Mitch Wand, Will Clinger, David Lorenz, and whoever else would like to speak will start off with short presentations on open problems of current interest.
And of course we will continue to recruit volunteers to present papers in future meetings.