NU Programming Languages Seminar Wednesday, June 30, 2004 Room 366 West Village H (http://www.ccs.neu.edu/home/wand/directions.html) 1:30-3:00
Kanren: A declarative logic programming system
Oleg Kiselyov, FNMOC
Kanren is a declarative logic programming system with first-class relations embedded in a pure functional subset of Scheme. The system has true unions, fair scheduling, lexically-scoped logical variables, set-theoretical semantics, and high performance without cuts. The talk will present the main ideas of Kanren and focus on the proof of the mirror theorem, which may be stated (in pseudocode, not Kanren!) as:
if (mirror nil) = nil (mirror (cons a d)) = (cons (mirror d) (mirror a)) then (mirror (mirror l)) = l
NU Programming Languages Seminar Wednesday, May 26, 2004 Room 366 West Village H (http://www.ccs.neu.edu/home/wand/directions.html) 1145-145. Bring your lunch.
Garbage-First Garbage Collection
Tony Printezis, Java Technology Group, SunLabs East
Garbage-First is a high-throughput concurrent and parallel garbage collector, targeted for server applications with large memory heaps, running on large multi-processors. It is designed to meet a user-defined soft real-time goal with a high degree of probability.
Garbage-First uses a single physical heap which is divided into fixed size regions. Global mostly-concurrent marking provides collection completeness and identifies heap regions ripe for reclamation via compacting evacuation. The absence of fine-grain free lists eliminates any potential fragmentation problems.
Garbage-First uses two techniques to try to meet the given soft real-time goal. First, it attempts to meet a pause time goal by using global liveness information and other easily-obtainable metrics to predict the cost of evacuation of a set of heap regions. Second, it attempts to schedule all stop-world pauses so that they do not violate the given soft real-time goal.
Experimental results show that Garbage-First achieves throughput comparable, within 5%, to that of a production-quality widely-used mostly-concurrent collector, while it performs considerably better in meeting the given soft real-time goal.
NU Programming Languages Seminar Wednesday, March 24, 2004 306 Egan Hall, Northeastern University (building 60 on http://www.campusmap.neu.edu/) 1145-145. Bring your lunch.
Writing Compiler Optimizations Using Fold and Build
Kenichi Asai
Simple compiler optimizations are typically represented as syntax-directed rules that show how to transform each syntax constructor. In this talk, I push it further to write compiler optimizations using the general constructor-substitution functions, fold and build. By writing optimizations using fold and build, it becomes possible to fuse multiple optimizations that go over the abstract syntax tree (AST) into one optimization that goes over the AST only once.
Joint work with Mayumi Sasaki.
NU Programming Languages Seminar Wednesday, March 10, 2004 306 Egan Hall, Northeastern University (building 60 on http://www.campusmap.neu.edu/) 1145-145. Bring your lunch.
Joshua Guttman
Mitre Corporation
Information Flow Goals in Security-Enhanced Linux
In this paper, we present a systematic way to determine the information flow security goals achieved by systems running a secure O/S, specifically systems running Security-Enhanced Linux. A formalization of the access control mechanism of the SELinux security server, together with a labeled transition system representing an SELinux configuration, provides our framework. Information flow security goal statements expressed in linear temporal logic provide a clear description of the objectives that SELinux is intended to achieve. We use model checking to determine whether security goals hold in a given system. These formal models combined with appropriate algorithms have led to automated tools for the verification of security properties in an SELinux system. Our approach has been used in other security management contexts over the past decade, under the name rigorous automated security management.
(Workshop on Issues in the Theory of Security, April '03, and Journal of Computer Security, Forthcoming.)
Joint work with Amy L. Herzog and John D. Ramsdell .
NU Programming Languages Seminar Wednesday, February 18, 2004 306 Egan Hall, Northeastern University (building 60 on http://www.campusmap.neu.edu/) 1145-145. Bring your lunch.
Greg Pettyjohn
Modeling Web Interactions
Abstract: Programmers confront a minefield when they design interactive Web programs. Web interactions take place via Web browsers. With browsers, consumers can whimsically navigate among the various stages of a dialog and can thus confuse the most sophisticated corporate Web sites. In turn, Web services can fault in frustrating and inexplicable ways. The quickening transition from Web scripts to Web services lends these problems immediacy. To address this programming problem, we develop a foundational model of Web interactions and use it to formally describe two classes of errors. The model suggests techniques for detecting both classes of errors. For one class we present an incrementally checked record type system, which effectively eliminates these errors. For the other class, we introduce a dynamic safety check, which catches the mistakes relative to programmers' simple annotations.
[Joint work with: Graunke, Findler, Krishnamurthi, Felleisen]
NU Programming Languages Seminar Wednesday, February 11, 2004 306 Egan Hall, Northeastern University 1145-145. Bring your lunch.
Matthias Felleisen
Northeastern University
Software Contracts as Projections
Software contracts help programmers enforce program properties that the language's type system cannot express. Unlike types, contracts are (usually) enforced at run-time. When a contract fails, the contract system signals an error. Beyond such errors, contracts should have no other observable (functional) effect on the program's results. In most implementations, however, the language of contracts is the full-fledged programming language, which means that programmers may (intentionally or unintentionally) introduce visible effects into their contracts.
Here we present the results of investigating the nature of contracts from a denotational perspective. Specifically, we use SPCF and the category of observably sequential functions to show that contracts are best understood as projections. Thus far, the investigation has produced a significantly faster contract implementation and the insight that our contract language cannot express all projections, which in turn has produced a new contract combinator.
NU Programming Languages Seminar Wednesday, February 4, 2004 306 Egan Hall, Northeastern University (building 60 on http://www.campusmap.neu.edu/) 1145-145. Bring your lunch.
Greg Morrisett
Harvard University
Tracking State Changes
Why can't a reference cell hold values of different type at different program points? I've been working on a type-and-effects framework that aims for this goal without forcing references to be linear. Part of the goal is to unify and better understand what's behind the type systems of Vault, C-Qual, TAL, Cyclone, Ownership types, etc.
NU Programming Languages Seminar Wednesday, January 28, 2004 206 Egan Hall, Northeastern University (building 60 on http://www.campusmap.neu.edu/) 1145-145. Bring your lunch.
Mitchell Wand
Northeastern University
Relating Backtracking Monads
(joint work with Dale Vaillancourt)
There are two well-known models of backtracking computation: the stream model and the two-continuation model. The stream model treats backtracking computations with a stream of possible answers, and the two-continuation model uses a success continuation and a failure continuation. Hughes [2000] defined a "backtracking monad" to be a monad with additional operations "disj" and "fail" satisfying 5 additional axioms. Both the stream model and the two-continuation model are backtracking monads, but this fact does not give us any deeper relation between the two.
Past attempts to relate these models have met with limited success: either the types do not work out, or the relation works in one direction but not the other, or the relation does not work for higher-order values.
We show how to relate the two models in a simple way. We relate streams of scalars using a representation inspired by Danvy et al. [2001]. We then extend this to higher-order values using logical relations. At observable types this turns into the identity relation, so we get a denotational equivalence between the values in each model. All of this is done with only elementary mathematics; no category theory is necessary!
NU Programming Languages Seminar Wednesday, January 7, 2004 206 Egan Hall, Northeastern University (building 60 on http://www.campusmap.neu.edu/) 1145-145. Bring your lunch.
Philippe Meunier
Northeastern University
Modular Set-Based Analysis from Contracts
Functional contracts supplement module interfaces with additional information about a function's domain and range. In this talk, we show how to use such contracts to turn set-based analysis in a fully modular analysis. The modified analysis translates modular contracts into two forms of constraints: negative and positive obligations. For the module itself, the derived negative constraints represent checks that ensure that the module meets its expectations. For the clients of the module, the derived positive constraints represent the services that the module provides.
NU Programming Languages Seminar Wednesday, December 3, 2003 206 Egan Hall, Northeastern University (building 60 on http://www.campusmap.neu.edu/) 1145-145. Bring your lunch.
Dale Vaillancourt
Northeastern University
will present
Separation Logic: A Logic for Shared Mutable Data Structures, by John Reynolds
Abstract:
In joint work with Peter O'Hearn and others, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about low-level imerative programs that use shared mutable data structures. The simple imperative programming language is extended with commands for accessing and modifying shared structures, and for explicit allocation and deallocation of storage. Assertions are extended by introducing a ``separating conjunction'' that asserts that its subformulas hold for disjoint parts of the heap, and a closely related ``separating implication''. Coupled with the inductive definition of predicates on abstract data structures, this extension permits thte concise and flexible description of structures with controlled sharing."
NU Programming Languages Seminar Wednesday, November 12, 2003 206 Egan Hall, Northeastern University (building 60 on http://www.campusmap.neu.edu/) 1145-145. Bring your lunch.
Theo Skotoniotis
Northeastern University
will present
A Theory of Aspects, by David Walker, Steve Zdancewic, and Jay Ligatti (ICFP 2003).
Abstract:
We define the semantics of MinAML, an idealized aspect-oriented programming language, by giving a type-directed translation from its user-friendly external language to its compact, well-defined core language. We argue that our framework is an effective way to give semantics to aspect-oriented programming languages in general as the trans-lation eliminates shallow syntactic differences between re-lated constructs and permits definition of a clean, easy-to-understand, and easy-to-reason-about core language. The core language extends the simply-typed lambda calculus with two central new abstractions: explicitly labeled program points and first-class advice. The labels serve both to trigger advice and to mark continuations that the advice may return to. These constructs are defined orthogonally to the other features of the language and we show that our abstractions can be used in both functional and object-oriented contexts. The labels are well-scoped and the language as a whole is well-typed. Consequently, programmers can use lexical scoping in the standard way to prevent aspects from interfering with local program invariants.
NU Programming Languages Seminar Wednesday, November 5, 2003 206 Egan Hall, Northeastern University (building 60 on http://www.campusmap.neu.edu/) 1145-145. Bring your lunch.
Richard C. Cobbe
Northeastern University
will present
"Environmental Acquisition---A New Inheritance-Like Abstraction Mechanism" by Joseph Gil and David Lorenz. (OOPSLA '96)
Abstract:
The class of an object is not necessarily the only determiner of its runtime behavior. Often it is necessary to have an object behave differently depending on the other objects to which it is connected. However, as it currently stands, object-oriented programming provides no support for this concept, and little recognition of its role in common, practical programming situations. This paper investigates a new programming paradigm, environmental acquisition in the context of object aggregation, in which objects acquire behaviour from their current containers at runtime. The key idea is that the behavior of its component may depend on its enclosing composite(s). In particular, we propose a form of feature sharing in which an object "inherits" features from the classes of objects in its environment. By examining the declaration of classes, it is possible to determine which kinds of classes may contain a component, and which components must be contained in a given kind of composite. These relationships are the basis for language constructs that [support] acquisition. We develop the theory of acquisition that includes topics such as the kinds of links along which acquisition may occur, and the behaviour of routine (methods) and attribute features under acquisition. The proposed model for acquisition as a hierarchical abstraction mechanism is a strongly typed model that allows static type checking of programs exploiting this mechanism. We compare it to several other mechanisms including inheritance and delegation, and show that it is significantly different than these.
NU Programming Languages Seminar Wednesday, October 29, 2003 206 Egan Hall, Northeastern University (building 60 on http://www.campusmap.neu.edu/) 1145-145. Bring your lunch.
Jeff Palm
Northeastern University
AspectJ
AspectJ is a general-purpose AOP language implemented as an extension to Java. We report on this language's history, core concepts, comparison to other AOP technologies, and future directions.
NU Programming Languages Seminar Wednesday, October 22, 2003 206 Egan Hall, Northeastern University (building 60 on http://www.campusmap.neu.edu/) 1145-145. Bring your lunch.
Paul C. Attie Northeastern University
A Compositional Automaton-based Model for Dynamic Systems
We present a compositional model of dynamic systems, based on I/O automata. In our model, automata can be created and destroyed dynamically, as computation proceeds. In addition, an automaton can dynamically change its signature, that is, the set of actions in which it can participate. This allows us to model mobility, by enforcing the constraint that only automata at the same location may synchronize on common actions.
Our model is hierarchical: a dynamically changing system of interacting automata is itself modeled as a single automaton that is "one level higher." This can be repeated, so that an automaton that represents such a dynamic system can itself be created and destroyed. This allows us to model the addition and removal of entire subsystems with a single action.
We show that trace inclusion is monotonic with respect to parallel composition in a dynamic system only under certain conditions. Specifically, if automaton creation is not correlated with external behavior, then trace inclusion is not monotonic with respect to parallel composition.
Our trace inclusion results enable a refinement methodology for dynamic systems that is independent of specific methods of establishing trace inclusion. This provides much more flexibility in refinement than a methodology which is, for example, based on the monotonicity of forward simulation with respect to parallel composition. In the latter every automaton must be refined using forward simulation, whereas in our framework different automata in the system can be refined using different methods.
NU Programming Languages Seminar Friday, October 17, 2003 206 Egan Hall, Northeastern University (building 60 on http://www.campusmap.neu.edu/) 1000-1130
Kenichi Asai
The reflective language Black
In this talk, I introduce a Scheme-based reflective language called Black. The interesting feature of the language is its ability to access and even modify its language semantics (provided as a metacircular interpreter) at runtime from within the same language framework. After demonstrating some example interaction on the Black system, I present how such a system can be implemented using metacontinuations and `hooks.' I then clarify its relationship to a tower of interpreters (known as the reflective tower). Finally, I describe challenges for the efficient execution of reflective programs. Although reflection seems to be too theoretical or impractical at first sight, it has impacts on the understanding of interpreters and compilers because of its generality.
NU Programming Languages Seminar Wednesday, October 8, 2003 206 Egan Hall, Northeastern University (building 60 on http://www.campusmap.neu.edu/) 1145-145. Bring your lunch.
Mitch Wand Understanding Aspects
We report on our adventures in the AOP community, and suggest a narrative to explain the main ideas of aspect-oriented programming. We show how AOP as currently practiced invalidates conventional modular program reasoning, and discuss a reconceptualization of AOP that we hope will allow an eventual reconciliation between AOP and modular reasoning.
[This is a presentation of an invited talk given at ICFP 2003. Position paper at ftp://ftp.ccs.neu.edu/pub/people/wand/papers/icfp-03.ps Slides at http://www.ccs.neu.edu/home/wand/papers/icfp-03-slides.ppt ]
NU Programming Languages Seminar Wednesday, October 1, 2003 206 Egan Hall, Northeastern University (building 60 on http://www.campusmap.neu.edu/) 1145-145. Bring your lunch.
Ryan Culpepper will present:
Composable and Compilable Macros: You Want it When? (M. Flatt, ICFP 2002).
Many macro systems, especially for Lisp and Scheme, allow macro transformers to perform general computation. Moreover, the language for implementing compile-time macro transformers is usually the same as the language for implementing run-time functions. As a side effect of this sharing, implementations tend to allow the mingling of compile-time values and run-time values, as well as values from separate compilations. Such mingling breaks programming tools that must parse code without executing it. Macro implementors avoid harmful mingling by obeying certain macro-definition protocols and by inserting phase-distinguishing annotations into the code. However, the annotations are fragile, the protocols are not enforced, and programmers can only reason about the result in terms of the compiler's implementation. MzScheme-the language of the PLT Scheme tool suite-addresses the problem through a macro system that separates compilation without sacrificing the expressiveness of macros.
NU Programming Languages Seminar Tuesday, September 9, 2003 206 Egan Hall, Northeastern University (building 60 on http://www.campusmap.neu.edu/) 1000-1200
Eric Allen
Sun Microsystems, Burlington, MA
A First-Class Approach to Genericity
We describe how to add first-class generic types, including mixins, to strongly-typed OO languages with nominal subtyping such as Java and C#. A generic type system is ``first-class'' if generic types can appear in any context where conventional types can appear. In this context, a mixin is simply a generic class that extends one of its type parameters, e.g., a class C that extends T. Although mixins of this form are widely used in C++ (via templates), they are clumsy and error-prone because C++ treats mixins as macros, forcing each mixin instantiation to be separately compiled and type-checked. The abstraction embodied in a mixin is never separately analyzed.
Our formulation of mixins using first class genericity accommodates sound local (class-by-class) type checking. A mixin can be fully type-checked given symbol tables for each of the classes that it directly references---the same context in which Java performs incremental class compilation. To our knowledge no previous formal analysis of first-class genericity in languages with nominal type systems has been conducted, which is surprising because nominal type systems have become predominant in mainstream object-oriented programming languages.
What makes our treatment of first class genericity particularly interesting and important is the fact that it can be added to the existing Java language without any change to the underlying Java Virtual Machine. Moreover, the extension is backward compatible with legacy Java source and class files. Although our discussion of a practical implementation strategy focuses on Java, the same implementation techniques could be applied to other object-oriented languages such as C# or Eiffel that support incremental compilation, dynamic class loading, and a static type system with nominal subtyping.
Last modified: Mon Aug 21 15:13:57 EDT 2006