NU Programming Languages Seminar Wednesday, May 27, 2003 206 Egan Hall, Northeastern University (building 60 on http://www.campusmap.neu.edu/) 1030-1230
[Sorry about the late notice -Mitch]
Torben Amtoft, Kansas State University:
The Semantic Soundness of a Type System for Interprocedural Register Allocation and Constructor Flattening
Abstract: We consider the semantic soundness of an annotated type system for a compiler intermediate language. (The type system was introduced at TLDI'03 and designed to support interprocedural register allocation and the representation of tuples and variants directly in the register file.)
We define an abstract machine that simultaneously
(1) simulates the assembly code generated by the register annotations
(2) evaluates the original program using standard techniques.
A consistency theorem then ensures that the two semantics coincide, in particular that live registers are not overwritten. Thus our correctness result is stronger than what is seen for, e.g., Typed Assembly Language.
This is joint work with Bob Muller.
NU Programming Languages Seminar Wednesday, April 23, 2003 206 Egan Hall, Northeastern University (building 60 on http://www.campusmap.neu.edu/) 1030-1230
XeLda: Unit-checker for spreadsheets
Tudor Antoniu Brown University
XeLda is a unit-checker for Excel spreadsheets. When units are misused or derived units clash with unit annotations, XeLda flags errors. Specifically, it highlights the offending cells and allows the user to draw source arrows for debugging. Our tool is sensitive to the intracicies of Excel spreadsheets, and can handle tables, matrices, and even circular references. Our approach draws on the idea of unit inference for programming languages developed by Goubault, Kennedy, Wand, and others. XeLda integrates smoothly with Excel by accessing its COM interfaces from PLT Scheme. Our technology can detect errors in the dimensional consistency of some off-the-shelf scientific spreadsheets.
NU Programming Languages Seminar Wednesday, February 5, 2003 206 Egan Hall, Northeastern University (building 60 on http://www.campusmap.neu.edu/) 1030-1230
Putting Failure in Context
Mitch Wand
There are two well-known models of non-deterministic programming. The direct semantics takes a non-deterministic program to denote a stream of possible answers. The continuation semantics uses two continuations, a success continuation and a failure continuation, to model explicit backtracking. The connection between these two models is subtler than one might expect. We show how the connection goes, using context machines as an intermediate representation.
NU Programming Languages Seminar Wednesday, January 22, 2003 206 Egan Hall, Northeastern University (building 60 on http://www.campusmap.neu.edu/) 1030-1230
The Java Syntactic Extender
Jonathan Bachrach, MIT AI Lab
The ability to extend a programming language with new constructs is a valuable tool. With it, system designers can grow a language towards their problem domain, enhance productivity and ease maintenance. We present an extension to the Java language, called the Java Syntactic Extender (JSE), that allows Java programmers to define new syntactic constructs. The design is based on the Dylan macro system (e.g., rule-based pattern matching and hygiene), but exploits Java's compilation model to offer a full procedural macro engine. In other words, syntax expanders may be implemented in, and so use all the facilities of, the full Java language. This talk will include motivating examples, an implementation overview, and future challenges. The described system is implemented and working as a Java preprocessor.
Joint work with Keith Playford of Functional Objects, Inc.
Bio: Jonathan Bachrach is a research scientist at the MIT AI Lab. Upcoming presentations:
NU Programming Languages Seminar Wednesday, January 8, 2003 206 Egan Hall, Northeastern University (building 60 on http://www.campusmap.neu.edu/) 1030-1230
Kenneth Baclawski College of Computer and Information Science
An ontology is a theory about what entities can exist and how entities can be related with each other in a domain. Ontologies are emerging as the most effective means for enabling flexible communication between autonomous computer systems. The notion of ontology is at the center of the "Semantic Web", proposed by Tim Berners-Lee and featured in a recent article in Scientific American. This talk will give some motivation for ontology-based computing and will discuss some of the research and development efforts that are attempting to make ontology-based computing a reality:
- The Web Ontology Language (OWL), a standard language for expressing ontologies and knowledge representations.
- Inference and consistency checking.
- Performance and scalability problems.
- Integration with other computer-based technologies, such as programming languages, databases, Web servers, etc.
- Applications of ontology-based computing in such diverse areas as biomedical research, wireless communication and situation awareness.
NU Programming Languages Seminar Wednesday, November 13, 2002 306 Egan Hall, Northeastern University <<- NOTE NONSTANDARD ROOM (building 60 on http://www.campusmap.neu.edu/) 1030-1230
Harry Mairson Computer Science Department Brandeis University
"From Hilbert Spaces to Dilbert Spaces: Context Semantics Made Simple"
I want to give a first-principles description of the {\em context semantics} of Gonthier, Abadi, and L\'{e}vy, a computer-science analogue of Girard's {\em geometry of interaction.} I'll explain how this denotational semantics models lambda-calculus, and more generally multiplicative-exponential linear logic (MELL), by explaining the call-by-name (CBN) coding of the lambda-calculus, and proving the correctness of {\em readback}, where the normal form of a lambda-term is recovered from its semantics. This analysis yields the correctness of Lamping's optimal reduction algorithm.
I also hope to discuss the relation of context semantics to linear logic types and to ideas from {\em game semantics}, used to prove full abstraction theorems for PCF and other lambda-calculus variants, and to discuss their relation to Levy labels (used for {\em labelled reduction} in lambda calculus) and their relation to flow analysis. This talk doesn't have a lot of theorems, but it does have a lot of nice looking pictures.
NU Programming Languages Seminar Wednesday, November 6, 2002 206 Egan Hall, Northeastern University (building 60 on http://www.campusmap.neu.edu/) <<- NOTE CORRECT MAP REFERENCE 1030-1230
Sukyoung Ryu
Harvard University
Title: Debugging Everywhere Project (work in progress)
Abstract: Even though many current applications run on heterogeneous networks and are composed of modules written in different programming languages, debugging technology is not ready to support such applications. We are developing techniques for building source-level debuggers for multiple platforms and multiple languages. Since our project has shown that it is easy to retarget our prototype, ldb, from machine to machine, we are focusing on supports for multi-language debugging.
Much of a debugger's job is to undo what the compiler has done or to do what the compiler could do, but at run time. And the set of all operations performed by debuggers is small. ldb makes the compiler do as much of this work as possible. Instead of giving the debugger data about the program, forcing it to figure out how to manipulate the data on the target machine, the compiler gives the debugger code that it can run to probe the program. And a variant of the compiler runs at debug time and compiles expressions into PostScript, which ldb uses to evaluate the expressions. Since this approach reuses knowledge already in the compiler, it simplifies debugger and gives much freedom for the compiler writer.
NU Programming Languages Seminar Wednesday, October 16, 2002 206 Egan Hall, Northeastern University (building 44 on http://www.campusmap.neu.edu/) 1030-1230
Andrei Sabelfeld
Language-Based Information-Flow Security
Current standard security practices do not provide substantial assurance that the end-to-end behavior of a computing system satisfies important security policies such as confidentiality. An end-to-end confidentiality policy might assert that secret input data cannot be inferred by an attacker through the attacker's observations of system output; this policy regulates information flow.
Conventional security mechanisms such as access control and encryption do not directly address the enforcement of information-flow policies. Recently, a promising new approach has been developed: the use of programming-language techniques for specifying and enforcing information-flow policies. In this article we survey the past three decades of research on information-flow security, particularly focusing on work that uses static program analysis to enforce information-flow policies. We give a structured view of recent work in the area and identify some important open challenges.
Paper available via
http://www.cs.cornell.edu/~andrei/Papers/jsac.ps http://www.cs.cornell.edu/~andrei/Papers/jsac.pdf
NU Programming Languages Seminar Wednesday, October 9, 2002 206 Egan Hall, Northeastern University (building 44 on http://www.campusmap.neu.edu/) 1030-1230
John Clements
Peaceful Coexistence for Tail Calls & Stack Inspection
Security folklore holds that a programming language with stack inspection for security permissions cannot implement a global tail call optimization policy. That is, an implementation of such a language may have to allocate memory for a tail call in the source code. As a result, a program that uses only tail calls may nevertheless exhaust the available memory. We prove this widely held belief wrong. We exhibit an abstract machine for a language with security stack inspection whose space consumption function is equivalent to that of the canonical tail call optimizing abstract machine. The machine is surprisingly simple and suggests that tail-calls are as easy to implement in a security setting as they are in a conventional one.
NU Programming Languages Seminar Wednesday, September 18, 2002 206 Egan Hall, Northeastern University (building 44 on http://www.campusmap.neu.edu/) 9:00-11:00
Cormac Flanagan (SRC, DEC/Compaq/HP)
Program Checking = Logic + Lambda
Ensuring the correctness and reliability of a software system is a challenging problem. Documenting correctness properties that the system should obey is straightforward. For example, it should not dereference dangling pointers or read from unopened files. However, verifying that the system actually satisfies these properties is much harder.
Automatic theorem proving provides a promising approach for verifying that a code fragment satisfies its correctness properties for all possible input values. However, existing fully-automatic theorem provers are unable to reason directly about code that uses iteration or recursion, and instead require the programmer to help by supplying loop invariants and procedure specifications. The burden of providing these annotations has so far limited the cost-effectiveness of such checking tools.
This talk presents a novel, annotation-free approach to program checking. Our approach is based on an extended logic that provides explicit support for iteration and recursion. Although the satisfiability of queries in this logic is undecidable in general, we present an efficient semi-algorithm based on a combination of lazy abstraction, counter-example driven abstraction refinement, and explicating, proof-generating decision procedures for specific theories such as linear arithmetic.
The problem of deciding if a software system satisfies its correctness properties can be then expressed as a satisfiability query in this logic, without burdening the programmer with supplying loop invariants and procedure specifications.