Programming Languages Seminar

Regular Meeting Time:

Wednesdays, 11:45am-1:45pm. Brown-bag lunch is encouraged.

We meet in 366 WVH (West Village Building H) [directions].

PL-seminar planning wiki (NUCCIS login required, sorry).

Organizers:

Mitchell Wand (wand@ccs.neu.edu)
(617) 373 2072
Will Clinger (will@ccs.neu.edu)
(617) 373 8687
Matthias Felleisen (matthias@ccs.neu.edu)
(617) 373 2085
Olin Shivers
Riccardo Pucella (riccardo@ccs.neu.edu)
(617) 373-2076

College of Computer and Information Science, Northeastern University
360 Huntington Avenue #202 WVH,
Boston, MA 02115
Fax: (617) 373-5121

To subscribe to the pl-seminar mailing list, visit the mailing list home page.

[Mail archives | Old Schedules]

[Semantics at NU | College of Computer and Information Science | Northeastern University]

NU Programming Languages Seminar Wednesday, May 28, 2008 11:45-1:30 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

William Cook University of Texas at Austin

Strategic Programming by Model Interpretation and Partial Evaluation (Work in Progress)

Abstract: Strategic Programming is a programming paradigm based on factoring programs into general strategies and descriptions of particular application requirements. The descriptions are called models, and they generally describe one aspect of an application. Parser generators (like Yacc) are a prototypical example of strategic programming. My talk focuses on defining the semantics of models using interpreters instead of transformations, as in most related work. It may be possible to define fully-functional applications by a collection of interrelated models for different aspects of a system, including user interface, security, workflow, data abstraction and persistence. The models may also contain fragments of code written in general-purposes languages. Model interpreters are compiled by partial evaluation. One novelty of this approach is the ability to create data abstractions by model interpretation and compile them by partial evaluation. I will describe my progress on a Scheme implementation of a software development toolset, called Borg, to support strategic programming by model interpretation and partial evaluation. Borg is implemented in itself and is targeted at information management applications, including desktop, web and distributed services, although it may be applicable to other domains as well. This is a description/discussion of work in progress.

================================================================

Upcoming Events:

No events scheduled. Come give a talk!

--Mitch

NU Programming Languages Seminar Wednesday, April 23, 2008 11:45-1:30 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Bryan Chadwick Removing Accidental Traversal Complexities from Programs

In this talk we present a functional traversal abstraction that decomposes traversal computation into three sets of functions (or function objects) and a traversal control function. Sets of functions transform, combine values, and modify traversal arguments over a generic traversal, while the control function allows programmers to limit the extent of a traversal. A multiple dispatch mechanism matches functions/methods to applicable types during data structure traversal providing more flexible computation during traversal, supporting multiple levels of generalization. Using the generic traversal and matching we eliminate explicit accesses to the underlying structure and reduce the need for traversal calls. The resulting programs can be checked with respect to specific types encountered during a traversal, resulting in programs that are safer than previous imperative Adaptive Programming solutions.

Our new abstraction is supported by Java and Scheme libraries that allow programmers to use functional and OOP techniques to develop traversal related programs. The libraries provide a rich set of default traversal behavior supporting SYB style transformations and queries in addition to more complex (ad-hoc) computation. We describe the traversal algorithm, functional decomposition, and its usefulness using a few common examples in Scheme (BST and lambda calculus related functions). Our Java Library, called DemeterF, has been used in two graduate courses here at Northeastern (PPL and Software Development), to reduce traversal complexity in interpreters, type checkers, and CSP related algorithmic game players.

================================================================

Upcoming Events:

No events scheduled. Come give a talk!

--Mitch

Pl-Seminar Announcement, revision 3: Log: Revision 3: NU Class picture is at 1145, so we will start at 1200 instead Revision 2: Room changed from 108 to 366 (the usual place). Sorry for the confusion. --Mitch

NU Programming Languages Seminar Wednesday, April 16, 2008 ** NOTE CORRECTED TIME ** 12:00-1:30 **NOTE CORRECTED ROOM** Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Nikolaos Papaspyrou National Technical University of Athens

Continuations for Prototyping Concurrent Languages

Continuation Semantics for Concurrency (CSC) is a technique that attempts to exploit the benefits of using continuations in concurrent systems development. In CSC, a continuation is an application-dependent configuration of computations (partially evaluated denotations). Every computation or group of computations contained in a continuation can be accessed and manipulated separately by the denotational semantic function. The CSC technique provides excellent flexibility and a "pure" continuation-based approach to communication and concurrency, in which all control concepts are modeled as operations manipulating continuations.

This talk is about a methodology for concurrent language development, based on denotational semantics. We propose carefully designed continuation structures for various traditional concurrent control concepts, or for more complex constructs such as remote object (process) destruction and cloning. We show that, by using the CSC technique, a simple relation can be established between the structure of continuations and the control flow constructs of the language under study. Using monads and the lazy functional programming language Haskell, we show how to obtain semantic interpreters for concurrent languages, capable of producing either one or all possible execution traces of a program.

[joint work with Eneia Todoran, Technical University of Cluj-Napoca]

================================================================

Upcoming Events:

# Wed 4/23 Bryan Chadwick: Functional Adaptive Programming with DemeterF

We are otherwise open. Come give a talk!

--Mitch

NU Programming Languages Seminar Wednesday, April 16, 2008 11:45-1:30 **NOTE CORRECTED ROOM** Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Nikolaos Papaspyrou National Technical University of Athens

Continuations for Prototyping Concurrent Languages

[joint work with Eneia Todoran, Technical University of Cluj-Napoca]

================================================================

Upcoming Events:

# Wed 4/23 Bryan Chadwick: Functional Adaptive Programming with DemeterF

We are otherwise open. Come give a talk!

--Mitch

NU Programming Languages Seminar Wednesday, April 16, 2008 11:45-1:30 Room 108 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Nikolaos Papaspyrou National Technical University of Athens

Continuations for Prototyping Concurrent Languages

[joint work with Eneia Todoran, Technical University of Cluj-Napoca]

================================================================

Upcoming Events:

# Wed 4/23 Bryan Chadwick: Functional Adaptive Programming with DemeterF

We are otherwise open. Come give a talk!

--Mitch

NU Programming Languages Seminar Wednesday, April 2, 2008 12:00-1:30 Room 108 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

** NOTE NON-STANDARD TIME AND ROOM ** ** This is a joint presentation with the NU ACM Student Chapter ** ** Come on time if you want a seat, and pizza **

Caml Trading Yaron Minsky Jane St. Capital

Jane Street Capital is a successful proprietary trading company that has shifted from developing software in mainstream programming languages to developing software almost entirely in OCaml, a statically typed functional programming language that has only modest industrial use. The scope of the enterprise is small but growing: Jane Street now has over 25 OCaml programmers who have collectively written hundreds of thousands of lines of OCaml code. OCaml is used for building everything from trading systems to research infrastructure to user interfaces to systems administration tools. This talk will discuss the motivations behind Jane Street's adoption of OCaml, and why we think that statically typed functional programming languages are such a good fit for the world of trading and finance.

================================================================

Upcoming Events:

# Wed 4/9 open # Wed 4/16 Nikolaos Papaspyrou: Continuations for Prototyping Concurrent Languages

We are otherwise open. Come give a talk!

--Mitch

NU Programming Languages Seminar Wednesday, March 26, 2008 11:45am-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Spatial Computing in Proto Jonathan Bachrach, MIT CSAIL

ABSTRACT

The computational landscape is drastically changing. Processing, sensing, communication, and actuation are now affordable and embeddable, allowing us to manufacture myriads of devices that can be spread through space and placed in the world. The catch is that in order to manufacture these devices economically in bulk, we must accept faults, inaccuracies, and communication delays. If we were to be able to robustly harness these devices, we could economically develop systems with unparalleled power, grace, fidelity, and pervasiveness. Example spatial computing domains are sensor networks, smart materials, swarm robotics, biofilms, and modular robotics, to name a few. Unfortunately, traditional engineering approaches do not apply, and we must rethink our computing models, languages, and practices. Typical solutions entangle robustness with coordination, producing applications that do not scale well and modules that do not compose well nor map easily over to other application domains. We offer an alternate approach whereby the programmer controls a single virtual _spatial computer_ which fills the environment space. The computations on this spatial computer are actually performed by a large number of locally-interacting individual devices. This abstracts the actual computational hardware behind the spatial computer interface, and allows the programmer to focus on a single model of global computation. We achieve this abstraction with two components: a language that embodies continuous space and time semantics and a runtime library that implements these semantics approximately. In this talk, I will introduce our language, called Proto, using examples from sensor networks, and hint at the generality of the approach, using examples from modular and swarm robotics.

BIO

Jonathan Bachrach is a research scientist at the MIT Computer Science and Artificial Intelligence Lab (CSAIL) who researches programming languages, spatial computing, and robotics. Before MIT, he held postdocs at Stanford and UC Berkeley, was a researcher at IRCAM in Paris, developing new musical platforms, and a principal software engineer at Harlequin Inc (RIP), working on a compiler and runtime for the Dylan programming language. He studied cognitive science, computer science, and visual arts, receiving a B.S. degree from the University of California at San Diego and MS and PhD degrees from the University of Massachusetts at Amherst.

================================================================

Upcoming Events:

# Wed 4/2 open # Wed 4/9 open # Wed 4/16 Nikolaos Papaspyrou: Continuations for Prototyping Concurrent Languages

We are otherwise open. Come give a talk!

--Mitch

NU Programming Languages Seminar Wednesday, February 27, 2008 11:45am-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Interface Safety in Multilingual Software Gang Tan Boston College

Most real-world software systems consist of software components developed in different programming languages. For example, Sun's Java Development Kit 1.6 (JDK) contains around 2 million lines of Java code as well as 800,000 lines of C/C++ code. Unfortunately, the interface code that glues multilingual software components is a constant source of software bugs and vulnerabilities. This is demonstrated by our empirical security study of JDK 1.6, which identified O(100) bugs in the interface code between Java and C components.

We propose two novel frameworks that shed light on how to achieve interface safety in multilingual software. The first system, SafeJNI, follows the principle of language-based isolation to ensure C code respects Java's invariants. The second system, ILEA, is a general framework for performing analysis across programming-language boundaries. By automatically extracting an approximate Java specification from C code, ILEA enables existing Java analyses to cover foreign C code.

================================================================

Upcoming Events:

# Wed 3/5 no seminar: spring break # Wed 3/19 no seminar # Wed 4/16 Nikolaos Papaspyrou: Continuations for Prototyping Concurrent Languages

We are otherwise open. Come give a talk!

--Mitch

NU Programming Languages Seminar Wednesday, February 13, 2008 11:45am-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

An overview of Manticore, a heterogeneous parallel language. Riccardo Pucella, Northeastern University

Manticore is a new functional language for parallel programming being developed at the University of Chicago. Unlike many parallel languages, Manticore is meant to be heterogeneous: it supports parallelism as several levels of granularity. Pragmatically, it combines CML-style explicit concurrency with NESL-style fine-grain, implicitly threaded, data parallel constructs. I will review the basic design of Manticore, and outline some challenges in its implementation.

================================================================

Upcoming Events:

# Wed 2/20 no seminar # Wed 2/27 Gang Tan (BC): Interface Safety in Multilingual Software # Wed 3/5 no seminar: spring break # Wed 3/19 no seminar # Wed 4/16 Nikolaos Papaspyrou: Continuations for Prototyping Concurrent Languages

We are otherwise open. Come give a talk!

--Mitch

NU Programming Languages Seminar Wednesday, February 6, 2008 11:45am-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Sorry, no seminar this week. Riccardo Pucella's talk on Manticore will be rescheduled to next week, Wednesday, 2/13.

================================================================

Upcoming Events:

# Wed 2/13 Riccardo Pucella: The Manticore project # Wed 2/20 et seq are open. Come give a talk!

--Mitch

NU Programming Languages Seminar Wednesday, January 30, 2008 11:45am-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Gene Cooperman Northeastern University

Multi-Core Processors: Background and Issues from an Applications Viewpoint

(sorry, no abstract available)

================================================================

Upcoming Events:

# Wed 2/6 Riccardo Pucella: The Manticore project # Wed 2/13 et seq are open. Come give a talk!

--Mitch

NOTE CHANGE OF TIME FOR TUESDAY'S TALK BY CHRISTIAN URBAN

================================================================

NU Programming Languages Seminar Tuesday, 1/22/08 9:30-11:00am (**NOTE CHANGE OF TIME **) Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Christian Urban TU Munich

Nominal Techniques in the Theorem Prover Isabelle or, How Not to be Intimidated by the Variable Convention

Abstract:

Dealing with binders, renaming of bound variables, capture-avoiding substitution, etc., is very often a major problem in formal proofs, especially in proofs by induction. In informal proofs by induction one often assumes a variable convention in order to sidestep all problems and to obtain simple proofs. Unfortunately, this convention is usually not formally justified, which makes it hard to formalise such proofs. In this talk I will show how strong induction principles can be formally derived that have the variable convention already built-in. I will also show that the variable convention depends on some non-trivial conditions in order to be a sound reasoning principle. The aim of this work is to provide all proving technology necessary for reasoning conveniently about the lambda-calculus and programming languages.

================================================================

NU Programming Languages Seminar Wednesday, 1/23/08 11:45am-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Greg Morrisett Harvard University Ynot: integrating effects with dependent types

I want a type system that will let me capture anything from simple type-safety properties, to contracts, and even go all the way to full correctness. Ideally, the system should have a "pay-as-you-go" property: If you only want simple types, then everything can and should be automated. If you want to prove really deep properties, then you should be able to express this, but you may have to pay the price of writing some explicit proofs (or proof scripts). Furthermore, the language should have a uniform way to treat models, specifications, types, code, and proofs so that abstraction is feasible.

It turns out that Coq (more or less) has such a type system. Unfortunately, it only works on purely functional programs, where effects of any kind are forbidden, including non-termination, mutable state, continuations, I/O, etc. For the past year or two, we've been figuring out how to add these features to Coq. There are some really tricky semantic issues that we had to solve, and a number of implementation issues that we are still working on. We've now written some (mildly) interesting code that leverages these features, including thing like hash-tables and parser combinators. The interfaces capture (partial) correctness, and are designed, in the style of separation logic, with frame properties that make reasoning compositional.

================================================================

Upcoming Events:

# Wed 1/30 Gene Cooperman: Multi-Core Processors: Background and Issues from an Applications Viewpoint # Wed 2/6 Riccardo Pucella: The Manticore project # Wed 2/13 Norman Ramsay: Dataflow 'Optimization' for the Semantically Inclined # Wed 2/20 et seq are open. Come give a talk!

--Mitch

We have two events next week:

================================================================

NU Programming Languages Seminar Tuesday, 1/22/08 11:45am-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Christian Urban TU Munich

Nominal Techniques in the Theorem Prover Isabelle or, How Not to be Intimidated by the Variable Convention

Abstract:

================================================================

NU Programming Languages Seminar Wednesday, 1/23/08 11:45am-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Greg Morrisett Harvard University Ynot: integrating effects with dependent types

================================================================

Upcoming Events:

--Mitch

No pl-seminar, Wed 12/4/07.

The previously scheduled talk on Manticore will be rescheduled for January.

Upcoming Events:

# January is open! Please volunteer! # 02/13 Norman Ramsay: Dataflow 'Optimization' for the Semantically Inclined

--Mitch

NU Programming Languages Seminar Wednesday, November 28, 2007 11:45-1:30 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

WaveScript: Language Support for Distributed Stream Processing

Ryan Newton, MIT

Applications that combine live data streams with embedded, parallel, and distributed processing are becoming more commonplace. WaveScript is a domain-specific language that brings high-level, type-safe, garbage-collected programming to these domains. This is made possible by three primary implementation techniques. First, we employ a novel evaluation strategy that uses a combination of interpretation and reification to partially evaluate programs into stream dataflow graphs. Second, we use profile-driven compilation to enable many optimizations that are normally only available in the synchronous (rather than asynchronous) dataflow domain. Finally, we incorporate an extensible system for rewrite rules to capture algebraic properties in specific domains (such as signal processing).

We have used our language to build and deploy a sensor-network for the acoustic localization of wild animals, in particular, the Yellow-Bellied marmot. In this application, WaveScript yields good performance on both embedded and desktop-class machines, including distributed execution and substantial parallel speedups. In fact, the WaveScript implementation outperformed a previous C implementation of the same algorithms by different authors. CPU time was improved by 35% using fewer than half the lines of code. I will discuss the contribution of our compiler optimizations to this success.

Upcoming Events:

# 12/05 Riccardo Pucella: The Manticore project # 01/16 et seq are open. Volunteer! # 02/13 Norman Ramsay: Dataflow 'Optimization' for the Semantically Inclined

--Mitch

NU Programming Languages Seminar Monday, November 19, 2007, 10:30am-11:30am Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

**NOTE NON-STANDARD DAY AND TIME**

Radha Jagadeesan DePaul University

Trust and Authorization via Provenance and Integrity in Distributed Objects Existing web services, portlets, and mashups can be viewed as collaborative distributed systems built by assembling components from multiple independent applications. These examples motivate the study of methods to facilitate service composition and content aggregation. From a security standpoint, such composition and aggregation involves subtle combinations of authentication, authorization, delegation, trust, and labeling. It has been said that An application can be mashup-friendly or it can be secure, but it cannot be both. We disagree. We describe a calculus of distributed objects and a type-and-effect system to to achieve both security and flexibility aims. This is joint work with Andy Cirillo, James Riely and Corin Pitcher.

Upcoming Events:

# 11/21 Thanksgiving; no meeting # 11/28 Ryan Newton: Language Support for Distributed Stream Processing # 12/05 Riccardo Pucella: The Manticore project # 01/16 et seq are open. Volunteer!

--Mitch

NU Programming Languages Seminar Wednesday November 14, 2007, 11:45am-1:30pm Room *108* WVH (http://www.ccs.neu.edu/home/wand/directions.html) ** NOTE NON-STANDARD ROOM**

Guy Steele: Designing by Accident

Many design efforts rely on the addition of features. But often the best breakthroughs happen by subtraction, when a unifying insight permits the consolidation or elimination of features.

An extreme example of this phenomenon was Scheme, an accidental programming language that had astonishing success. In this talk, Guy Steele will explain what he was trying to do, what went wrong, and why what went wrong was a good thing after all.

Guy Steele invented Scheme in the 1970s, was the driving force behind the first Java specification, was a major contributor to High Performance Fortran, and is now working on a new language called Fortress.

(Joint talk with NU Student ACM Chapter. Pizza will be served. Come early if you want a seat.)

Upcoming Events:

# Mon 11/19 1030am: Radha Jagadeesan # 11/21 Thanksgiving; no meeting # 11/28 Ryan Newton: Language Support for Distributed Stream Processing # 12/05 Riccardo Pucella: The Manticore project # 01/16 et seq are open. Volunteer!

--Mitch

NU Programming Languages Seminar Wednesday November 7, 2007, 11:45am-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Vassilis Koutavas will present:

The Join Calculus: a Language for Distributed Mobile Programming by Fournet, Cardelli, et al.

The join calculus is a language that models distributed and mobile programming. It is characterized by asynchronous communication between processes, an explicit notion of locality, a strict adherence to local synchronization, and a direct embedding of the ML programming language. Local synchronization means that messages always travel to a set destination, and can interact only after they reach that destination; this yields an efficient implementation.

The join calculus is used as the basis for several distributed languages and implementations, such as JoCaml, Polyphonic C#, and the continuation of the latter, Comega.

Upcoming Events:

# 11/14 Guy Steele: Designing by Accident: a History of Scheme # Mon 11/19 1030am: Radha Jagadeesan # 11/21 Thanksgiving; no meeting # 11/28 Ryan Newton: Language Support for Distributed Stream Processing # 12/05 Riccardo Pucella: The Manticore project # 01/16 et seq are open. Volunteer!

--Mitch

NU Programming Languages Seminar Wednesday October 31, 2007, 12:00pm-1:30pm Room 108 WVH (http://www.ccs.neu.edu/home/wand/directions.html) **note non-standard room and starting time**

CCIS Distinguished Lecture Machines Reasoning About Machines J Moore University of Texas at Austin

Computer hardware and software can be modeled precisely in mathematical logic. If expressed appropriately, these models can be executable. This allows them to be used as simulation engines or rapid prototypes. But because they are formal they can be manipulated by symbolic means: theorems can be proved about them, directly, with mechanical theorem provers. But how practical is this vision of machines reasoning about machines? In this highly personal talk, I will describe the 35 year history of the ``Boyer-Moore Project'' and discuss progress toward making formal verification practical. Among other examples I will describe important theorems about commercial microprocessor designs, including parts of processors by AMD, Motorola, IBM, Rockwell-Collins and others. Some of these microprocessor models execute at 90% the speed of C models and have had important functional properties verified. In addition, I will describe a model of the Java Virtual Machine, including class loading and bytecode verification and the proofs of theorems about JVM methods.

Upcoming Events:

# 11/7 Vassilis Koutavas: The join-calculus and polyphonic C-sharp # 11/14 Guy Steele: Designing by Accident: a History of Scheme # Wed 11/21 Thanksgiving; no meeting # Wed 11/28 Ryan Newton: Language Support for Distributed Stream Processing # Wed 12/05 Riccardo Pucella: The Manticore project

--Mitch

NU Programming Languages Seminar Wednesday October 24, 2007, 11:45am-1:30pm

Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Squeak, NewSqueak, and Obliq

Dave Herman

Luca Cardelli experimented with the design of a number of concurrent programming languages in the 80's and 90's. I will discuss the design and implementation of Squeak, a CSP-style programming language for implementing user interface from the 80's, its 90's re-implementation Newsqueak, and Obliq, a distributed concurrent language from the 90's based on a notion of "distributed lexical scope."

Upcoming Events:

# 10/31 J Moore # 11/7 Vassilis Koutavas: The join-calculus and polyphonic C-sharp # 11/14 Guy Steele: Designing by Accident: a History of Scheme # Wed 11/21 Thanksgiving; no meeting # Wed 11/28 Ryan Newton: Language Support for Distributed Stream Processing # Wed 12/05 Riccardo Pucella: The Manticore project

--Mitch

NU Programming Languages Seminar Wednesdays, 11:45am-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

10/10: No seminar this week. This week's seminar has been rescheduled for 10/24, sorry.

Upcoming Events:

# 10/17 Gene Cooperman: Multi-Core Processors: Background and Issues from an Applications Viewpoint # 10/24 David Herman on Obliq and Newsqueak # 10/31 J Moore # 11/7 Vassilis Koutavas: The join-calculus and polyphonic C-sharp # 11/14 Guy Steele: Designing by Accident: a History of Scheme

--Mitch

NU Programming Languages Seminar Wednesdays, 11:45am-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Upcoming Events:

# 10/10 David Herman on Obliq and Newsqueak # 10/17 Gene Cooperman: Multi-Core Processors: Background and Issues from an Applications Viewpoint # 10/31 J Moore # 11/7 Vassilis Koutavas: The join-calculus and polyphonic C-sharp # 11/14 Guy Steele: Designing by Accident: a History of Scheme

--Mitch

NU Programming Languages Seminar Wednesday, 7/25/07 11:45am-1:30pm Room 166 WVH (http://www.ccs.neu.edu/home/wand/directions.html) (** NOTE CHANGE OF LOCATION **)

Jacob Matthews University of Chicago

Parametricity from Run-Time Sealing

Abstract: In this talk, I will follow up on my earlier talk "Operational Semantics for Multi-Language Programs" by extending the technique I presented there to an embedding of call-by-value System F and the call-by-value untyped lambda calculus. While it is not hard to build a type-sound embedding between those two languages, it turns out to be somewhat more challenging to devise an embedding that preserves Reynolds' parametricity property, i.e. that a value whose type contains a free variable must be completely indifferent to the set of values chosen to be the interpretation of that variable. I use Morris's notion of dynamic seals to give such an embedding, and show that the System F side of the resulting system retains parametricity. I will not assume familiarity with the formal details of parametricity; instead I will devote a section of the talk to introducing them (and, more generally, the method of logical relations).

Upcoming Events:

# Don't you want to speak at pl-seminar?

--Mitch

NU Programming Languages Seminar Wednesday, 7/25/07 11:45am-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html) [location subject to change, sorry]

Jacob Matthews University of Chicago

Parametricity from Run-Time Sealing

Upcoming Events:

# Don't you want to speak at pl-seminar?

--Mitch

NU Programming Languages Seminar Tuesday, 6/5/07 3:00-5:00pm (** NOTE NON-STANDARD DAY AND TIME **) Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

It's All about Being Right: Lessons from the R6RS Process

Michael Sperber DeinProgramm

"The original Revised Report on Scheme was taken as a model for future definitions of Scheme, and a self-selected group of so-called ~authors~ took on the role of evolving Scheme. The rule they adopted was that features could be added only by unanimous consent. After a fairly short period [...], the rate of change of Scheme slowed down due to this rule. Only peer pressure in a highly intellectual group could convince any recalcitrant author to change his blackball. As a result there is a widely held belief that whenever a feature is added to Scheme, it is clearly the right thing." --Guy L. Steele, Jr., Richard P. Gabriel, The Evolution of Lisp

Arguably, this process reached its limits with the Revised^5 Report on Scheme: Crucial language additions such as modules, records and exceptions had little chance of reaching unamimous consent, no matter what the specific design. While the editors of the Revised^6 Report no longer follow this rule, standardization is still driven by a strong desire to do the right thing. Continuing the tradition of Lisp culture, reaching this goal has been difficult and elusive, as the participants hold different and strongly opinionated ideas about what the right thing is. In the talk, I will review the R6RS process, and attempt to show that R6RS is indeed the right thing for Scheme.

Upcoming Events:

# 6/1 "Conversations with Functional Programmers" @ Harvard # Don't you want to speak at pl-seminar?

--Mitch

NU Programming Languages Seminar Tuesday, 6/5/07 3:00-5:00pm (** NOTE NON-STANDARD DAY AND TIME **) Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

It's All about Being Right: Lessons from the R6RS Process

Michael Sperber DeinProgramm

Upcoming Events:

# 6/1 "Conversations with Functional Programmers" @ Harvard # Don't you want to speak at pl-seminar?

--Mitch

NU Programming Languages Seminar Wed, 5/30/07 11:45am-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Torben Amtoft Kansas State University

Verification Condition Generation for Conditional Information Flow

Abstract:

We formulate an intraprocedural information flow analysis algorithm for sequential, heap manipulating programs. We prove correctness of the algorithm, and argue that it can be used to verify some naturally occurring examples in which information flow is conditional on some Hoare-like state predicates being satisfied. Because the correctness of information flow analysis is typically formulated in terms of noninterference of pairs of computations, the algorithm takes as input a program together with two-state assertions as postcondition, and generates two-state preconditions together with verification conditions. To process heap manipulations and while loops, the algorithm must additionally be supplied two-state "object flow invariants" as well as two-state "loop flow invariants" which are themselves possibly conditional.

This is joint work with Anindya Banerjee. http://www.cis.ksu.edu/~tamtoft/Papers/Amt+Ban:CondInfFlow-2007/short.pdf

Upcoming Events:

# 6/1 "Conversations with Functional Programmers" @ Harvard # Don't you want to speak at pl-seminar?

--Mitch

**CHANGE OF DATE**

NU Programming Languages Seminar ***TUESDAY 5/22/07*** (*** NOTE CHANGE OF DATE ***) 11:45am-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Relating Complexity and Precision in Control Flow Analysis David Van Horn

We analyze the computational complexity of kCFA, a hierarchy of control flow analyses that determine which functions may be applied at a given call-site. This hierarchy specifies related decision problems, quite apart from any algorithms that may implement their solutions. We identify a simple decision problem answered by this analysis and prove that in the 0CFA case, the problem is complete for polynomial time. The proof is based on a nonstandard, symmetric implementation of Boolean logic within multiplicative linear logic (MLL). We also identify a simpler version of 0CFA related to eta-expansion, and prove that it is complete for LOGSPACE, using arguments based on computing paths and permutations.

For any fixed k>0, it is known that kCFA (and the analogous decision problem) can be computed in time exponential in the program size. For k=1, we show that the decision problem is NP-hard, and sketch why this remains true for larger fixed values of k. The proof technique depends on using the approximation of CFA as an essentially nondeterministic computing mechanism, as distinct from the exactness of normalization. When k=n, so that the ``depth'' of the control flow analysis grows linearly in the program length, we show that the decision problem is complete for EXPTIME.

In addition, we sketch how the analysis presented here may be extended naturally to languages with control operators. All of the insights presented give clear examples of how straightforward observations about linearity, and linear logic, may in turn be used to give a greater understanding of functional programming and program analysis.

(joint work with Harry Mairson)

Upcoming Events:

# 5/30 Torben Amtoft # Don't you want to speak at pl-seminar?

--Mitch

NU Programming Languages Seminar Wednesday, 5/23/07 (** that's NEXT Wed, not tomorrow 5/16 **) 11:45am-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Relating Complexity and Precision in Control Flow Analysis David Van Horn

(joint work with Harry Mairson)

Upcoming Events:

# 5/30 Torben Amtoft # Don't you want to speak at pl-seminar?

--Mitch

NU Programming Languages Seminar Wednesday, 5/2/07 11:45am-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Concurrency-Oriented Programming in Erlang

Jesse Tov

Erlang is a language and methodology for programming fault-tolerant distributed systems. It features lightweight processes that communicate via message passing in a dynamic topology. Erlang claims to provide massive parallelism with little performance penalty, little cost for distribution, and robustness in the face of both programmer error and an uncooperative environment. It has been used to build several successful real-world systems that may demonstrate these properties.

In this talk I will present an introduction to Erlang programming, compare Erlang to other models such as actors and CSP, and attempt to evaluate some of the claims of Erlang's promoters, in particular with respect to the impact of Erlang's design guidelines compared to the importance of language features.

Upcoming Events:

# Don't you want to speak at pl-seminar?

--Mitch

NU Programming Languages Seminar Wednesday, 4/25/07 11:45am-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

An Introduction to Orc

Dimitris Vardoulakis

Abstract:

Orc is a language for task orchestration, a form of concurrent programming suitable for web service coordination. It has a small set of primitives; however, non-trivial programs using timeouts, fork-join parallelism and priority can be written in Orc. In this talk I will give an overview of the language and its operational semantics. I will also show useful programs that can be coded succinctly in Orc. Last, I will present the trace semantics of Orc.

Relevant Paper: A Language for Task Orchestration and its Semantic Properties David Kitchin, William R. Cook and Jayadev Misra Proc. of the International Conference on Concurrency Theory (CONCUR), 2006.

Upcoming Events:

# 5/2/07: Jesse Tov on Erlang # Don't you want to speak at pl-seminar?

--Mitch

NU Programming Languages Seminar Wednesday, 3/28/07 11:45am-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Structure shyness in the XML world

Ralf L�mmel, Microsoft Corp. Data Programmability Team

Abstract:

XML programming involves idioms for expressing "structure shyness" such as the descendant axis of XPath or the default templates of XSLT. We initiate a discussion of the relationships between such XML idioms and generic functional programming, while focusing on the (Haskell-based) "Scrap your boilerplate" style of generic programming (SYB). In particular: (i) we compare SYB style and XSLT style of programming; (ii) we approximate XPath in SYB; (iii) we illustrate the expressivity of SYB, when compared to a DSL like XPath; (iv) we explain SYB-style transformations as an alternative to destructive updates (a la XQuery); (v) we illustrate the use the Haskell type system for rejecting certain, trivial traversal behaviors; (vi) we popularize recent work by Cunha and Visser on an algebraic style of traversal optimization; (vii) on our way, we demo untyped and typed XML programming in LINQ / C# 3.0, thereby showing how more generic functional programming power may get into the mainstream.

Links to relevant papers: - POPL 2007: http://doi.acm.org/10.1145/1190215.1190240 - PLAN'X 2007: http://www.cs.vu.nl/~ralf/planx07/ - XML 2006: http://2006.xmlconference.org/programme/presentations/49.html - XML 2006: http://2006.xmlconference.org/programme/presentations/91.html

Bio of the speaker:

Dr. Ralf L�mmel is affiliated with Microsoft Corp. He serves on a research and development position with focus on XML technologies. In the years 2001--2004, Ralf L�mmel served on a permanent faculty position, at the Free University of Amsterdam, in the Software Engineering department, and he was also affiliated with the Dutch Center for Mathematics and Computer Science (CWI) -- starting in 1999. His research interests include program transformation, programming languages, generic language technology, grammarware engineering, and automated software engineering. Ralf L�mmel has published approximately 60 peer-reviewed papers on these subjects, and he has participated in numerous national and international collaborations and funded research projects on these subjects. In academic and industrial projects, Ralf L�mmel has designed, implemented, and deployed software development tools, migration tools and application generators. Ralf L�mmel received his PhD in computer science from the University of Rostock (Germany, 1999). Ralf L�mmel participates in various international conferences as program committee member and as organizer. For instance, he has recently (co-) organized a Dagstuhl seminar on program transformation, and an international summer school on generative and transformational techniques.

Upcoming Events:

# 4/25 Dimitris Vardoulakis on Orc # Don't you want to speak at pl-seminar?

--Mitch

NU Programming Languages Seminar Wednesday, 3/28/07 11:45am-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Structure shyness in the XML world

Ralf L�mmel, Microsoft Corp. Data Programmability Team

Abstract:

Bio of the speaker:

Upcoming Events:

# 4/25 Dimitris Vardoulakis on Orc # Don't you want to speak at pl-seminar?

--Mitch

NU Programming Languages Seminar Wednesday, 1/24/07 11:45am-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Debugging Backwards in Time Bil Lewis

What if a debugger could allow you to simply step BACKWARDS? Instead of all that hassle with guessing where to put breakpoints and the fear of typing "continue" one too many times... What if you could simply go backwards to see what went wrong?

This is the essence of the "Omniscient Debugger" -- it remembers everything that happened during the run of a program, and allows the programmer to "step backwards in time" to see what happened at any point of the program. All variable values, all objects, all method calls, all exceptions are recorded and the programmer can now look at anything that happened at any time.

In this talk, I will describe the design of the "ODB" -- an implementation of Omniscient Debugging for Java programs -- and discuss the various costs and trade-offs. The last half of the talk will be a demonstration of the ODB, showing how the various pieces of data are displayed and how the programmer can "navigate" through time to see what the program was doing, where values were set, when various threads ran, etc.

At the conclusion of the talk, the audience will be invited to use the ODB to find some actual bugs. Anyone having a laptop with Java on it can download the ODB (beforehand!) and try using it to find the bugs themselves.

================

The ODB is an experimental program under development. It is written in 100% pure Java and has been tested under Solaris, MacOS, and Windows. It is freely available at my web site: www.LambdaCS.com.

================

Bil Lewis is a computer scientist currently teaching at Tufts University. He has worked on natural language understanding, expert systems, language design, and programming tools. He studied at Ripon College, the University of Indiana, and Penn. He has taught at Stanford and for numerous companies. He has worked at Stanford Research Institute, the FMC AI Center, and Sun Microsystems. He wrote "GNU Emacs Lisp", the "Threads Primer", "Multithreaded Programming with PThreads", and "Multithreaded Programming with Java".

Upcoming Events:

# Don't you want to speak at pl-seminar?

--Mitch

NU Programming Languages Seminar Wednesday, 12/13/06 11:45am-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Pete Maniolos Georgia Tech

A Complete Compositional Reasoning Framework with Applications to Hardware Verification

Abstract: We present a complete compositional reasoning framework for verifying that a concrete system satisfies the same safety and liveness properties as its specification. Our framework consists of a powerful theory of refinement and a set of convenient, easily-applicable, and complete compositional proof rules. An important benefit of our approach over current methods is that the counterexamples generated tend to be much simpler, as bugs are isolated to a particular step in the composition proof.

We have applied our work to the problem of hardware verification. This is one of the major challenges currently facing the hardware industry, with recent estimates indicating that verification accounts for up to 70% of the total development costs for new products. We show that our framework greatly extends the applicability of decision procedures by automatically proving that complex pipelined machines defined at the RTL level and containing features such as out-of-order completion, branch prediction, caches, and deep pipelines refine their instruction set architectures.

This is joint work with Sudarshan Srinivasan.

Speaker Bio: Pete Manolios is an Assistant Professor in the College of Computing at the Georgia Institute of Technology. He is also an Adjunct Assistant Professor in the School of Electrical and Computer Engineering. He has a B.S. and an M.A. in Computer Science from Brooklyn College and a Ph.D. in Computer Sciences from the University of Texas at Austin.

Pete's primary research interest is formal verification. This includes developing algorithms, methodologies, concepts, and tools to formally and mechanically reason about both software and hardware systems. Pete is particularly interested in decision procedures, theorem proving, model checking, refinement, and abstraction. He also has broad interests in systems, software engineering, logic, computational biology, distributed computing, and pedagogy.

Upcoming Events:

# Wed 1/24 Bil Lewis, Omniscient Debugging

--Mitch

NU Programming Languages Seminar Wednesday, 12/06/06 11:45am-1:30pm Room 108 WVH (http://www.ccs.neu.edu/home/wand/directions.html) (* Note non-standard room *)

Richard P. Gabriel, PhD MFA Distinguished Engineer Sun Microsystems, Inc.

Design Beyond Human Abilities

For 50 years we've been developing a science and practice of software based on understandings and explorations of software systems of modest size-centering on systems of a few tens of thousands of lines of code but extending up to about 50 million lines. Scale makes a difference: scale of time and of size. The prospect of ultra large scale software systems-systems with perhaps trillions of lines of code encompassing millions of processors, ranging from sensors the size of dust to the largest servers, with much of it with real-time requirements-will change everything. Imagine, if you can, how such systems will be made. Can they truly be said to be designed at all? The realities of such systems will force us to re�examine the very foundations of computing and software engineering; our concepts of abstraction, modularity, information hiding, pure static typing, and many other things will need to be refined, expanded, or reformulated. Consider, further, that such systems in normal circumstances cannot be routinely re�nstalled nor globally rebooted, and when used in life- critical situations, they must not stop. Data must be readable and usable for decades, even as standards and hardware changes.

This talk will examine the nature of such systems, especially how they are designed, built, and what is needed to keep them running. We'll take both a philosophical and technical look at some of the aspects of ultra large scale software that make us need to revise our foundations and what those revisions will be like.

Biography: Richard P. Gabriel is a Distinguished Engineer at Sun Microsystems looking at the architecture, design, and implementation of extraordinarily large, self-sustaining systems. He is the award- winning author of four books and a poetry chapbook. He lives in California.

This talk is joint with the NU ACM Student Chapter.

Upcoming Events:

# Wed 12/13 Pete Manolios, A Complete Compositional Reasoning Framework with Applications to Hardware Verification # Wed 1/24 Bil Lewis, Omniscient Debugging

--Mitch

NU Programming Languages Seminar Wednesday, 11/29/06 11:45am-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Riccardo Pucella

The Semantics of Evidential Reasoning

Many scenarios in CS can be modeled as agents making decisions based on observations that help them decide between competing hypotheses. Observations can be seen as outcomes of simple experiments. Intuitively, observations may provide more evidence for some of the hypotheses than some others. This evidence can be quantified, and has a several pleasant properties.

In this talk, I want to focus on the general problem of deriving the evidence provided by observations when the experiment controlling the observations is more complex. Roughly, we can view an experiment as a program in a particular programming language, and devise an evidence-based semantics for experiments written in that programming language that associates with every observations in an experiment the evidence provided by those observations. I will explore the relationship between the resulting semantics and the classical semantics for probabilistic programs.

Upcoming Events:

# Wed 12/6 Dick Gabriel # Wed 12/13 Pete Manolios, A Complete Compositional Reasoning Framework with Applications to Hardware Verification # Wed 1/24 Bil Lewis, Omniscient Debugging

--Mitch

NU Programming Languages Seminar No seminar Wednesday, 11/22/06

Upcoming Events:

# Wed 11/29 Riccardo Puccella # Wed 12/6 Dick Gabriel # Wed 12/13 Pete Manolios, A Complete Compositional Reasoning Framework with Applications to Hardware Verification # Wed 1/24 Bil Lewis, Omniscient Debugging

--Mitch

NU Programming Languages Seminar Wednesday, 11/8/06 11:45-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Chet Murthy

Advanced Programming Languages in Enterprise Software: A lambda-calculus theorist wanders into an enterprise datacenter

Upcoming Events:

# Wed 11/29 Riccardo Puccella # Wed 12/6 Dick Gabriel # Wed 12/13 Pete Manolios

--Mitch

NU Programming Languages Seminar Wednesday, 10/25/06 11:45-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Will Clinger

The Java Memory Model: From Multithreading to Multicore

Nondeterministic concurrent computation is fundamental. Deterministic sequential computation is an increasingly rare special case, but compilers and hardware have conspired to preserve an increasingly desperate illusion of this special case. That illusion cannot be sustained. As usual, the worst damage was caused by the coverup.

Upcoming Events:

Open. Wouldn't you like to give a seminar??

--Mitch

**Oops, I meant Wed 10/18, not today. Sorry. --Mitch**

NU Programming Languages Seminar Wednesday, **10/18/06** 11:45-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Cormac Flanagan UC Santa Cruz

Hybrid Type Checking for Flexible Specifications

Software systems typically contain large APIs that are informally specified and hence easily misused. This talk describes the Sage programming language, which is designed to support and enforce precise yet flexible interface specifications. In additional to traditional static types, the Sage type system also supports first-class types and arbitrary refinement types. Sage enforces these specifications using a combination of static type checking, dynamic contract checking, automatic theorem proving, and a database of historical specification violations.

Upcoming Events:

10/25 Will Clinger: The Java Memory Model: From Multithreading to Multicore

--Mitch

NU Programming Languages Seminar Wednesday, 10/16/06 11:45-1:30pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Cormac Flanagan UC Santa Cruz

Hybrid Type Checking for Flexible Specifications

Upcoming Events:

10/25 Will Clinger: The Java Memory Model: From Multithreading to Multicore

--Mitch

** LAST REMINDER ** ** REGISTER BY WED, 9/6 IF YOU WANT A FREE LUNCH!!**

--Mitch

Friday, September 8 NU PRL Seminar Day Raytheon Ampitheatre

Program:

08:45 Andrew D. Gordon (Microsoft Research, Cambridge) Provable Implementations of Security Protocols 10:00 Hans Boehm (HP Labs) Towards a Memory Model for C++ 11:15 Dan Grossman (University of Washington, Seattle) The Why, What, and How of Software Transactions for More Reliable Concurrency 12:15 LUNCH

The College of Computer Science will provide lunch for registered participants. 01:30 Carolyn Talcott (SRI International) Pathway Logic: Application of Formal Modeling Techniques to Understanding Biological Signaling Processes 03:00 Scott Smith (Johns Hopkins University) A Microkernel Virtual Machine: Building Security with Clear Interfaces

Registration:

Please register via email with Rachel Kalwait (rachelb@ccs.neu.edu) by September 6.

Location:

The seminar will take place in the Raytheon Theater of Egan Hall, located next to Ruggles Station on the ORANGE and Commuter Lines and about a long block from the Northeastern University stop on the GREEN E Line. Look for building 60 on the campus map (http://www.campusmap.neu.edu/).

Abstracts, etc., at http://www.ccs.neu.edu/home/matthias/Tmp/seminar.html

Friday, September 8 NU PRL Seminar Day Raytheon Ampitheatre

Program:

Registration:

Please register via email with Rachel Kalwait (rachelb@ccs.neu.edu) by September 6.

Location:

Abstracts, etc., at http://www.ccs.neu.edu/home/matthias/Tmp/seminar.html

UPCOMING SPECIAL EVENT -- SAVE THE DATE

Friday, September 8 Pre-POPL Workshop Day

On Friday, September 8, we will hold a pre-POPL-PC-meeting workshop day with talks by

Andrew Gordon Scott Smith Carolyn Talcott Hans Boehm Dan Grossman

Titles, abstracts, and schedule to be posted later.

NU Programming Languages Seminar Tuesday 8/8/06 11:45-1:30 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Experimenting with Formal Languages using Forlan

Alley Stoughton Kansas State University

Since the 1930s, the subject of formal language theory, also known as automata theory, has been developed by computer scientists, linguists and mathematicians. Because of its many applications to computer science, most CS programs offer both undergraduate and graduate courses in this subject. Many of the results of formal language theory are proved constructively, using algorithms that are useful in practice. In typical courses on formal language theory, students apply these algorithms to toy examples by hand, and learn how they are used in applications. But they are not able to experiment with them on a larger scale.

Over the past several years, I have been designing and developing a computer toolset, called Forlan, for experimenting with formal languages. Forlan is implemented in the functional programming language Standard ML, a language whose notation and concepts are similar to those of mathematics. Forlan is used interactively; in fact, a Forlan session is simply a Standard ML session in which the Forlan modules are pre-loaded. Users are able to extend Forlan by defining ML functions.

In Forlan, the usual objects of formal language theory -- automata, regular expressions, grammars, labeled paths, parse trees, etc. -- are defined as abstract types, and have concrete syntax. The standard algorithms of formal language theory are implemented in Forlan, including conversions between different kinds of automata and grammars, the usual operations on automata and grammars, equivalence testing and minimization of DFAs, etc.

In my talk, I will give a brief introduction to formal language theory, and will then give an extended example of how one can experiment with formal languages using Forlan.

Forlan is an open source project; it may be downloaded from

http://www.cis.ksu.edu/~stough/forlan/

More information concerning Forlan, including a draft (open source) textbook on formal language theory, can be found on this WWW site.

NU Programming Languages Seminar Tuesday 7/25/06 11:45-1:30 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Waitomo, an Interface-Oriented Programming Language Peter Thiemann Universit�t Freiburg

Waitomo is an experimental programming language derived from Java. It aims to strengthen the guarantees of type safety by eliminating the need for casting without sacrificing the flexibility of the object-oriented programming style. The vital ingredients of the language are generics combined with a new approach to interfaces that includes a notion of self-types and union types. Waitomo interfaces are not types, but rather constraints which can be imposed on generics. This choice enables elegant solutions to standard programming problems.

Besides an introduction to the language, the paper contains the full formalization of a core language with proofs of type soundness and decidability of subtyping. A prototype implementation of the language exists.

NU Programming Languages Seminar Wednesday, 6/7/06 11:45-1:30 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Programming Ad-hoc Networks of Mobile Devices Ulrich Kremer Rutgers University

Abstract:

Ad-hoc networks of mobile devices such as smart phones and PDAs represent a new and exciting distributed system architecture. Building distributed applications on such an architecture poses new design challenges in programming models, languages, compilers, and runtime systems.

This talk will introduce SpatialViews, a high-level language designed for programming mobile devices connected through a wireless ad-hoc network. SpatialViews allows specification of virtual networks with nodes providing desired services and residing in interesting spaces. These nodes are discovered dynamically with user-specified time constraints and quality of result (QoR). The programming model supports ``best-effort'' semantics, i.e., different executions of the same program may result in ``correct'' answers of different quality. It is the responsibility of the compiler and runtime system to produce a high-quality answer for the particular network and resource conditions encountered during program execution. Example applications will be used to illustrate the different features of the SpatialViews language, and to demonstrate the expressiveness of the language and the efficiency of the compiler generated code. Sample applications include sensor network applications that collect and aggregate sensor data within the network, applications that use dynamic service installation and computation offloading, and augmented-reality gaming. A simulation environment allows the execution of SpatialViews programs under different simulated physical conditions. More information about the language, compiler and runtime system, including a distribution of our prototype system, can be found at http://www.cs.rutgers.edu/spatialviews .

NU Programming Languages Seminar Wednesday, 5/17/06 11:45-1:30 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Modular Static Analysis with Sets and Relations

Viktor Kuncak MIT CSAIL

ABSTRACT:

We present a new approach for statically analyzing data structure consistency properties. Our approach is based on specifying interfaces of data structures using abstract sets and relations. This enables our system to independently verify that

1) each data structure satisfies internal consistency properties and each data structure operation conforms to its interface;

2) the application uses each data structure interface correctly, and maintains the desired global consistency properties that cut across multiple data structures.

Our system verifies these properties by combining static analyses, constraint solving algorithms, and theorem provers, promising an unprecedented combination of precision and scalability. The combination of different techniques is possible because all system components use a common specification language based on sets and relations.

In the context of our system, we developed new algorithms for computing loop invariants, new techniques for reasoning about sets and their sizes, and new approaches for extending the applicability of existing reasoning techniques. We successfully used our system to verify data structure consistency properties of examples based on computer games, web servers, and numerical simulations. We have verified implementations and uses of data structures such as linked lists with back pointers and iterators, trees with parent pointers, two-level skip lists, array-based data structures, as well as combinations of these data structures. This talk presents our experience in developing the system and using the system to build verified software.

ABOUT THE SPEAKER: Viktor Kuncak is a Ph.D. candidate in the MIT Computer Science and Artificial Intelligence Lab. His interests include program analysis and verification, formal methods, programming languages, and software engineering.

NU Programming Languages Seminar Wednesday, 2/15/06 12:30-1:45 pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Declarative Process Models for ERP and Workflow Systems

Christian Stefansen DIKU University of Copenhagen, Denmark

Abstract:

This talk sketches some recent research toward a declarative process-based framework for ERP systems. In particular, the talk describes the following two areas:

1. A declarative language for compositional specification of commercial contracts governing the exchange of economic resources. The language extends Eber and Peyton Jones's declarative language for specifying financial contracts to the exchange of money, goods and services amongst multiple parties, and it complements McCarthy's Resources, Events and Agents (REA) accounting model with a view-independent formal contract model that supports definition of user-defined contracts, automatic monitoring under execution, and user-definable analysis of their state before, during and after execution.

2. A pi-calculus encoding of common workflow control patterns, which leads to a pi-calculus-based macro language for workflow specification. The encodings presented here demonstrate some of the strengths and weaknesses of pi-calculus for business process formalization vis a vis Petri nets and concrete languages such as BPEL and YAWL.

This is work in progress.

http://www.stefansen.dk

NU Programming Languages Seminar Wednesday, 1/18/06 11:45-1:30 pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Aleksandar Nanevski Harvard University

A Modal Approach to Functional Programming

Abstract:

It is becoming increasingly important today to execute programs in very complex run-time environments. Modern programs are often required to run in parallel, be mobile, use distributed data, accommodate dynamically to changing run-time conditions.

When approaching hard programming problems, a language-enforced programming discipline is crucial, and a natural way to enforce it is through the type mechanism of functional languages. Types express assumptions and guarantees required of program expressions, and usually correspond to propositions in some logic. The compiler checks if the program matches its type, thereby aiding the debugging process.

Unfortunately, most type systems of today only ensure that functions are invoked with matching arguments, and usually ignore how programs interact with their environments. For example, when programs interact with memory, it is usually possible and desirable to execute a number of memory reads out of order, while the memory writes must typically be serialized. This distinction between reads and writes should be encoded in the type system.

The natural question then becomes: which logic captures the relevant properties of run-time environments, and thus may serve as a foundation for languages of the future? In this talk, I will describe a language based on a version of modal logic, and illustrate how it structures the interaction between programs and environments. In the examples I consider, programs interact with memory (giving rise to a calculus for destructive and non-destructive state update), with the control stack (calculus of exceptions), and with the syntactic representation of program contexts (calculus for run-time code generation and meta programming).

NU Programming Languages Seminar Wednesday, 11/30/05 11:45-1:30 pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Type-systems for Region-based Memory Management

Matthew Fluet Harvard University

Region-based memory management offers a healthy compromise in tuning a program's memory usage; by reclaiming groups of related objects wholesale, region-based languages may avoid both the inefficiency of garbage collectors and the tedium of malloc/free. Type systems for region-based languages further enhance their utility by statically catching (possibly) erroneous use of the region primitives. In this talk, we'll look at three "flavors" of type systems for region-based languages: * a type-and-effect system (a la Tofte-Talpin) * a monadic type system * a sub-structural type system Our goal is to demonstrate that we may successively encode the type-and-effect system into the monadic type system and monadic type system into the sub-structural type system.

The essence of the first encoding is to translate effects to an indexed monad, inspired by (and generalizing) the ST monad of Launchbury and Peyton Jones. The upshot of this translation is that we are able to trade the subtleties of an effect system for the simplicity of a monadic system, where plain old parametric polymorphism (a la System F) provides sufficient encapsulation.

However, both the type-and-effect system and the monadic type system rquire that regions have last-in-first-out (LIFO) lifetimes following the block structure of the language. This places sever restrictions on when objects may be effectively reclaimed and many natural programs may give rise to (unbounded) leaks when compard to a garbage collected implementation. Hence, we introduce a sub-structural type system that eliminates the LIFO restriction. The key idea is to separate the lifetime of a region from the scope of the region's name, by providing explicit region creation and destruction primitives.

The essence of the second encoding, then, is to "break open" the monad and reveal it's store passing implementation. Furthermore, the sub-structural type system allows us to faithfully encode even more advanced features, such as Cyclone's dynamic regions and unique pointers.

NU Programming Languages Seminar Wednesday, 11/9/05 1:45-3:00 pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

The Fortress Programming Language

Sam Tobin-Hochstadt Northeastern University

Fortress is a next-generation language for High Performance computing. But it's also a language with new ideas of relevance to the broader PL community. This talk will give a PL researcher's overview of Fortress, and talk about three ways in which it is attempting radical innovation: in the syntax, the type system, and the component system.

NU Programming Languages Seminar Wednesday, 10/26/05 1:45-3:00 pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

The Scala Experiment -- Can We Provide Better Language Support for Component Systems?

Martin Odersky EPFL

True component systems have been an elusive goal of the software industry. Ideally, software should be assembled from libraries of pre-written components, just as hardware is assembled from pre-fabricated chips. In reality, large parts of software applications are written ``from scratch'', so that software production is still more a craft than an industry.

Components in this sense are simply program parts which are used in some way by larger parts or whole applications. Components can take many forms; they can be modules, classes, libraries, frameworks, processes, or web services. Their size might range from a couple of lines to hundreds of thousands of lines. They might be linked with other components by a variety of mechanisms, such as aggregation, parameterization, inheritance, remote invocation, or message passing.

At least to some extent, the lack of progress in component software is due to shortcomings in the programming languages used to define and integrate components. Most existing languages offer only limited support for component abstraction and composition. This holds in particular for statically typed languages such as Java and C\# in which much of today's component software is written.

In our work on Scala, we have tried to rethink abstraction mechanisms for components from the ground up. We have identified three programming language abstractions for the construction of reusable components: abstract type members, explicit selftypes, and modular mixin composition. Together, these abstractions enable us to transform an arbitrary assembly of static program parts with hard references between them into a system of reusable components. The transformation maintains the structure of the original system.

In this talk, I give an introduction to Scala and demonstrate how it helps solving some hard problems in the construction of component systems.

NU Programming Languages Seminar Monday 10/17/05 2:00-4:00pm Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

The Meaning of Multilanguage Programs

Jacob Matthews University of Chicago, Chicago

Monday, October 17, 2005

Software developers have long understood that real applications are built out of components in different languages and connected using a variety of different strategies. For example, foreign function interface systems like SWIG connect high-level languages to low-level languages; component frameworks like COM and; CORBA connect high-level languages to; each other; and domain-specific languages such as Yacc are embedded into their host languages in such a away that control and data flow back and forth between the programs.

In this talk I will present a general technique for modelling the operational semantics of multilanguage systems such as these. The technique is simple and general, and surprisingly connects traditional multilanguage systems to seemingly unrelated concepts such as contracts.

Joint work with Robert B. Findler

[Mail archives | Old Schedules]