The Pi-Lambda Seminar


at the Department of Computer Science, Faculty of Science, University of Aarhus



Previous Talks



* 2007
* 2006
* 2005
* 2004
* All

2007


Talk #65

Title: Formal Topology and the Correctness of a Haskell Program for Untyped Normalization by Evaluation
Speaker: Peter Dybjer (Computing Science Department, Chalmers University of Technology, Sweden)
Time and place: Wednesday, October 24, 2007 at 14:15 in Turing-230
Host: Olivier Danvy

Abstract:

I will show a Haskell program which normalizes untyped terms in combinatory logic, and prove that it lazily computes (in a certain sense) the combinatory Böhm tree of a term. The proof method follows an approach to domain theory due to Martin-Löf 1983 which uses so called "formal neighbourhoods" of programs. I will also say something general about these elegant and not widely known ideas which connect operational and denotational viewpoints in semantics and constitute a first chapter in "formal topology".

Bio:

Peter Dybjer is professor of computing science at Chalmers University of Technology in Gothenburg, Sweden. He got his MSc at UCLA in 1980, was a visiting PhD student at the University of Edinburgh 1980-81, and received his PhD at Chalmers in 1983. He has been a guest researcher at the Newton Institute for Mathematical Sciences in Cambridge, England and at the Mittag-Leffler Institute in Djursholm, Sweden. He was the founder of the EU working group on Applied Semantics, and has also participated in the EU projects on Categorical Logic in Computer Science and Types for Proofs and Programs. Peter Dybjer is an invited speaker at various scientific meetings (e.g., MFPS 2008) and is going to give a keynote talk at FLOPS 2008. His main interests revolve around Martin-Löf's constructive type theory. He has in particular contributed to the constructive theory of inductive definitions, and found the new unifying principle of "inductive-recursive definition" which helps systematizing the constructive higher infinite. Other interests include interactive proof assistants, semantics of programming languages, the connection between category theory and type theory, and normalization by evaluation.

Talk #64

Title: Teaching with Scheme
Speaker: Jens Axel Søgaard (Vestjysk Gymnasium Tarm, DK)
Time and place: Friday, October 19, 2007 at 14:15 in Turing-014
Host: Olivier Danvy

Abstract:

Teaching a first programming course in high school involves a lot of choices, including the following three questions:

  • Which programming language?
  • Which programming environment?
  • Which text book?

To answer these questions objectively it is important to make explicit the principles of programming we expect the students to learn in a first programming course. Making the principles explict allows us to focus on which features the programming language and the programming environment must possess in order to facilitate teaching the principles.

In this talk I'll present a set of principles of programming, and argue why my answers to the first three questions are: Scheme, DrScheme and "How to Design Programs" (Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, and Shririam Krishnamurthi). I'll also present my experience teaching with Scheme and give examples of student projects.

I will also address the following question: Why are the four authors of HtDP all programming-language theorists, and what's in it for them? An answer is that implementing the DrScheme environment and its various teaching languages has been the inspiration for a number of research papers on topics such as:

  • macros and modules (main ideas now in R6RS)
  • algebraic stepper (visualize the evaluation)
  • functional reactive programming
  • delimited-control operators

Bio:

Jens Axel Søgaard received his MsC from the University of Aarhus in 2000. From 2001 to the present he has taught mathematics and computer science at Vestjysk Gymnasium Tarm. He runs Planet Scheme and writes a blog on Everything Scheme.

Talk #63

Title: Multi-Level Generic Programming
Speaker: Sven-Bodo Scholz (Senior Lecturer at the University of Hertfordshire, UK)
Time and place: Wednesday, October 17, 2007 at 13:15 in Turing-014
Host: Olivier Danvy

Abstract:

Data type generic programming enables the definition of functions on the structure of data types rather than individual data types themselves. Similar to all-quantified polymorphic functions, data type generic functions have an open nature: The exact definitions of the data types of the arguments are neither required for type-checking nor for compiling these functions. Instead, they are applicable to novel data types right away. However, data type generic functions contrast from polymorphic functions in that they are usually integrated with ad-hoc polymorphism, i.e., with overloading mechanisms. This measure allows the data type generic functions to be used as boilerplate code which can be "overwritten" for individual data types whenever required. Due to the nature of the type classes that realise ad-hoc polymorphism, such type-specific function definitions are of a closed nature: they cater for a fixed set of known data types only.

In this talk we propose a different approach to data type generic programming which caters for arbitrary levels of data type generic functions that are open. It is based on the idea of combining subtyping and function overloading in a general fashion. Besides sketching a type system for our approach, we give several examples of the resulting expressiveness as they can be observed in SaC, a functional programming language for high-performance array programming. Finally, we also discuss a few implementation issues of the proposed approach.

Bio:

Sven-Bodo Scholz received his PhD and a German Habilitation from the University of Kiel in 1996 and in 2004, respectively. Currently, he is Senior Lecturer at the University of Hertfordshire, UK. His main research interest is in functional programming languages, high-level array programming, high-performance parallel computing and all theoretical advances and technologies that affect the interplay of these goals. He has led several research projects focused around the design and implementation of functional programming systems all of which contributed to ready-to-use systems in the public domain. He is a key contributor to the design and implementation of the functional array language SaC whose runtime performance competes with that of industrial Fortran compilers.

His home page is at http://homepages.feis.herts.ac.uk/~comqss/.
The SaC homepage is at http://www.sac-home.org/.

Talk #62

Title: The advent of a new Generation of Hardware -- new Opportunities for Functional Programming???
Speaker: Sven-Bodo Scholz (Senior Lecturer at the University of Hertfordshire, UK)
Time and place: Wednesday, October 17, 2007 at 11:15 in Turing-014
Host: Olivier Danvy

Abstract:

For the last decades Moore's law has manifested itself in terms of clock frequency increases. Today, there seems to be a consensus among the major hardware vendors and the computer architecture research community that we will see an increase of the number of processing cores per die instead.

This poses a particular challenge on the software and programming environments of the future: an utilisation of the new processing power requires programs not only to be executed in a parallel fashion, but it also requires the available parallelism to scale to the programming resources available.

Functional programming languages have demonstrated their particular suitability for concurrent executions. In this talk we try to relate the potential of the functional paradigm to the upcoming generation of hardware. After giving a brief introduction to some of the novel hardware architectures we outline the achievements of parallel functional programming at the example of SAC, a high-performance functional array programming language. Emphasis is put on the generic programming facilities in SaC as well as the runtime performance that can be achieved from such specifications by means of advanced functional optimisation and compilation techniques.

Bio:

Sven-Bodo Scholz received his PhD and a German Habilitation from the University of Kiel in 1996 and in 2004, respectively. Currently, he is Senior Lecturer at the University of Hertfordshire, UK. His main research interest is in functional programming languages, high-level array programming, high-performance parallel computing and all theoretical advances and technologies that affect the interplay of these goals. He has led several research projects focused around the design and implementation of functional programming systems all of which contributed to ready-to-use systems in the public domain. He is a key contributor to the design and implementation of the functional array language SaC whose runtime performance competes with that of industrial Fortran compilers.

His home page is at http://homepages.feis.herts.ac.uk/~comqss/.
The SaC homepage is at http://www.sac-home.org/.

Talk #61

Title: Generation of musical sounds through lazy functional techniques
Speaker: Jerzy Karczmarczuk (University of Caen, France)
Time and place: Tuesday, October 9, 2007 at 13:15 in Turing-014
Host: Olivier Danvy

Abstract:

Among many methods of implementing musical instruments in software, one, based on the simplified simulation of real instruments through the s.c. wave-guide techniques, seems particularly interesting, since it bases a bit more on the physical reality, than on solutions ad hoc. We implement those "wave-guide circuits" as *lazy streams*, which result in incredibly short (and readable) programs able to simulate plucked string, clarinet, etc. We show how the lazy techniques facilitate the implementation of filters, of the reverberation module, and some other effects. As an extra bonus we show a really very short implementation of the generator of the paradoxical Sheppard/Risset sound, which gives the illusion of a continuously rising pitch. Lazy streams are variants of 'lists' whose length is not specified, and whose elements are automatically generated upon need. Their handling involve co-recursion: loops are replaced by "open" recurrencies, without terminating clause, which eliminates most of the administrative code.

Speaker's Bio:

Jerzy Karczmarczuk, on sabbatical from the University of Caen, France, is a former theoretical physicist from the University of Cracow, Poland. His current domain of interest is the scientific / engineering application of functional programming languages, and the functional algorithmization of scientific computational (numerical and semi-numerical) problems, and in particular the application of functional methods to computations in quantum physics.

Talk #60

Title: Programming Languages for Interactive Applications
Speaker: Shriram Krishnamurthi (Brown University)
Time and place: Tuesday 25 September 2007 at 13:15 in Turing-014
Host: Olivier Danvy

Abstract:

Web and graphical applications lend themselves to natural expression in an event-driven, dataflow style. This style is especially valuable when it layers reactivity transparently atop a traditional programming language. It has become especially necessary and valuable with the advent of Ajax applications, with events and flows both within and across processing nodes.

We have therefore built two languages, first FrTime ("father time") atop Scheme and now Flapjax atop JavaScript, to explore these ideas. We have studied implementation techniques, principles for interfacing to interface components and the network, applications such as scriptable debugging, program transformations to improve performance, and integration into programming environments. The talk will cover our results in these areas.

http://www.flapjax-lang.org/

Speaker's Bio:

Shriram Krishnamurthi is an Associate Professor of Computer Science at Brown University. His research draws from programming languages, software engineering, computer-aided verification, and security. His recent work focuses on language support for interactive software, and on analyses for security policies. He is a co-author of the DrScheme programming environment, the FASTLINK genetic linkage analysis package, the Continue conference paper server, the Margrave access control policy analysis package, the Flapjax programming language, and the book "How to Design Programs" (MIT Press, 2001). He has more recently written the text "Programming Languages: Application and Interpretation". He also coordinates the decade-old and highly successful TeachScheme! high school computer science outreach program.

Talk #59

Title: Policy-Informed Program Analyses
Speaker: Shriram Krishnamurthi (Brown University)
Time and place: Tuesday 25 September 2007 at 11:15 in Turing-014
Host: Olivier Danvy

Abstract:

Access-control policies play a central role in controlling the dissemination of sensitive data in domains ranging from library services to healthcare. They represent an important but not isolated example of policies or rules that govern the behavior of programs. Developers increasingly extract these policies into separate modules in their programs, expressing the policies in domain-specific, declarative policy languages.

The subtle nature of these policies suggests this is a natural domain to apply formal methods, while the separation of the policy from the rest of the program affords interesting opportunities. It is, however, unclear that the straightforward application of verification is appropriate or useful. We will discuss these issues, as well as concrete results and tools we have produced.

The talk is self-contained, including a brief tutorial on access-control.

Speaker's Bio:

Shriram Krishnamurthi is an Associate Professor of Computer Science at Brown University. His research draws from programming languages, software engineering, computer-aided verification, and security. His recent work focuses on language support for interactive software, and on analyses for security policies. He is a co-author of the DrScheme programming environment, the FASTLINK genetic linkage analysis package, the Continue conference paper server, the Margrave access control policy analysis package, the Flapjax programming language, and the book "How to Design Programs" (MIT Press, 2001). He has more recently written the text "Programming Languages: Application and Interpretation". He also coordinates the decade-old and highly successful TeachScheme! high school computer science outreach program.

Talk #58

Title: A two value passing call-by-name CPS transformation
Speaker: Xinxin Liu, xinxinios.ac.cn (Laboratory of Computer Science, Institute of Software, Chinese Academy of Science)
Time and place: Wednesday, 19 September 2007 at 11:15 in Turing-014
Host: Olivier Danvy

Abstract:

In this talk we present a CPS encoding for the call-by-name lambda calculus. This encoding improves Plotkin's original encoding in that basic constants and functional constants are encoded uniformly. The trick to achieve this is to pass two values instead of one value in the continuation. We will show that a relationship can be established between terms and their encodings via call-by-name evaluation contexts, and that the relationship can play an important role in proving both simulation and translation theorems.

Biosketch::

Xinxin Liu obtained his Phd degree from the University of Aalborg in 1992. He is now a research professor in the Laboratory of Computer Science in the Institute of Software at the Chinese Academy of Sciences. His research interests include models of concurrency, higher-order and concurrent programming, program specification and verification.

Talk #57

Title: Local testing of message sequence charts is difficult
Speaker: prof. Madhavan Mukund (Chennai Mathematical Institute, Chennai, India )
Time and place: Thursday, August 23, 2007 at 15:15 in Turing-230
Host: Mogens Nielsen

Abstract:

Message sequence charts are an attractive formalism for specifying communicating systems. One way to test such a system is to substitute a component by a test process and observe its interaction with the rest of the system. Unfortunately, local observations can combine in unexpected ways to define implied scenarios not present in the original specification. Checking whether a scenario specification is closed with respect to implied scenarios is known to be undecidable when observations are made one process at a time. We show that even if we strengthen the observer to be able to observe multiple processes simultaneously, the problem remains undecidable. In fact, undecidability continues to hold even without message labels, provided we observe two or more processes simultaneously. On the other hand, without message labels, if we observe one process at a time, checking for implied scenarios is decidable.

This is joint work with Puneet Bhateja, Paul Gastin and K Narayan Kumar.

Talk #56

Title: Model Checking the First Order Fragment of Higher Order Fixpoint Logic
Speaker: Roland Axelsson (Ludwig-Maximilians-Universität München)
Time and place: Wednesday, July 11, 2007 at 11:15 in IT-Huset Undervisning lokale 5520

Abstract:

We present a model checking algorithm for HFL1, the first-order fragment of Higher-Order Fixpoint Logic. This logic is capable of expressing many interesting properties which are not regular and, hence, not expressible in the modal mu-calculus. The algorithm avoids best-case exponential behaviour by localising the computation of functions and can be implemented symbolically using BDDs.

We show how insight into the behaviour of this procedure, when run on a fixed formula, can be used to obtain specialised algorithms for particular problems. This yields, for example, the competitive antichain algorithm for NFA universality but also a new algorithm for a string matching problem.

Talk #55

Title: Linear Time Logics around PSL: Complexity, Expressiveness, and a little bit of Succinctness
Speaker: Martin Lange
Time and place: Friday, June 29, 2007 at 11:15 in IT-Huset Undervisning lokale 5520.112

Abstract:

We consider linear time temporal logic enriched with semi-extended regular expressions through various operators that have been proposed in the literature, in particular in Accelera's Property Specification Language. We obtain results about the expressive power of fragments of this logic when restricted to certain operators only: basically, all operators alone suffice for expressive completeness w.r.t. omega-regular expressions, just the closure operator is too weak. We also obtain complexity results. Again, almost all operators alone suffice for EXPSPACE-completeness, just the closure operator needs some help.

Talk #54

Title: Termination Analysis of Logic Programs through Combination of Automatically Inferred Type-Based Norms
Speaker: John Gallagher (Roskilde University)
Time and place: Wednesday, June 20, 2007 at 11:15 in 5520.112 (IT-huset Underv. lok.)
Host: Olivier Danvy

Abstract:

We present two contributions to semantics based termination analysis for logic programs. The first involves a novel notion of type-based size measure (or "norm") where for a given type a corresponding norm is defined to count in a term the number of sub-terms of that type. This provides a collection of candidate norms, one for each type defined in the program. The second enables an analyser to base termination proofs on the combination of several different norms. This is useful when different norms are better suited to justify the termination of different parts of the program. Automatic termination proofs are founded on a version of Ramsey's theorem. Application of the two contributions together consists in considering the combination of the type-based candidate norms for a given program. Both contributions have been introduced into a working termination analyser. Finally, we show that for untyped dialects of Prolog, a recent automatic type inference method yields type-based norms that are just as effective in termination analysis as user-supplied types.

Joint work with Maurice Bruynooghe, Michael Codish, Samir Genaim, Wim Vanhoof and Wouter Van Humbeeck.

About the speaker:

John Gallagher is Professor in the Department of Communication, Business and Information Technologies at Roskilde University. More information about him can be found in his home page.

Talk #53

Title: Practical program transformation using temporal logic and model checking
Speaker: Julia Lawall (DIKU)
Time and place: Wednesday, May 2, 2007 from 11:15 to 12:15 in Ada-018
Host: Olivier Danvy

Abstract:

Program transformations that affect the use of protocols, such as open/read/write/close for files or malloc/free for memory, require taking program control-flow into account, and thus cannot be expressed using program transformation systems that only allow description of abstract syntax trees. An attractive option for reasoning about program control flow is the use of temporal logic and model checking, as a control-flow graph can be viewed as a model, a pattern of code to transform can be viewed as a formula of temporal logic, and the identification of fragments of code that match the pattern can be viewed as model checking. There is, however, a mismatch between the behavior of model checking and the needs of program transformation. A model checker only determines whether a formula holds at a given state, whereas for program transformation, we need to identify all of the states that should be transformed and the transformation that should be applied.

In this talk, we present a variant of the temporal logic CTL that addresses the needs of program transformation. For this, we extend CTL with metavariables and quantification. This work is part of the Coccinelle project targeting a specific kind of program transformation, collateral evolutions, in a specific kind of code, Linux device drivers. We thus also present the Coccinelle transformation specification language SmPL and its translation into our logic. We have implemented our approach and used it to specify the transformations involved in over 70 collateral evolutions. We have successfully applied these transformation rules to over 6000 device driver files from various recent Linux versions.

[Joint work with Rene Rydhof Hansen, Yoann Padioleau, and Gilles Muller]

About the speaker:

Julia Lawall is Associate Professor at DIKU. More information about her can be found in her home page .

Talk #52

Title: JavaGI: Generalized Interfaces for Java
Speaker: Peter Thiemann (Universität Freiburg, Germany)
Time and place: Tuesday, May 1, 2007 at 10:15 in Turing-230
Host: Olivier Danvy

Abstract:

JavaGI is an experimental language that extends Java 1.5 by generalizing the interface concept to incorporate the essential features of Haskell's type classes. In particular, generalized interfaces cater for retroactive and constrained interface implementations, binary methods, static methods in interfaces, default implementations for interface methods, interfaces over families of types, and existential quantification for interface-bounded types. As a result, many anticipatory uses of design patterns such as Adapter, Factory, and Visitor become obsolete; several extension and integration problems can be solved more easily. JavaGI's interface capabilities interact with subtyping (and subclassing) in interesting ways that go beyond type classes. JavaGI can be translated to Java 1.5. Its formal type system is derived from Featherweight GJ.

Joint work with Stefan Wehr and Ralf Lämmel, to be presented at ECOOP'07.

About the speaker:

Peter Thiemann is associate professor at Albert-Ludwigs-University in Freiburg, Germany. His research is centered around programming languages with particular emphasis on static analysis, typing, and program transformation. More information about him can be found on his home page.

Talk #51

Title: Verification with Bounded Model Checking
Speaker: Keijo Heljanko (Academy Research Fellow, Helsinki University of Technology)
Time and place: Friday, April 20, 2007 at 11:15 in Turing-024
Host: Martin Lange

Abstract:

Model checking is a set of methods for analysing whether a model of a system (e.g., a Petri net) fulfils its specification given as a temporal logic formula. Bounded model checking (BMC) was introduced by Biere et. al to further improve the scalability of model checking by applying methods based on propositional satisfiability (SAT). In bounded model checking only counterexample executions of the system that are shorter than some fixed length are considered. The success of BMC, especially in the context of hardware verification, is based on the enormous advances in SAT solving techniques achieved during the last few years. In this talk we focus is on topics which arise when creating an efficient bounded model checkers for an asynchronous system model (e.g., a 1-bounded Petri net). This requires the use of efficient SAT encodings for the model checking problem at hand.

About the speaker:

Keijo Heljanko is an Academy Research Fellow working at Laboratory for Theoretical Computer Science, Helsinki University of Technology (TKK). His research interests are in the areas of computer aided verification tools and algorithms, distributed systems, model checking, and net unfoldings. Keijo received his Master's and doctoral degrees from TKK, and worked as a PostDoc with Prof. Javier Esparza in Stuttgart, Germany before returning back to TKK. More information about him can be found on his webpage.

Talk #50

Title: Disinformation in the Information Age
Speaker: Olivier Danvy
Time and place: Thursday, April 19, 2007 at 15:15 in Turing-024

Abstract:

In his legendary commencement address ``Cargo Cult Science'' at Caltech, Richard Feynman urged scientific writers to report their work as honestly as they possibly can:

``The idea is to try to give all the information to help others to judge the value of your contribution; not just the information that leads to judging it in one particular direction or another.''
The temptation not to follow this advice in our writing is strong, on top of the fact that it is so easy to ``fool ourselves,'' to quote Feynman again.

As reviewers, it takes a certain eye to detect in a submission that we are being led to judging it in one particular direction or another.
As Netizens, we are bombarded with false and misguiding information snippets: spam e-mails, phishing attempts, etc.
As citizens, we are also exposed to disinformation: just click on "all X news articles" on any particular story at http://news.google.com/, and see the slant of some group of story tellers in contrast to others.

The goal of this lecture is to review common disinformation techniques used to present stories in the news.

The lecture will be concluded with some chocolate goodies and an exercise session. The audience will be given a simple story and a few minutes to report it in a slanted way, based on the disinformation techniques presented during the lecture.

About the speaker:

Olivier Danvy works as Associate Professor at DAIMI. He defended a PhD thesis (June 1986) and a French Habilitation (January 1993) in Computer Science at the University Pierre et Marie Curie (Paris VI), and a Danish Doctorate (October 2006) in Computer Science at the University of Aarhus. He has been associated with the BRICS adventure throughout, supervising 12 PhD students with 1 more to go. For better or for worse, he suggested the name "pi-lambda" to the pi-minded and the lambda-inclined programming-language people at DAIMI for the present seminar.

More information about him can be found on the web.

Talk #49

Title: Dynamic Nash equilibria, auto-regulated behaviour, and systems biology
Speaker: Rene Vestergaard (JAIST, Japan)
Time and place: Tuesday, March 13, 2007 at 15:15 in Turing-024
Host: Olivier Danvy

Abstract:

We start by outlining a recent discrete Nash theorem with dynamic equilibria and, in particular, look at how it differs from the usual probabilistic approach in game theory to guaranteeing the existence of "solutions". We then introduce the formal concepts of `auto-regulating system' and `prioritised influence graph' in order to facilitate the kind of steady-state analysis that the result points to. We shall exemplify the technology by looking at the strange case of "the student, the night nurse, and the threat at the watercooler" as a means of introducing and conceptualising life-science applications, e.g., for understanding the pathogenesis of the neurodegenerative Alzheimer's Disease. Finally, we shall attempt to sketch the big picture, namely the use of game-theoretic reasoning as a mathematical/automated abstraction mechanism in middle-out modelling, i.e., to do predictions.

Speaker's bio:

Rene Vestergaard is currently Associate Professor and head of the Formal Reasoning Laboratory at JAIST (Japan Adv. Inst. of Science and Tech.). Before coming to Japan, he worked and studied in Aarhus, Boston, Glasgow, Munich, Edinburgh, and Marseille. His long-term research interests revolve around "proof and economic theory of information structures", i.e., formalising information, proving results about it, and developing meta-theory that clarifies what it all means.

More information about him can be found on his webpage.

Talk #48

Title: Static Analysis for Digital Rights Management
Speaker: Christian W. Probst (Assistant Professor, Technical University of Denmark)
Time and place: Friday, March 2, 2007 at 11:15 in Turing-024

Abstract:

Digital Rights Management is a security property gaining in importance due to commercial interest. It is well known that static analysis can be used to validate a number of more classical security policies, such as discretionary and mandatory access control policies, as well as communication protocols using symmetric and asymmetric cryptography. We show how to develop a staged Flow Logic for validating the conformance of client software with respect to a Digital Rights Management policy and without imposing any cryptographic protection. Our approach is sufficiently flexible that it extends to fully open systems that can admit new services on the fly.

Speaker's bio:

Christian W. Probst is an Assistant Professor at the Technical University of Denmark. His research interests are in the areas of modelling and analysis of systems, virtual execution environments, and optimizing compilers. Christian received his Masters and his Ph.D. in Computer Science from the University of Saarland, Germany. After his Ph.D. he worked as a PostDoc with Michael Franz at the University of California, Irvine.

Talk #47

Title: Register Allocation via Coloring of Chordal Graphs
Speaker: Jens Palsberg (Professor, Vice Chair of Computer Science, UCLA)
Time and place: Tuesday, February 27, 2007 at 15:15 in Turing-024
Host: Olivier Danvy

Abstract:

A revolution in register allocation is going on right now: compared to the state of the art, the new register allocators are much simpler and generate code of equivalent quality. In 2005, Bouchez, Brisk et al., and Hack independently discovered that if a program is in static-single assignment (SSA) form, then a core register allocation problem can be solved in polynomial time. Many compilers and virtual machines represent programs in SSA form internally, including gcc version 4.0, Sun Microsystem's Java HotSpot Virtual Machine, and IBM's Java virtual machine Jikes RVM. A compiler can translate any program to SSA form in polynomial time, and amazingly thereby change the register allocation problem from NP-complete to polynomial time; the reason is that the transformation may change the need for registers. Luckily, the program in SSA form needs a number of registers which is the same or smaller than that of the original program. We have a win-win situation here: translating to SSA form changes an NP-complete problem to a simple polynomial-time problem and it decreases the need for registers.

The key insight is that a program in SSA form has a chordal interference graph. A greedy algorithm can optimally color a chordal graph in linear time in the number of edges. Completing the picture, Hack et al. have presented a new SSA-elimination algorithm that does not demand extra registers. The combined result is a simple, optimal, polynomial-time algorithm for a core register allocation problem. The new SSA-elimination algorithm of Hack et al. is essential because classical SSA elimination leads to an NP-complete core register allocation problem, as shown by Palsberg and Pereira. Register allocation with spilling for SSA form remains NP-complete.

We can get most of the advantages of SSA form without actually transforming to SSA form: a vast majority of realistic benchmark programs have chordal interference graphs. For example, 95% of the methods in the Java 1.5 library have chordal interference graphs when compiled with the JoeQ compiler. Pereira and Palsberg have shown how to add simple heuristics for spilling and coalescing to the greedy coloring algorithm. The result is a simple and efficient register allocation algorithm which compares well with the iterated register coalescing algorithm of George and Appel. This talk was also his keynote talk at Computing: The Australasian Theory Symposium 2007.

Speaker's bio:

Jens Palsberg is a Professor and Vice Chair of Computer Science at UCLA. He received a Ph.D. from University of Aarhus in 1992. His research interests span the areas of compilers, embedded systems, programming languages, software engineering, and information security. He has authored over 80 technical papers, co-authored the book Object-Oriented Type Systems with Michael Schwartzbach, and co-authored the 2002 revision of Appel's textbook on Modern Compiler Implementation in Java. He is the recipient of National Science Foundation CAREER and ITR awards, a Purdue University Faculty Scholar award, an IBM Faculty Award, and an Okawa Foundation research award. Dr. Palsberg's research has also been supported by DARPA, Intel, and British Telecom.

Dr. Palsberg is an associate editor of ACM Transactions of Programming Languages and Systems, a member of the editorial board of Information and Computation, and a former member of the editorial board of IEEE Transactions on Software Engineering. He is serving as the secretary/treasurer of ACM SIGBED, Special Interest Group on Embedded Systems, and he has served as the general chair of the ACM Symposium on Principles of Programming Languages. More information about him can be found on his webpage.

Talk #46

Title: Pantachou, a domain-specific language for distributed and heterogeneous applications
Speaker: Nicolas Palix (Phoenix group, INRIA/LaBRI, Bordeaux, France)
Time and place: Friday, February 23, 2007 at 11:15 in Turing-024
Host: Olivier Danvy

Abstract:

Many domains such as assisted living and building surveillance are based on environments populated with entities that are distributed and networked. These environments challenge developers because entities are heterogeneous in terms of their functionalities, availability, mechanisms to produce/consume data, etc.

Heterogeneity has been successfully modeled with what is called an `ontology' (e.g., Olympus), and ontologies are currently supported by existing languages and tools (e.g., OWL and Protégé). Ontological modeling, however, is not yet integrated into the programming process, and therefore is still a challenge for developers, albeit a smaller one.

We propose a Domain-Specific Language, named Pantachou which is Greek for "everywhere", to develop services that coordinate heterogeneous entities in a customized distributed system.

Our approach consists of first describing the target environment to abstract over variations of entities; this description is then used by Pantachou developers for applications that discover and invoke abstractions of entities. Because it separates concerns, the overall approach enables high-level programming, code re-use, and portability.

A compiler for Pantachou is under development. It targets frameworks customized (i.e., tailored) with respect to environment descriptions.

The Pantachou language is a joint work with Julien Mercadal and Charles Consel. The Framework customization is a joint work with Wilfried Jouve, Julien Lancia and Charles Consel.

Speaker's bio:

Nicolas Palix is a PhD student in the Phoenix group at INRIA/LaBRI. He has previously worked on the Session Processing Language, a domain-specific language for IP telephony services. This language relies on the SIP protocol for IP telephony. SIP is underlying technology of the Pantachou language and its customized frameworks. More information about him can be found on his webpage.

Talk #45

Title: Information Flow, Modularity, and Declassification
Speaker: Anindya Banerjee (Kansas State University)
Time and place: Monday, February 19, 2007 at 15:15 in Turing-024
Host: Olivier Danvy

Abstract:

We give, via a relational Hoare-like logic, the specification of an interprocedural and flow sensitive (but termination insensitive) information flow analysis for heap-manipulating programs. Pointer aliasing is ubiquitous in such programs, and can potentially leak confidential information. Thus the logic employs agreement assertions to describe the noninterference property that formalizes confidentiality, and employs region assertions to describe possible aliasing. Programmer assertions, in the style of JML, are also allowed, thereby permitting a more fine-grained specification of information flow policy. The logic supports local reasoning about state in the style of separation logic.

In the second, more speculative part of the talk, we show how the logic can be used to formalize some recent proposals for declassification. We also show limitations of the logic and consider how abstract interpretation techniques may be used to predict the information released by a security policy.

Parts of this work are joint with Torben Amtoft, Sruthi Bandhakavi, Roberto Giacobazzi, Isabella Mastroeni and David Naumann.

Speaker's bio:

Anindya Banerjee is Associate Professor in the Department of Computing and Information Sciences at Kansas State University, where he is a member of the SAnToS laboratory. More information about him can be found on his webpage.