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 presents two talks by

Erich Neuwirth Didactic Center for Computer Science and Institute for Scientific Computing University of Vienna

Wednesday, August 12, 2009 Both talks in Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

11:45-1:30:

Music as a paradigm for teaching Computer Science abstractions

Creating and performing music has a lot of structural implications. The base unit to deal with is a musical phrase. Combining phrases creates melodies. Playing a melody as a canon can be seen as combining shifted copies of one melody. Transposing can easily be seen as an arithmetic operation on pitch, and many more musical operations can easily be mapped into functions applied to phrases. So the concept of a musical phrase seen as an abstract data type can be seen as fundamental when working with music on a computer. We will see a toolkit for creating, and transforming musical phrases and combining them into larger pieces of music. Performing polyphonic music also has an important computer science model: synchronizing parallel processes.

The toolkit has two different mini languages. The beginners version is implemented in a spreadsheet, so the user always can see the data and perform transformations manually. The more advanced version in implemented in Logo.

3:00-4:00:

Design of a Spreadsheet/R Interface

RExccel is an add-in to Excel that allows the use of R as a "helper application" for Excel. Data can be transferred between Excel and R (in both directions), and Excel can call R functions to perform calculations and then transfer the results to Excel. RExcel allows the use of R functions in Excel cell formulas, effectively controlling R calculations from Excel's automatic recalculation mechanism. It also allows the creation of a standalone RExcel application which hides R almost completely from the user and uses Excal as the main interface to R.

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

Upcoming Events:

# Nothing scheduled :-( Wouldn't you like to give a talk?

--Mitch

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

The script-writer's dream: How to write great SQL in your own language and be sure it will succeed.

Ezra Cooper University of Edinburgh

Language-integrated query is a new way of interfacing to databases that expresses queries using natural iteration constructs in a general-purpose programming language; the compiler then generates SQL to execute these expressions. The result is a safer and more flexible way to query databases.

This talk shows how to translate these general expressions into SQL, even when they take advantage of linguistic mechanisms not present in SQL. We can handle nested intermediate data structures and functional abstraction. In fact, any expression with an appropriate type that doesn't make use of non-SQL primitives can be translated. A straightforward type-and-effect system tells us at compile time whether a given expression will translate. Thus, unlike in Hollywood where a script-writer can never be sure a movie sequel will be popular, we show how to be sure that your SQL---written in your own language---will succeed (in being translated).

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

Upcoming Events:

# Nothing scheduled :-( Wouldn't you like to give a talk?

--Mitch

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

Automatic Differentiation of Functional Programs and its use for Probabilistic Programming

Jeffrey Mark Siskind School of Electrical and Computer Engineering Purdue University

It is extremely useful to be able to take derivatives of functions expressed as computer programs to support function optimization and approximation, parameter estimation, machine learning, and ultimately computational science and engineering design. The established discipline of Automatic Differentiation (AD) has largely focussed on imperative languages, where it is most efficiently implemented as a source-to-source transformation performed by a preprocessor. This talk will present a novel formulation of AD for functional programs expressed in the lambda calculus. A key novel aspect of our formulation is that AD is performed by higher-order functions that reflectively transform closure bodies. Our methods exhibit an important closure property that prior AD formulations lack: the ability to transform the entire space of input programs, including those produced by the AD transformations themselves. This is crucial for solving the kinds of nested optimizations that arise in domains such as game theory and automatic control. Furthermore, since the input and output of our transformations is the lambda calculus, efficient implementation is facilitated by novel extensions of standard compilation techniques. We exhibit a novel "almost" union-free polyvariant flow-analysis algorithm, formulated as abstract interpretation, that partially evaluates calls to the AD operators, migrating reflective source-to-source transformation to compile time. This yields code with run-time performance that exceeds the best existing AD implementations for imperative languages by a factor of two and outperforms all AD implementations for functional languages by two to three orders of magnitude.

AD has traditionally been applied to purely numeric programs written in imperative languages like Fortran. Our novel methods can be applied to mixed symbolic-numeric programs written in functional languages. This is useful for developing complex stochastic models such as is done in the emerging field of probabilistic programming. We demonstrate how our methods support this enterprise by constructing evaluators for two different probabilistic programming languages, one based on Scheme and one based on Prolog, and using both forward-mode and reverse-mode variants of our AD methods to take the gradients of such evaluators executing probabilistic programs in their respective target languages in order to perform gradient-based maximum-likelihood estimation of the distribution parameters of the free random variables in those programs. We demonstrate that for this domain our methods yield performance that exceeds straightforward implementation of AD in functional languages by many orders of magnitude.

Joint work with Barak A. Pearlmutter

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

Upcoming Events:

# Nothing scheduled :-( Wouldn't you like to give a talk?

--Mitch

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

Unit Tests in Java Viera Proulx (joint work with Weston Jossey)

The design of unit test consists of three separate but collaborating components. First, the programmer designs the test cases by defining the needed data, method invocations, and expected outcomes. To evaluate the tests, the programmer needs to define how the expected and actual value should be compared, i.e. what constitutes the successful outcome of the test and what constitutes a failure. Finally, there needs to be a program that evaluates all tests and reports the outcomes in a manner that helps the programmer identify the source of the problem.

The most popular testing software in Java, JUnit, provides only a limited support for unit test design and evaluation. The task of comparing the expected and actual values is left entirely to the individual programmer.

This talk presents a user-friendly and novice-appropriate library that provides unit testing in Java. The library uses the java reflection support to generate automatically the equality comparison of arbitrary two objects, comparing the values of the individual fields. The user specifies only the actual and expected objects to be compared. The test report includes a pretty-printed display of all fields for both the actual and expected data, and a link to the location of the failed test.

The tester library has been used successfully by hundreds of students at several institutions and is used daily in all of our Java programming tasks.

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

Upcoming Events:

# Nothing scheduled :-( Wouldn't you like to give a talk?

--Mitch

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

Unit Tests in Java Viera Proulx (joint work with Weston Jossey)

The tester library has been used successfully by hundreds of students at several institutions and is used daily in all of our Java programming tasks.

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

Upcoming Events:

# Nothing scheduled :-( Wouldn't you like to give a talk?

--Mitch

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

Bounded-Latency Generational Garbage Collection

Will Clinger and Felix Klock

Abstract:

Generational garbage collectors offer good throughput on typical programs, but most generational collectors perform occasional full collections, which do not scale well; even on 32-bit machines, a full collection can last several seconds.

Real-time collectors may scale well, but sacrifice throughput. Furthermore some real-time collectors assume a well-behaved program, and have unknown or poor worst-case performance.

We have designed and prototyped a new algorithm that offers a compromise between real-time and generational collection. In this talk, we show that the algorithm is scalable by proving theoretical worst-case bounds for space, gc latency, and minimum mutator utilization.

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

Upcoming Events:

# Nothing scheduled :-( Wouldn't you like to give a talk?

--Mitch

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

Adam Chlipala Harvard University

Liberating Semi-Automated PL Proofs from Binder Bookkeeping

Abstract:

The advantages of machine-checked proofs about programming languages have been clear for decades now, and the POPLmark Challenge has helped get more PL researchers started building such formal proofs. Unfortunately, almost everyone not doing research in proof assistants finds the state-of-the-art extremely cumbersome. The most popular encoding schemes for general-purpose proof assistants like Coq and Isabelle/HOL involve so much bookkeeping about variables that such "obvious" theorems usually make up a majority of a formal development. Systems like Twelf enable the use of higher-order abstract syntax, but they require that every step of every proof be written out manually in complete detail, and they are intrinsically less well-suited to verification of functional programs and to theorem-proving about domains beyond syntactic metatheory.

In this talk, I will present a way of getting (most of) the best of both worlds, via parametric higher-order abstract syntax. This technique makes it possible to define syntax tree datatypes so that every well-typed AST is well-formed, by construction, in contrast to the more standard Coq and Isabelle methodologies. Moreover, it is easy to write functions, like compiler transformations, whose types guarantee that they manipulate syntax correctly. We can build mostly-automated correctness proofs of such transformations without ever once mentioning syntactic substitution, the subject of the bulk of proof effort with previous techniques.

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

Upcoming Events:

# Nothing scheduled :-( Wouldn't you like to give a talk?

--Mitch

NU Programming Languages Seminar Wednesday, February 11, 2009 (* I THINK I'VE GOT THE DATE RIGHT NOW... *) 11:45-1:30 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Ranjit Jhala University of California, San Diego

Liquid Types

We present Logically Qualified Data Types, abbreviated to Liquid Types, a new static program verification technique which combines the complementary strengths of automated deduction (SMT solvers), model checking (Predicate Abstraction), and type systems (Hindley-Milner inference). We have implemented the technique in a tool that infers liquid types for Ocaml programs. To demonstrate the utility of our approach, we show how liquid types reduce, by more than an order of magnitude, the manual annotations required to statically verify (1) the safety of array accesses on a diverse set of benchmarks, and (2) invariants like sortedness, balancedness, binary-search-ordering, variable ordering, set-implementation, heap-implementation, and acyclicity of data structure libraries for list-sorting, union-find, splay trees, AVL trees, red-black trees, heaps, associative maps, extensible vectors, and binary decision diagrams. (Joint work with Patrick Rondon and Ming Kawaguchi)

Ranjit Jhala is an Assistant Professor in the Department of Computer Science and Engineering at UC San Diego. Before joining UCSD, he was a graduate student at UC Berkeley. Ranjit is interested in Programming Languages and Software Engineering, more specifically, in techniques for building reliable computer systems. His work draws from, combines and contributes to methods the areas of Model Checking, Program Analysis and Automated Deduction.

Host: Pete Manolios

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

Upcoming Events:

# 2/18 Adam Chlipala, Liberating Semi-Automated PL Proofs from Binder Bookkeeping

Wouldn't you like to give a talk?

--Mitch

NU Programming Languages Seminar **OOPS, THIS TIME LET'S GET THE DATE RIGHT** Wednesday, February 4, 2009 11:45-1:30 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Ranjit Jhala University of California, San Diego

Liquid Types

Host: Pete Manolios

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

Upcoming Events:

# 2/11 Adam Chlipala, Mechanized Semantics with Definitional Compilers

Wouldn't you like to give a talk?

--Mitch

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

Ranjit Jhala University of California, San Diego

Liquid Types

Host: Pete Manolios

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

Upcoming Events:

# 2/11 Adam Chlipala, Mechanized Semantics with Definitional Compilers

Wouldn't you like to give a talk?

--Mitch

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

Derek Dreyer Max Planck Institute for Software Systems (MPI-SWS)

Mixin' Up the ML Module System

Abstract:

ML modules provide hierarchical namespace management, as well as fine-grained control over the propagation of type information, but they do not allow modules to be broken up into mutually recursive, separately compilable components. Mixin modules facilitate recursive linking of separately compiled components, but they are not hierarchically composable and typically do not support type abstraction. We synthesize the complementary advantages of these two mechanisms in a novel module system design we call MixML.

A MixML module is like an ML structure in which some of the components are specified but not defined. In other words, it unifies the ML structure and signature languages into one. MixML seamlessly integrates hierarchical composition, translucent ML-style data abstraction, and mixin-style recursive linking. Moreover, the design of MixML is clean and minimalist; it emphasizes how all the salient, semantically interesting features of the ML module system (as well as several proposed extensions to it) can be understood simply as stylized uses of a small set of orthogonal underlying constructs, with mixin composition playing a central role.

This is joint work with Andreas Rossberg.

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

Upcoming Events:

# 2/4 Ranjit Jhala (UCSD) # 2/25 Christian Skalka (Univ. of VT)

Who else would like to give a talk?

--Mitch

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

Geoffrey Mainland Harvard University

Flask: Staged Functional Programming for Sensor Networks

Severely resource-constrained devices present a confounding challenge to the functional programmer: we are used to having powerful abstraction facilities at our fingertips, but how can we make use of these tools on a device with an 8- or 16-bit CPU and at most tens of kilobytes of RAM? Motivated by this challenge, we have developed Flask, a domain specific language embedded in Haskell that brings the power of functional programming to sensor networks. Flask consists of a staging mechanism that cleanly separates node-level code from the meta-language used to generate node-level code fragments; syntactic support for embedding standard sensor network code; a restricted subset of Haskell that runs on sensor networks and constrains program space and time consumption; a higher-level "data stream" combinator library for quickly constructing sensor network programs; and an extensible runtime that provides commonly-used services. Through microbenchmarks and measurements on physical hardware, we demonstrate that Flask produces programs that are efficient in terms of CPU and memory usage and that can run effectively on existing sensor network hardware.

The full paper is available at http://www.eecs.harvard.edu/~mainland/flask/.

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

Upcoming Events:

# No talks scheduled past these. Come give a talk!

--Mitch

NU Programming Languages Seminar Tuesday, November 11, 2008 **NOTE NON-STANDARD DAY** 11:45-1:30 Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Marco Carbone Queen Mary's University, London

Communication-Centred Programming with Session Types

In this talk, I shall introduce two different paradigms of descriptions of communication behaviour, one focussing on global message flows and another on end-point behaviours, using formal calculi based on session types. The global calculus, which originates from a web service description language (W3C WS-CDL), describes an interaction scenario from a vantage viewpoint; the end-point calculus, an applied typed pi-calculus, precisely identifies a local behaviour of each participant. We explore a theory of end-point projection, by which we can map a global description to its end-point counterpart preserving types and dynamics. Three principles of well-structured description and the type structures play a fundamental role in the theory.

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

Upcoming Events:

# Wed 11/12 no seminar # Wed 11/19 Geoffrey Mainland (Harvard): Flask: Functional Programming for sensor networks (tentative)

# No talks scheduled past these. Come give a talk!

--Mitch

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

RCF, Refinement Types, and the State Monad

Riccardo Pucella NU PRL

Abstract:

RCF [Bengtson, Bhargavan, Fournet, Gordon, and Maffeis, 2008] is a concurrent lambda-calculus equipped with refinement types for expressing pre- and post-conditions within first-order logic. The values of a refinement type {x:T | C} are the values of the type T that satisfy the formula C. Refinement types are a way of unifying type systems with program logics. The goal of RCF is to verify security properties of the source code of cryptographic protocols and access control mechanisms. Well-typed programs enjoy assertion-based security properties, with respect to a realistic threat model including key compromise. But RCF is a calculus that is useful beyond its ability to establish security properties.

I will spend most of the talk reviewing RCF and talking about refinement types. I will also describe work that Andy Gordon and I started this summer on using RCF as a basis for capturing stateful type systems. As an example, I will consider the problem of typechecking stateful (role-based) access control properties, where the set of permissions of the code depends on the roles that are active at runtime.

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

Upcoming Events:

# Wed 11/12 no seminar # Wed 11/19 Geoffrey Mainland (Harvard): Flask: Functional Programming for sensor networks (tentative)

# No talks scheduled past these. Come give a talk!

--Mitch

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

Aaron Turon NU PRL

Spec# and Boogie

The Spec#/Boogie tools are a Microsoft-backed foray into lightweight software verification. The aim of the project is similar in spirit to "extended static checking": go beyond (decidable) type systems to do more sophisticated, behavioral analysis of code, but stop short of performing full verification. A working hypothesis is that there is a lucrative middle ground between the virtually free structural checks provided by type checkers, and high-cost verification. Although the Spec#/Boogie analysis requires a theorem prover, the system is fully automated, and programmers interact with the analysis through compiler errors that refer to specific code locations and specification failures.

Unlike ESC/Java, the Spec#/Boogie stack provides a sound program analysis.

The project is broken into two modular components, Spec# and Boogie. Spec# is an extension of the C# language with nonnull types, method contracts, object invariants, and an ownership model of the heap. Used in isolation, Spec# compiles annotated code to MSIL bytecode with dynamic checks. Boogie, on the other hand, is an intermediate language for verification, similar to Dijkstra's language of guarded commands. The Boogie tool infers loop invariants and generates verification conditions from a Boogie program. Boogie can be used (soundly) as a back-end for the Spec# compiler; if the resulting analysis succeeds, then no dynamic check in the compiled program will ever fail.

I will discuss the most important features of both Spec# and Boogie in detail, and also demonstrate how the tools are used together.

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

Upcoming Events:

# Wed 11/5 Riccardo Pucella: Stateful RCF # Wed 11/12 no seminar # Wed 11/19 Geoffrey Mainland (Harvard): Flask: Functional Programming for sensor networks (tentative)

--Mitch

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

Amal Ahmed TTI-Chicago

All for Nothing: Gradual Typing with Polymorphism and Blame

Static and dynamic typing offer complementary advantages: static typing provides early error detection, efficient execution, and better documentation of code, whereas dynamic typing encourages rapid development and makes it easier to adapt to changing requirements. As a result, they each have their adherents, but recently interest has emerged in a 'third way' that combines the best of both worlds.

In this talk, I will present a language that integrates statically typed and dynamically typed components, similar to the gradual types of Siek and Taha (2006), and show how to extend it to incorporate parametric polymorphism. This language, dubbed the polymorphic blame calculus, is a core calculus of casts between more and less precise types. Our system includes a notion of blame (as found in contracts), which allows us to show that when more-typed and less-typed portions of a program interact, that any type failures are due to the less-typed portion.

Values of polymorphic type satisfy a strong semantic property known as relational parametricity. Our system permits a dynamically typed value to be cast to a polymorphic type, with the type enforced by dynamic sealing. We have shown that this method of enforcement is so strong as to ensure relational parametricity.

(Joint work with Robby Findler, Jacob Matthews, and Philip Wadler)

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

Amal will be with us all day on Wed 10/22. If you'd like to talk to her, let me know and we'll work out a schedule.

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

Upcoming Events:

# Wed 10/29 Aaron Turon: Spec# and Boogie # Wed 11/5 Riccardo Pucella: Stateful RCF # Wed 11/12 no seminar # Wed 11/19 Geoffrey Mainland (Harvard): Flask: Functional Programming for sensor networks (tentative)

--Mitch

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

Olivier Danvy Department of Computer Science, University of Aarhus, Denmark

A call-by-name normalization function for the simply typed lambda-calculus with sums and products

Abstract:

We report on the first call-by-name normalization function for the simply typed lambda-calculus with sums and products that is purely functional (no `gensym' and no control operators as well as no pre-computed state) and that passes the Filinski test. We present two definitions: one is typeless and we wrote it in Scheme as well as in ML with a universal type of values; the other is typeful and we formalized it in ML, using the type inferencer as a logical framework.

Our solution to this open problem is remarkably simple: we use an ordinary evaluation function towards a call-by-name domain of continuation-passing values; and we invert it by instantiating the domain of answers with a continuation-based code generating function towards long beta-eta-normal forms using de Bruijn levels. The resulting normalization function is thus lightweight and it operates at native speed. For all we can see, it also lends itself gracefully to validating extra equations over normal forms.

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

Olivier will be with us all day on Wed 8/6. If you'd like to talk to Olivier, let me know and we'll work out a schedule.

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

Upcoming Events:

No events scheduled. Come give a talk!

--Mitch

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

Olivier Danvy Department of Computer Science, University of Aarhus, Denmark

A call-by-name normalization function for the simply typed lambda-calculus with sums and products

Abstract:

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

Olivier will be with us all day on Wed 8/6. If you'd like to talk to Olivier, let me know and we'll work out a (possibly wiki-based) schedule.

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

Upcoming Events:

No events scheduled. Come give a talk!

--Mitch

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]