Mitchell Wand
[Semantics
at NU
| College of Computer Science
| Northeastern University]
NU Programming Languages Seminar Wednesday, June 19, 2002 306 Egan Hall, Northeastern University (building 44 on http://www.campusmap.neu.edu/) 9:30-11:30
Manuel Serrano INRIA
Scheme Fair Threads
FairThreads offers a very simple framework for concurrent and parallel programming. Basically, it defines schedulers which are synchronization servers. All threads are executed in a cooperative way, at the same pace, and they can synchronize and communicate using broadcast events. FairThreads has a precise and clear semantics and are actually deterministic.
During the talk, we will compare cooperative threads and preemptive threads in the context of the Scheme programming language. We will then present FairThreads semantics (including the semantics of the scheduler). Then, we will present the actual FairThreads API and implementation in Bee, a programming environment for Scheme. Finally, we will conclude with some graphical demonstrations deploying FairThreads.
URL: http://www.inria.fr/mimosa/fp/Bigloo
NU Programming Languages Seminar Wednesday, June 12, 2002 306 Egan Hall, Northeastern University (building 44 on http://www.campusmap.neu.edu/) 9:30-11:30
Mark Logan Northeastern University
Anomaly: A special purpose language for System and Network Management.
One of the central problems of system administration is coping with heterogeneity. Even in medium sized local area networks, the number of unique configurations can grow too large to manage manually. A number of techniques for managing heterogeneity have emerged over the years, including: The aggregation of recurring configuration data via OOP techniques, the use of RDBMS back-ends for storing configuration data, and the use of basic logic programming techniques in configuration scripts.
Anomaly is a declarative data specification language that combines elements of these three techniques. Our key insight is that administrators often configure hosts, switches, and other objects in a LAN using contextual data, that is, data that originates in the physical or logical environment of the item. Anomaly uses environmental acquisition to allow administrators to model these contextual relationships explicitly. This technique can be used to exploit structure implicit in the design of the network, and reduce the complexity of the network configurations.
Our talk will cover the motivation for Anomaly, its design, and how its semantics simplify system and network administration.
NU Programming Languages Seminar Wednesday, May 22, 2002 206 Egan Hall, Northeastern University (building 44 on http://www.campusmap.neu.edu/) [!** note non-standard room **!] 9:30-11:30
Timothy Hickey, Brandeis University
Jscheme: A Scheme-like language for the JVM
Jscheme is a Scheme-like dialect of Lisp which provides transparent access to Java via a simple and powerful syntactic extension - the Java-dot notation. Jscheme borrows much of its semantics from Java; in particular it directly uses Java threads, exception handling, primitive data types, and libraries. It adds to these basic elements most of R4RS Scheme (failing only in that call/cc is partially implemented as call/ec and strings are not mutable). Jscheme is fully tail recursive, both when interpreted and compiled.
Jscheme has been designed to compete with Java as a language for programming the Java Virtual Machine. It provides full access to Java and can be easily called from Java. In this talk we describe the Jscheme language and demonstrate how it compares to Java in implementing applications, servlets, applets, and Java Web Start applications. We also compare Jscheme to some of the other Java implementations of Scheme including Kawa and SISC.
NU Programming Languages Seminar Wednesday, May 15, 2002 306 Egan Hall, Northeastern University (building 44 on http://www.campusmap.neu.edu/) 9:30-11:30
Richard Rasala and Viera Proulx
will continue their presentation on
Java Power Tools: Abstractions and Encapsulations
This talk presents abstractions and encapsulations in the Java Power Tools (JPT) that are used to:
* encapsulate model-string communication * encapsulate view-string communication * encapsulate building and using GUI components * encapsulate creating and using actions * encapsulate event handling * encapsulate error handling and parsing * encapsulate the organizing of displays and layouts into compound components
We will also present the Problem Solving Framework designed for the exploration, testing, and development of programs and their component classes.
The Java Power Tools toolkit lays the foundation for defining and implementing a language for designing and building GUI-based applications. This will be discussed at the conclusion of the talk.
NU Programming Languages Seminar Wednesday, May 8, 2002 306 Egan Hall, Northeastern University (building 44 on http://www.campusmap.neu.edu/) 9:30-11:30
Richard Rasala and Viera Proulx
Java Power Tools: Abstractions and Encapsulations
This talk presents abstractions and encapsulations in the Java Power Tools (JPT) that are used to:
* encapsulate model-string communication * encapsulate view-string communication * encapsulate building and using GUI components * encapsulate creating and using actions * encapsulate event handling * encapsulate error handling and parsing * encapsulate the organizing of displays and layouts into compound components
We will also present the Problem Solving Framework designed for the exploration, testing, and development of programs and their component classes.
The Java Power Tools toolkit lays the foundation for defining and implementing a language for designing and building GUI-based applications. This will be discussed at the conclusion of the talk.
NU Programming Languages Seminar Wednesday, May 1, 2002 306 Egan Hall, Northeastern University (building 44 on http://www.campusmap.neu.edu/) **9:30-11:30** **NOTE NEW MEETING TIME**
The Safe C Runtime Analyzer Alan Feuer
Nearly every day we are reminded that the spread of Internet access has opened the door for subtle program errors to become major security holes. Memory errors in C/C++ programs are a popular target of hackers. This talk will describe a runtime system for C programs that detects most memory errors. The program, sold commercially until 1993 as the Safe C Runtime Analyzer, works as a precompiler, transforming ordinary C programs into instrumented programs that are then compiled using a standard compiler. When an instrumented program is run, error messages are logged as they are detected. An important attribute of Safe C is that instrumented code can be mixed freely with non-instrumented code.
The talk will compare the strength of checking in Safe C to other runtime systems such as Purify and BCC. It will also include a brief demonstration of the software and present details of pointer checking. My primary purpose in presenting this rather dated work is to ascertain if there is interest in bringing the software into the college for further development. Feedback on the future potential of this work is solicited.
Upcoming presentations:
5/8 Richard Rasala and/or Viera Proulx: Program Patterns in the Java Power Tools toolkit (tentative).
Most meetings will be 930-1130 in 306 EG.
NU Programming Languages Seminar Wednesday, April 17, 2002 306 Egan Hall, Northeastern University (building 44 on http://www.campusmap.neu.edu/) **9:30-11:30** **NOTE NEW MEETING TIME**
Prof. Jonathan P. Bowen, South Bank University, London, UK www.jpbowen.com
will present
The Operational Semantics and Animation of the VERILOG Hardware Description Language
Abstract:
The VERILOG Hardware Description Language (HDL) is widely used in industry, despite the fact that the semantics is only informally defined as an IEEE standard. This talk presents a formalization of the key aspects of VERILOG using an operational semantics approach. The semantics have been formulated using the logic programming language Prolog. This allows the possibility of animating VERILOG programs directly from the semantic description. Using this approach enables the exploration of sometimes subtle behaviours of parallel programs and the possibility of rapid changes or additions to the semantics of the language covered. It also acts as a check on the validity of the operational semantics.
NU Programming Languages Seminar Wednesday, April 10, 2002 306 Egan Hall, Northeastern University (building 44 on http://www.campusmap.neu.edu/) **9:30-11:30** **NOTE NEW MEETING TIME**
Karen Zee will present
Write Barrier Removal by Static Analysis
We present a new static analysis for removing unnecessary write barriers in programs that use generational garbage collection. To our knowledge, this is the first analysis for this purpose. Our algorithm uses an interprocedural, flow-sensitive pointer analysis to locate assignments that always create a reference from a younger object to an older object, then transforms the program to eliminate the write barriers normally associated with such assignments. To enhance the effectiveness of the technique, we have implemented two transformations that reorder object allocations. These transformations can dramatically increase the number of write barriers that our algorithm is able to eliminate.
Results from our implemented system show that our technique can eliminate the majority of the write barriers in most of the programs in our benchmark set, producing modest performance improvements of up to 8% of the overall execution time. Moreover, by dynamically instrumenting the executable, we are able to show that for all but two of our nine benchmark programs, our analysis is close to optimal in the sense that it eliminates the write barriers for almost all assignments that do not, in the observed execution, create a reference from an older object to a younger object.
NU Programming Languages Seminar Wednesday, March 6, 2002 306 Egan Hall, Northeastern University (building 62 on the unfortunate map at http://www.neu.edu/maps/maps.html) 1030-1230
Fabio Rojas will present
"Abstract Models of Memory Management," by Morriset, Felleisen, and Harper
This paper was presented in FPCA 95 and was published as a Technical Report from the School of Computer Science at Carnegie Mellon University.
I will present the authors' framework for calculi that make the heap of a program "syntactically apparent." This approach can be used as the basis for specifying grabage collection alogrithms and for proving the correctness of such algorithms. As examples, I will present the authors's proof for the correctness of trace-based garbage collection, generational garbage collection, and type-based, tag-free collection. I will also show how this framework can be used to specify and prove that type inference can be used to identify objects as garbage if they are never used but are still accesible.
The paper is available at: http://www.ccs.neu.edu/scheme/pubs/fpca95-mfh.ps.gz
NU Programming Languages Seminar Wednesday, February 27, 2002 306 Egan Hall, Northeastern University (building 62 on the unfortunate map at http://www.neu.edu/maps/maps.html) 1030-1230
Harold Ossher and Peri Tarr IBM Thomas J. Watson Research Center
Multi-Dimensional Separation of Concerns
Multi-dimensional separation of concerns is a new approach to constructing, integrating and evolving software. Developers can decompose and organize code and other artifacts according to multiple, arbitrary criteria (concerns) simultaneously--even after the software has been implemented--and synthesize or integrate the pieces into larger-scale components and systems. This facilitates several common development and evolution activities, including: adaptation, customization and instrumentation; addition and mix-and-match of features; reconciliation and integration of multiple domain models; reuse and product line management; extraction or replacement of existing parts of software; and "on-demand remodularization."
In this talk, we will introduce and illustrate the concepts behind multi-dimensional separation of concerns, discuss how it relates to aspect-oriented software development, and briefly describe Hyper/J, our support for Java(tm) developers. We will discuss experience with Hyper/J, and a number of interesting and challenging research problems that remain.
More on HyperJ is at http://www.alphaworks.ibm.com/tech/hyperj.
NU Programming Languages Seminar Wednesday, February 20, 2002 306 Egan Hall, Northeastern University (building 62 on the unfortunate map at http://www.neu.edu/maps/maps.html) 1030-1130
Paul Graunke
Title: Growing GUIs on Trees
Web browsers permit consumers to backtrack, clone, and bookmark sites for future visits during interactions. My talk will show how to adapt this general and powerful form of interaction to a class of GUIs, including wizards.
NU Programming Languages Seminar Wednesday, February 13, 2002 306 Egan Hall, Northeastern University (building 62 on the unfortunate map at http://www.neu.edu/maps/maps.html) 1030-1230
Greg Sullivan, MIT
Design and Implementation of GLOS, "Greg's Little Object System"
Over the past few years and several projects, I've developed a small library of Scheme functions and macros that provide: * record types with multiple inheritance, * multiple dispatch (multimethods), * a type system with singleton types, conjunction and disjunction, and predicate types, * simple method combination (before and after methods), and * next-method. The goal has always been to provide orthogonal capabilities with extreme simplicity. The code is currently only about 1500 lines of Scheme. I will give an overview of the system, with lots of examples, including some from a project implementing the GOF Design Patterns in Scheme. I am interested in feedback from other Schemers not only regarding design and implementation issues but also whether this system might be useful for teaching object-oriented programming, as an alternative to the more popular message passing, class-centric approaches.
NU Programming Languages Seminar Wednesday, February 6, 2002 306 Egan Hall, Northeastern University (building 62 on the unfortunate map at http://www.neu.edu/maps/maps.html)
No pl-seminar today, but we have PL Day instead. See http://www.ccs.neu.edu/home/matthias/PL/
NU Programming Languages Seminar Wednesday, January 30, 2002, 10:30-12:30 306 Egan Hall, Northeastern University (building 62 on the unfortunate map at http://www.neu.edu/maps/maps.html)
Mitchell Wand
will continue his presentation on
Small-step Flow Analysis: But Wait, There's More!
0CFA is known to be sound with respect to a variety of semantics: big and small step; call-by-name, call-by-value, and unrestricted beta. We will sort out some of these soundness results.
We show that the soundness theorem a la Palsberg 95 (small-step, substitution semantics) is strictly weaker than the the soundness theorem a la Palsberg 94/Wand-Steckler 94 (big-step, environment semantics).
[On 1/30 we'll start here:]
We retrieve the power of environment semantics for a small-step semantics by showing the soundness of 0CFA for a small-step environment/continuation machine. We then extend the proof to cover a store; providing a simpler alternative to the semantics of (Flanagan and Felleisen 95).
The presentation will be largely self-contained if you weren't here on the 23rd.
NU Programming Languages Seminar Wednesday, January 23, 2002, 10:30-12:30 306 Egan Hall, Northeastern University (building 61 on the map at http://www.neu.edu/maps/maps.html)
Mitchell Wand
Small-step Flow Analysis: But Wait, There's More!
0CFA is known to be sound with respect to a variety of semantics: big and small step; call-by-name, call-by-value, and unrestricted beta. We will sort out some of these soundness results.
We show that the soundness theorem a la Palsberg 95 (small-step, substitution semantics) is strictly weaker than the the soundness theorem a la Palsberg 94/Wand-Steckler 94 (big-step, environment semantics).
We retrieve the power of environment semantics for a small-step semantics by showing the soundness of 0CFA for a small-step environment/continuation machine. We then extend the proof to cover a store; providing a simpler alternative to the semantics of (Flanagan and Felleisen 95).
But wait, there's more!.... depending on time.
NU Programming Languages Seminar Wednesday, January 9, 2002, 10:30-12:30 306 Egan Hall, Northeastern University (building 61 on the map at http://www.neu.edu/maps/maps.html)
Galen Williamson
We introduce a new proof technique for showing the correctness of 0CFA-like analyses with respect to small-step semantics. We illustrate the technique by proving the correctness of 0CFA for the pure lambda-calculus under arbitrary beta-reduction. This result was claimed by Palsberg in 1995; unfortunately, his proof was flawed. We provide a correct proof of this result, using a simpler and more general proof method. We illustrate the extensibility of the new method by showing the correctness of an analysis for the Abadi-Cardelli object calculus under small-step semantics.
NU Programming Languages Seminar Wednesday, December 5, 2001, 10:30-12:30 306 Egan Hall, Northeastern University (building 61 on the map at http://www.neu.edu/maps/maps.html)
Paul Steckler
Database Support in PLT Scheme, Past and Possibilities
To be considered seriously as a "scripting language", PLT Scheme needs to be able to connect to existing database servers. For that reason, we wrote a PLT Scheme extension called SrPersist, which implements the ODBC standard. With SrPersist, we can write Scheme programs that work with nearly any commercial relational database. Unfortunately, the programming model for ODBC is all about state, hence unSchemely. Can we design a database API that is suitable for functional languages in general, and Scheme in particular? We'll look at a recent design for Haskell, and Franscisco Solsona's SchemeQL functional layer over SrPersist.
NU Programming Languages Seminar Wednesday, November 14, 2001, 10:30-12:30 149 Cullinane Hall, Northeastern University (building 9 on the map at http://www.neu.edu/maps/maps.html)
Philippe Meunier
Selector-based Versus Conditional-constraint-based Data-flow Analysis of Programs
Static analysis of programs encompasses a whole set of techniques used during many stages of the software development process, from compiler optimization, to debugging, to security analysis. One important such technique is data-flow analysis, to compute the set of values each expression in a program might evaluate to.
In this talk, I will first describe the set-based analysis used by MrSpidey, the old PLT/DrScheme static debugger, and how this analysis uses selectors to simulate the flow of values in a program. I will show why selectors are not adequate enough when trying to analyze language constructs such as case-lambda functions with rest arguments, show how selectors can then be extended with annotations to improve the analysis, and explain why adding annotations is, in the end, not desirable. I will then describe a conditional-constraint-based analysis, explain how it can compute results at least as good as the ones computed by the old analysis, and present experimental data showing why this analysis is preferable to the old one. Finally, I will discuss some implementation issues encountered while implementing the new analysis for R5RS Scheme, for the new, upcoming, version of DrScheme.
NU Programming Languages Seminar Wednesday, November 7, 2001, 10:30-12:30 306 Egan Hall, Northeastern University (building 61 on the map at http://www.neu.edu/maps/maps.html)
Matthew Flatt
University of Utah
Programming Language Support for Software Components
One of the most promising directions for improving programming tools is in language-level support for reusable program components. Although components have been confused with modules or objects in the past, programmers are starting to recognize the importance of components as a separate kind of abstraction, and the value of specific language support for components.
A ``unit'' is a specific language construct that we have developed for defining and linking program components. We developed the unit construct as an extension to the Scheme programming language, and used it in the development of the DrScheme programming environment. More recently, with we have applied units to low-level systems software implemented in C, and to object-oriented Java code. The C tool is called ``Knit,'' and the Java tool is called ``Jiazzi''. (Both tools are freely available from our web site.)
In this talk, I will describe the unit model of program components and our experience with units in Scheme, C, and Java. In particular, I'll show how Jiazzi units complement Java's class system, providing flexibility that is valuable to both component implementors and component consumers.
NU Programming Languages Seminar Wednesday, October 31, 2001, 10:30-12:30 306 Egan Hall, Northeastern University (building 61 on the map at http://www.neu.edu/maps/maps.html)
John Clements Modeling an Algebraic Stepper
Programmers rely on the correctness of their tools. Semanticists have long studied the correctness of compilers, but we make the case that other tools deserve semantic models, too, and that using these models can help in developing these tools.
We examine these ideas in the context of DrScheme's stepper. The stepper operates within the existing evaluator, placing breakpoints and reconstructing source expressions from information placed on the stack. We must ask whether we can prove the correspondence between the source expressions emitted by the stepper and the steps in the formal reduction semantics.
To answer this question, we develop a high-level semantic model of the extended compiler and run-time machinery. Rather than modeling the evaluation as a low-level machine, we model the relevant low-level features of the stepper's implementation in a high-level reduction semantics. The higher-level model greatly simplifies the correctness proof. We expect the approach to apply to other semantics-based tools.
NU Programming Languages Seminar Wednesday, October 17, 2001 **10:30-12:30** 306 Egan Hall, Northeastern University (building 61 on the map at http://www.neu.edu/maps/maps.html)
Two presentations by Will Clinger
Research Topics in Garbage Collection
This short presentation describes a few research questions that have been raised by recent work on garbage collection.
Representation Inference in Twobit
The development version of the Twobit compiler for Scheme uses a table-driven algorithm to infer representations, and uses this knowledge to generate better machine code. These optimizations are implemented by about 1100 source lines of Scheme code, not including tables. Using concrete examples from Twobit, I expect to stimulate enthusiastic debate on the nature and role of types in Scheme and in programming languages in general.
Mitch Wand and Matthias Felleisen have promised to be in their finest fettle for this discussion.
NU Programming Languages Seminar Thursday, August 23, 2001, 10:30-12:30 149 Cullinane Hall, Northeastern University (building 9 on the map at http://www.neu.edu/maps/maps.html)
Paul Blain Levy, Brandeis University
Call-By-Push-Value: A Subsuming Paradigm
Abstract
Call-by-push-value (CBPV) is a new programming language paradigm, based on the slogan ``a value is, a computation does''. We claim that CBPV provides the semantic primitives from which the call-by-value and call-by-name paradigms are built. Evidence for this claim is found in a remarkably wide range of semantics: from operational semantics, in big-step form and in machine form, to denotational models using domains, possible worlds, continuations and games.
In this talk, we introduce the CBPV paradigm. Using an example program, we see how application and lambda can be understood as push and pop instructions for a stack. We make this more formal with a Felleisen/Friedman-style CK-machine.
We provide Scott semantics, printing semantics and continuation semantics for CBPV and see how we recover familiar and less familiar semantics for call-by-value and call-by-name.
NU Programming Languages Seminar Wednesday, March 14, 2001; 10:00am 149 Cullinane Hall, Northeastern University (building 9 on the map at http://www.neu.edu/maps/maps.html)
Jens Palsberg (Purdue University) will present
Efficient and Flexible Matching of Recursive Types
(Joint work with Tian Zhao; presented at LICS 2000)
Abstract:
Equality and subtyping of recursive types have been studied in the 1990s by Amadio and Cardelli; Kozen, Palsberg, and Schwartzbach; Brandt and Henglein; and others. Potential applications include automatic generation of bridge code for multi-language systems and type-based retrieval of software modules from libraries. Auerbach, Barton, and Raghavachari advocate a highly flexible combination of matching rules for which there, until now, are no efficient algorithmic techniques. In this paper, we present an efficient decision procedure for a notion of type equality that includes unfolding of recursive types, and associativity and commutativity of product types, as advocated by Auerbach et al. For two types of size at most n, our algorithm decides equality in O(n^2) time. The algorithm iteratively prunes a set of type pairs, and eventually it produces a set of pairs of equal types. In each iteration, the algorithm exploits a so-called coherence property of the set of type pairs produced in the preceding iteration. The algorithm takes O(n) iterations each of which takes O(n) time, for a total of O(n^2) time.