The BRICS Pi-Lambda Seminar

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:

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:

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.

2006

Talk #44

Title: A simple proof of the exponential succinctness gap between CTL+ and CTL
Speaker: Martin Lange
Time and place: Friday, December 8, 2006 at 14:15 in Undervisning lokale 5520.112, IT-Huset

Abstract:

It is known that CTL+, the branching time logics that admits boolean connections of simple linear time properties within each path quantifier, is only as expressive as CTL. According to Emerson/Halpern'85, for each CTL+ formula phi there is an equivalent CTL-Formula psi s.t. |psi|=O(n!). Wilke'99 showed by an automata-theoretic argument that a superpolynomial blow-up is unavoidable. This was improved to an Omega(n!) lower bound in Adler/Immerman'01. We will present a very simple proof of an Omega(2^n) lower bound using CTL's small model theorem.

We also suspect that this technique can be extended to reprove the Omega(n!) lower bound but unfortunately we do not know enough about the iterative generation of all permutations of a list of n elements. Any hints that lead to the finding of the missing knowledge and the encoding in CTL+ will be rewarded.

Talk #43

Title: Eager Normal Form Bisimulation for Sequential Control and State
Speaker: Kristian Støvring ()
Time and place: Tuesday, November 28, 2006, at 15:15 in Turing-024

Abstract:

We present a new normal form bisimulation theory for the untyped call-by-value lambda calculus extended with continuations and mutable references. The associated bisimulation proof principle is sound and complete with respect to contextual equivalence. We demonstrate that this proof principle is furthermore easy to use and that it is a powerful tool for proving equivalences between recursive imperative higher-order programs.

Normal form bisimulation is based on symbolic evaluation of open terms to normal forms. It does not involve any universal quantification over function arguments and is therefore, in some respects, a more powerful proof principle for proving equivalences between recursive higher-order functions than other operationally-based syntactic methods.

This work is joint with Soren Lassen; it is to be presented at POPL'07.

Special BRICS Pi-Lambda Seminar

Speaker: Guy L. Steele Jr. (Sun Fellow, Sun Microsystems Laboratories)
Time and place: Thursday October 5, 2006, 11:15-12:15 in Big Auditorium, IT Huset

Speaker: Erik Meijer (Microsoft Research)
Time and place: Thursday October 5, 2006, 12:30-13:30 in Undervisning lokale 5520.112, IT Huset

More information below.

Talk #42

Title: Parallel Programming and Code Selection in Fortress
Speaker: Guy L. Steele Jr. (Sun Fellow, Sun Microsystems Laboratories)
Time and place: Thursday October 5, 2006, 11:15-12:15 in Big Auditorium, IT Huset (joint with the semantics course)

Abstract:

As part of the DARPA program for High Productivity Computing Systems, the Programming Language Research Group at Sun Microsystems Laboratories is developing Fortress, a language intended to support large-scale scientific computation with the same level of portability that the Java programming language provided for multithreaded commercial applications. One of the design principles of Fortress is that parallelism be encouraged everywhere; for example, it is intentionally just a little bit harder to write a sequential loop than a parallel loop. Another is to have rich mechanisms for encapsulation and abstraction; the idea is to have a fairly complicated language for library writers that enables them to write libraries that present a relatively simple set of interfaces to the application programmer. Thus Fortress is as much a framework for language developers as it is a language for coding scientific applications. We will discuss ideas for using a rich parameterized polymorphic type system to organize multithreading and data distribution on large parallel machines. The net result is similar in some ways to data distribution facilities in other languages such as HPF and Chapel, but more open-ended, because in Fortress the facilities are defined by user-replaceable and -extendable libraries rather than wired into the compiler. A sufficiently rich type system can take the place of certain kinds of flow analysis to guide certain kinds of code selection and optimization, again moving policymaking out of the compiler and into libraries coded in the Fortress source language.

Short bio

Presentation

Talk #41

Title: A Language Geek Perspective of LINQ, XLINQ, DLINQ
Speaker: Erik Meijer (Microsoft Research)
Time and place: Thursday October 5, 2006, 12:30-13:30 in Undervisning lokale 5520.112, IT Huset

Abstract:

Modern applications operate on data in several different forms: Relational tables, XML documents, and in-memory objects. Each of these domains can have profound differences in semantics, data types, and capabilities, and much of the complexity in today's applications is the result of these mismatches. The future "Orcas" release of Visual Studio aims to unify the programming models through integrated query capabilities in C# and Visual Basic, a strongly typed data access framework, and an innovative API for manipulating and querying XML.

This talk explains the programming language theory roots (monads and monad comprehensions, lazy/co-inductive functional programming, meta-programming) behind language integrated queries (LINQ) and briefly discusses the language enhancements to support them. We will give an in-depth treatment of the three domain specific APIs that constitute the LINQ framework namely the standard query operators for objects, the new XLinq API for manipulating XML, and the new DLinq and ADO.Net object-persistence infrastructures.

Short bio:

Erik Meijer is an architect/language pimper in the SQL Server division at Microsoft where he and Brian Beckman run a small team that collaborates closely with the Visual Basic and C# teams on making programming against data radically simpler. In the past, Erik has worked on real and imaginary programming languages such as Haskell, Mondrian, and Comega.

Talk #40

Title: Event Structures with Symmetry
Speaker: Glynn Winskel
Time and place: Thursday, September 21, 2006, at 15:15 in Ada.333

Abstract:

I'll motivate the introduction of symmetry to event structures and give applications: to the equivalence of event structures; the unfolding of Petri nets; and the semantics of higher-order processes.

(The work is recent and ongoing so I'll try to indicate where it is incomplete.)

Talk #39

Title: A functional account of regular patterns
Speaker: Morten Rhiger
Time and place: Monday, September 18, 2006 at 13:15 in Ada.018

Abstract:

Regular patterns, as originally introduced by Hosoya and Pierce in the context of XML, combine features from regular expressions with features from ML-style patterns. In this talk we demonstrate how techniques from functional programming and staged evaluation can be used to specify and then to implement a matching algorithm for regular patterns.

This is work in progress.

Talk #38

Title: Temporal Logics Beyond Regularity
Speaker: Martin Lange
Time and place: Thursday, September 14, 2006, at 15:15 in Turing.024

Abstract:

Temporal logics are mainly used in computer science to specify correctness properties of programs. They are by now well understood in terms of their relationships among each other, expressiveness, and complexity of their satisfiability and model checking problems.

Research on these logics, however, has - with very few exceptions only - focused on very weak logics: variants of fragments of the modal mu-calculus like LTL, CTL, PDL, CTL*, etc. It is well-known that properties that are expressible in the modal mu-calculus are only regular, i.e. definable by a finite Rabin tree automaton for instance.

Many interesting properties of programs are non-regular though and involve some sort of counting for instance.

In this talk we will motivate the use of temporal logics for non-regular properties, introduce some of these logics, and survey known and unknown results about their relationships, expressive powers and complexities.

Slides

Talk #37

Title: Scripting in a Virtually Integrated XML World
Speaker: Kristoffer Rose (IBM T. J. Watson Research Center, New York)
Time and place: Monday, September 4, 2006 at 14:15 in Turing.024

Abstract:

The technology underlying the Internet is changing in fundamental ways. Data that used to be hidden behind (fire)walls is being exposed (for free and pay) through services in a machine readable form specified with the W3C "WSDL" standard (in contrast to the plain web/HTML user readable form). This creates an unprecedented opportunity to write scripts that combine data from many sources.

In this talk I will give an introduction to the new "XQuery" language being standardized by the W3C, and explain how simple extensions to the language allow writing such scripts that access a wide range of data sources.

This work is part of the Virtual XML project.

Short bio:

Kristoffer H. Rose is a Research Staff Member at the IBM T. J. Watson Research Center in New York where he works on solving problems with scalability of data access in general, and XML in particular, using program analysis techniques. Currently he works on scalability and performance of the XML processing languages, such as how XPath and XQuery can be made to execute effectively even when the access properties of data sources, like streamability, indexing, persistence, etc., may not be known until runtime. Most recently Dr. Rose is investigating how updates to data can be expressed and executed efficiently based on an XML model even when the underlying data source is not XML but instead a database, object structure, formatted file, etc.

Before Dr. Rose joined IBM in 2000 he spent three years as an associate professor at ENS-Lyon in France following one post-doctoral year at BRICS (1996-97).

Slides: virtual XML | phantom XML

Talk #36

Title: Implementing and Extending XQuery 1.0: The Story of Galax
Speaker: Mary Fernández (AT&T Labs - Research)
Time and place: Monday, August 28, 2006, at 15:15 in Undervisning lokale 5520.112, IT Huset

Abstract:

XQuery 1.0 and its sister language XPath 2.0 have set a fire underneath database vendors and researchers alike. More than thirty commercial and research XQuery implementations are listed on the XML Query working group home page. Galax (www.galaxquery.org) is an open-source, general-purpose XQuery engine, designed to be complete, efficient, and extensible. During Galax's development, we have focused on each of these three requirements in turn, while never losing sight of the other two.

In this talk, I will describe how these requirements have impacted Galax's evolution, have permitted us to experiment with novel applications of XQuery, and ultimately, have expanded our research interests. In particular, I will describe our extension to XQuery to support querying of distributed, volatile, and inter-dependent XML data sources. We are using "Distributed XQuery" to implement common tasks in distributed-system resource management, like job scheduling in Grid applications and name-resolution protocols in distributed directory systems, such as DNS, LDAP and Active Directory.

Galax is joint work with Jérôme Siméon, IBM T.J. Watson Research Center, and Distributed XQuery is joint work with Trevor Jim, AT&T Labs Research. Many students also participate in these projects.

Short bio:

Mary Fernández is Principal Technical Staff Member at AT&T Labs Research, New Jersey, and member of the W3C Query Working Group. She is co-editor of the XQuery 1.0 and XPath 2.0 Data Model and the XQuery 1.0 Formal Semantics, and she has made significant contributions to research in databases and XML.

Talk #35

Title: Generic Multiset Discrimination
Speaker: Fritz Henglein
Time and place: Thursday, March 30, 2006, at 14:15 in Turing.024

Abstract:

Multiset discrimination is a set of fundamental algorithmic techniques pioneered by Paige et al. in the 80s and 90s for partitioning an input list of acyclic data under a given equivalence relation in worst-case linear time, without the use of hashing or sorting.

In this talk we define a notion of parametric polymorphic discriminators that encapsulate multiset discrimination and show how a rich class of discriminators can be constructed by induction on a language of definable equivalence relations that includes structural equivalence, bag and set equivalences and equivalences definable as least fixed points. A definable equivalence relation gives thus rise to both proof of linear-time discriminability and automatic generation of a worst-case optimal time implementation, which is illustrated by a number of applications that are essentially partitioning problems (anagram classes, finite state machine minimization, type isomorphism with commutative type operators). Extensions to a richer language (preimages, greatest fixed points, etc.) and to circular data with application to more complex examples will be hinted at, time permitting. So will be open problems and consequences for programming language design and implementation.

[ Paper: "Multiset Discrimination" ]

Talk #34

Title: Psychology vs. Programming Languages
Speaker: Johan Trettvik & Rune Nørager (Institute of Psychology, University of Aarhus)
Time and place: Friday, March 17, 2006, at 13:15 in Benjamin.117 [POSTER]

Abstract:

Rune Nørager: "How humans don't think; but computers think we think and make us think...": [presentation]

Programmed technology, which contains software, presents a unique set of challenges to human use compared to other kinds of technology. The challenges, which basically can be described as an incompatibility between man and machine, reflect a deep misunderstanding of human activity and thought processes that can be traced back to logic governing the tools used to program technology – the programming languages.

In this presentation I will address these misunderstandings and give some pointers to how the problems can be remedied within programming languages.

Johan Trettvik: "Objects and Activity" [presentation]

The dealings with objects are part and parcel of our everyday activity. The understanding of objects leads traditionally to the notion of objectivity where objects are seen as independently and prior to the activity. Instead, the activity should be given primacy. I will in this presentation understand objects as crystallizations of activity, and discuss its relevance to a programming language like object oriented programming.

Talk #33

Title: Languages & Languages; Human Languages vs. Programming Languages [POSTER]
Speaker: Jan Rijkhoff & William McGregor (Dept. of Linguistics, University of Aarhus)
Time and place: Friday, February 3, 2006, at 13:15 in Benjamin.117

Abstract:

This special π-λ seminar, "Languages & Languages; Human Languages vs. Programming Languages", will give us insights on how linguists see and think of languages. The seminar features two talks given by researchers Jan Rijkhoff and William McGregor from the Department of Linguistics at the University of Aarhus followed by an open discussion centered around differences and similarities between (natural) human languages and (artificial) programming languages:

Part 1 by Jan Rijkhoff: "Diversity and vagueness in language" (30 mins + questions) [presentation]

This talk deals with two presuppositions on my part: what (I think) non-linguists believe is true for all natural human languages:

they are all rather similar (like Danish, English, etc.);
they are hopelessly vague and underspecified.

It will be shown that human languages

are extremely varied (but within certain limits) in all domains (syntactically, morphologically, semantically, pragmatically, ...), and
can be even more (much more) underspecified than Danish or English.

I will also argue, however, that there is unity in all this diversity, and that underspecification is often necessary for successful communication.

Part 2 by William McGregor: "Natural Human Languages" (30 mins + questions) (presentation)

In this paper I will highlight some characteristics of natural human languages, features that distinguish them from other communicative systems, including animal communication and programming languages (I won’t develop on the latter, but invite the audience at the end to comment on the relationships). I’ll say something about the functions of language - why it has the properties it has - the nature of linguistic meaning, and how meaning is made via language.

Part 3: Open discussion:

Differences and similarities between (natural) human languages and (artificial) programming languages?
What can computer science learn from linguistics?
What can linguistics learn from computer science?
Comments/Questions/...?

Talk #32

Title: Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative
Speaker: Kristian Støvring
Time and place: Friday, January 13, 2006, at 13:15 in Turing.024

Abstract:

The theory of surjective pairing is obtained by adding the following three axioms to the untyped lambda calculus:

		p1 <M, N> = M
		p2 <M, N> = N
		<p1 M, p2 M> = M

Intuitively, these axioms express that every value is a pair (hence the "surjective"), and that every pair is completely determined by its two components.

A "natural" reduction system for this theory is obtained by reading the three axioms above as reduction rules, from left to right. The resulting reduction system is, however, not confluent. In the absence of a (reasonable) confluent reduction system, otherwise simple properties of a theory can be relatively hard to prove.

In 1989, de Vrijer showed that the theory of surjective pairing is conservative over the pure lambda calculus, and then asked whether the same result holds for the extensional lambda calculus (i.e., when adding the eta-axiom). We recently showed that this is the case, using techniques different from those of de Vrijer.

We have formalized the proof of this result using the Twelf system, and the talk will also briefly cover the formalization. Having a machine-checked proof makes it very easy to verify that the proof also goes through when removing the eta-axiom: Remove the corresponding parts of the proof and run the proof-checker again.

2005

Talk #31

Title: Typed Delimited Continuations and its Connection to Modal Logic
Speaker: Yukiyoshi Kameyama (University of Tsukuba, Japan)
Time and place: Friday, December 16, 2005, at 10:15 in Ada.333

Abstract:

First-class delimited continuations (aka "shift" and "reset") are control operators which provide programmers an access to fine control over programs. In the literature several types systems for them have been proposed, however, none of them are satisfactory from programmers' and/or theoreticians' viewpoint. To fill this gap, we propose a simple type (and effect) system for them, and show our type system enjoys all pleasant properties and can type most examples. We also connect our type system to constructive modal logic.

Talk Frequency

Talk #30

Title: Types for Access Control in a Calculus of Mobile Resources [presentation]
Speaker: Hans Huttel (Aalborg University)
Time and place: Friday, November 25, 2005, at 14:15 in Turing.024

Abstract:

In this talk I present a type system for the calculus of Mobile Resources (MR) proposed by Godskesen et al. The type system is able to prevent undesirable border-crossing behaviour such as Trojan horses. This is achieved by combining the notion of group with a notion of security policy. Well-typed processes satisfy a safety property which is preserved under reduction. An algorithm is presented which computes the minimal security policy making a process well typed.

Joint work with Morten Kühnrich.

Talk #29

Title: Convergence of some Extended Systems of Reductions in Simply-typed Lambda-calculus with Inductive Types [paper | presentation]
Speaker: Sergei Soloviev (IRIT, Toulouse)
Time and place: Monday, November 7, 2005, at 14:15 in Turing.024

Abstract:

The interest of extended systems of reductions is that some computational rules are presented as reductions and this may help to obtain more efficient algorithms for equality of lambda-terms (and functions they represent). It is well known that the reasoning based on extensional equality (for example, in proof assistants) could be extremely heavy. At the same time, the attempt to add reductions based on all extensional equalities usually results in systems that are not strongly normalizing and do not have Church-Rosser property (i.e., are not convergent).

We studied the possibility to add reductions related to some extensional equalities of special interest in such a way that convergence is preserved. Maybe most interesting case we studied was the case of isomorphic copy, i.e., the functions f: A --> A’, f’: A’ --> A where A , A’ are inductive type and its isomorphic copy (the names of constructors are changed and possibly some parameters are replaced by isomorphic types). The functions f , f’ are mutually inverse w.r.t. extensional equality and new reduction is f’ o f --> id, f o f’ --> id .

In the talk we consider this and other cases in the context of possible applications.

The talk is based on joint works with D. Chemouil and F. Barral.

Workshop Relevant to π-λ

Title: Workshop on Topology and Concurrency [workshop homepage]
Speaker: Rafael Wisniewski, David E. Hurtubise, Ulrich Fahrenberg, Marcel Bökstedt, Glynn Winskel, Kathryn Hess, Éric Goubault, Lisbeth Fajstrup, Martin Raussen, and Krzysztof Worytkiewicz
Time and place: Tuesday, September 27, 2005 at 13:00 -- Friday, September 30, 2005, at 14:00 (University of Aalborg, Denmark)

Talk #28

Title: VDM: Applications of Semantics in Practice [slides]
Speaker: Peter Gorm Larsen (IHA, University College of Aarhus)
Time and place: Wednesday, September 28, 2005, at 15:15 in Ada.018

Abstract:

This presentation will provide a quick overview of the Vienna Development Method (VDM) and its specification languages (VDM-SL and VDM++). More detail will be supplied about the semantic foundations made in the ISO standard for VDM-SL more than a decade ago. Finally the presentation will provide an overview of a large number of industrial projects where I have been involved in applying this semantic-based technology. There is too much presentation material so the audience will be able to decide (dynamically) on the balance between the semantic foundations and the industrial usage of VDM.

Note: Peter Gorm Larsen has more than 10 years experience in industrial applications of semantics.

Joint talk with JuniorKlubben

Title: Implementing Efficient Exact Real Arithmetic
Speaker: Branimir Lambov
Time and place: Wednesday, September 14, 2005, at 14:15 in Turing.024

Abstract:

Many problems in computing come from the inexact nature of the floating point operations used to approximate real number computations. A computation may start with values that are very accurate, but build-up of rounding errors during the course of the computation may accumulate to lead to answers that are very inaccurate or simply completely false without any indication that such an event has occurred.

Although the theoretic foundations of exact real number computation have been discussed for over half a century, the practical implementations of such computations only started to appear in the last decade, but are still almost never used in practice. This is in part due to the the belief that real number computations require the vast computing resources that the initial (and most common) implementations demonstrated.

Fortunately, this need not be the case.

This talk will discuss the theory and practice of exact real computations, focussing on the problems that need to be overcome to achieve performance close to the level of the current hardware floating point (if the computation allows it). The talk will also contain a demonstration of a library that claims such performance.

Talk #27

Title: Eager Normal Form Bisimulation
Speaker: Søren Lassen (Google, Inc.)
Time and place: Wednesday, September 7, 2005, at 11:15 in Turing.130

Abstract:

This talk describes a new bisimulation equivalence for the pure untyped call-by-value lambda-calculus, called enf bisimilarity. It is based on eager reduction of open terms to eager normal form (enf) and can be viewed as the call-by-value analogue of Boehm tree equivalence. Enf bisimilarity is the congruence on source terms induced by the call-by-value CPS transform and Boehm tree equivalence on target terms. Enf bisimilarity enjoys a powerful bisimulation proof principle which, among other things, can be used to establish a retraction theorem for the call-by-value CPS transform.

Appeared in LICS 2005: 20th Annual IEEE Symposium On Logic In Computer Science, Chicago, IL, June, 2005.

[ paper | biography ]

Talk #26

Title: Event Structures and Higher-order Processes
Speaker: Glynn Winskell (University of Cambridge Computer Laboratory)
Time and place: Thursday, August 11, 2005, at 14:30 in Ada.018

Abstract:

Event structures are a model of computational processes. They represent a process as a set of event occurrences with relations to express how events causally depend on others, or exclude other events from occurring. In one of their simpler forms they consist of a set of events on which there is a consistency relation, expressing when events can occur together in a history, and a partial order of causal dependency.

This talk investigates "spans" of event structures to give causal semantics to nondeterministic dataflow and higher-order processes (where input and output may be processes). For this it is useful to generalise event structures to allow events which "persist". In the talk I will motivate the generalisation to event structures with persistence, and discuss applications of maps, monads and spans of event structures, specifically to the semantics of nondeterministic dataflow and higher-order processes. Despite these categorical terms the talk is designed to be largely accessible without knowledge of category theory.

Talk #25, Anniversary Talk

Title: Applications of Proof Interpretations to Proofs in Analysis
Speaker: Philipp Gerhardy
Time and place: Thursday, May 19, 2005, at 13:15 in Ada.018

Abstract:

The activity of proof mining is the extraction of additional information, e.g. algorithms or programs, from formal proofs in mathematics and computer science. In recent years, the technique of monotone functional interpretation (and similarly: monotone modified realizablity interpretation) developed by Ulrich Kohlenbach has proven particularly useful for "mining" proofs in analysis. In this talk, we will present recent extensions of those monotone proof interpretations and applications of these results to e.g. proofs in fixed point theory and approximation theory.

Pictures:

[ Pre-talk discussion:
"P = NP <=> N = 1 or P = 0" ]
[ 25^th π-λ speaker ]
[ "Piece of cake" ]

[ 25^th π-λ anniversary cake ]
[ "Divide & conquer" ]

Talk #24

Title: A Program Inverter Based on Parsing Methods
Speaker: Robert Glück (DIKU)
Time and place: Friday, May 13, 2005, at 13:15 in Turing.016

Abstract:

Program inversion is a fundamental concept in program transformation. We describe the principles behind an automatic program inverter, which we developed for a first-order functional language. The examples belong to different application areas, including encoding and decoding, printing and parsing, and bidirectional data conversion. The core of the system uses a stack-based language, local inversion, and eliminates nondeterminism by applying methods from parsing theory.

Joint work with M.Kawabe, Waseda University, Tokyo.

Talk #23

Title: Program Extraction from Proofs of Weak Head Normalization
Speaker: Kristian Støvring
Time and place: Wednesday, May 11, 2005, at 13:15 in Turing.016

Abstract:

Normalization of typed term calculi is often proved using a powerful technique known as logical predicates or reducibility predicates. It is well-known that such a constructive normalization proof often "contains" a special kind of normalization algorithm based on evaluation in a partially syntactic model: a so-called normalization by evaluation algorithm. Still, little work has been done on the formal correspondence between these normalization proofs and normalization algorithms.

In this talk, we consider two proofs of weak-head normalization for the simply-typed lambda calculus. Using Kreisel's modified realizability proof interpretation, we extract normalization functions based on evaluation in a "glueing" model, as described by Coquand and Dybjer. The methods we use were first used by Ulrich Berger to extract a normalization function from a proof of strong normalization for the simply-typed lambda calculus.

This is joint work with Malgorzata Biernacka and Olivier Danvy.

Talk #22

Title: Process Mining: Discovering Process Models From Event Logs [presentation]
Speaker: Wil van der Aalst (Technical University of Eindhoven (TU/e))
Time and place: Wednesday, May 4, 2005, at 13:15 in Turing.016

Abstract:

Recently, process mining has become a vivid research area. The basic idea of process mining is to discover process models from event logs. There are different approaches (e.g., genetic algorithms but also more analytical approaches) using different target formats (e.g., Petri nets). However, the topic is not limited to discovering process models. Process mining techniques and tools provide the means for discovering process, control, data, organizational, and social structures from event logs and can also be used for Delta analysis and conformance checking. In this talk, Prof. Wil van der Aalst provides an overview of process mining techniques / tools and their challenges. Moreover, he will focus on techniques to discover the control flow dimension, e.g., algorithmic and genetic approaches to construct Petri nets based on event logs. In addition he will show the ProM framework for supporting process mining efforts.

Talk #21

Title: Towards Ubiquitous Computing (An Overview)
Speaker: Doina Bucur (visiting student from University Politehnica of Bucharest)
Time and place: Monday, May 2, 2005, at 13:15 in Turing.016

Abstract:

This talk will present the work of Doina Bucur and some of the research belonging to the Computer Science department of the "University Politehnica of Bucharest" concerning design, mobility, communication and context-awareness tools in large-scale networks, with a view towards building a foundation for the study of the Global Ubiquitous Computer.

Talk #20

Title: A Framework for Concrete Reputation-Systems with Applications to History-Based Access Control
Speaker: Karl Krukow
Time and place: Thursday, April 21, 2005 at 14:15 in Turing.016

Abstract:

This talk is a continuation of an earlier pi-lambda talk (A Formal Framework for Concrete Reputation-Systems).

Short abstract for those who attended the last talk:

We have extended the logic to include parameterized events and quantification. Even though we quantify over infinite parameter sets, the model-checking problem remains decidable: we can extend the "array-based" algorithm in a neat way. Unfortunately the problem it is NP hard. We can encode (in the logic) several approaches to history-based access control, known from the litterature.

Paper abstract (for everyone else):

In a reputation-based trust-management system, agents maintain information about the past behaviour of other agents. This information is used to guide future trust-based decisions about interaction. However, while trust management is a component in security decision-making, few existing reputation-based trust-management systems aim to provide any formal security-guarantees.

We provide a mathematical framework for a class of simple reputation-based systems. In these systems, decisions about interaction are taken based on policies that are exact requirements on agents' past histories. We present a basic declarative language, based on pure-past linear temporal logic, intended for writing simple policies. While the basic language is reasonably expressive, we extend it to encompass more practical policies, including several known from the literature. A naturally occurring problem becomes how to efficiently re-evaluate a policy when new behavioural information is available. Efficient algorithms for the basic language are presented and analyzed, and we outline algorithms for the extended languages as well.

Talk #19

Title: CAC, a Context-Aware Calculus
Speaker: Pascal Zimmer
Time and place: Friday, April 15, 2005, at 14:15 in Turing.016

Abstract:

In order to answer the challenge of pervasive computing, we propose a new process calculus, whose aim is to describe dynamic systems composed of agents able to move and react differently depending on their location. This Context-Aware Calculus features a hierarchical structure similar to mobile ambients, and a generic multi-agent synchronization mechanism, inspired from the join-calculus. After general ideas and introduction, we review the full calculus' syntax and semantics, as well as some motivating examples, study its expressiveness, and show how the notion of computation itself can be made context-dependent.

Talk #18

Title: Bananas, Lenses, and Acid Rain
Speaker: Kevin Millikin
Time and place: Wednesday, March 16, 2005, at 15:15 in Turing.016

Abstract:

Programs are often structured as a composition of functions, each producing and consuming tree-structured data. The construction of intermediate trees is wasteful of both time and space. We show how to write such programs using the generic recursion operators catamorphism, anamorphism, and hylomorphism, which can be derived for any algebraic datatype. Generic recursion leads us to deforestation to eliminate intermediate trees. We focus on the intuition behind catamorphisms and anamorphisms, and on recognizing them in our programs.

Talk #17

Title: Verifying Programs That Manipulate Pointers
Speaker: Anders Møller
Time and place: Tuesday, March 1, 2005, at 13:15 in Turing.016

Abstract:

Reasoning about the correctness of programs that manipulate data structures using pointers is notoriously difficult: Destructive updating through pointers can make complex structures, the heap has an unbounded size, and data-structure invariants typically only hold at the beginning and end of operations. Correctness properties include absence of null pointer dereferences, dangling pointers, and leaking memory, but also more specialized requirements such as partial correctness of procedures.

This talk will give a brief overview of three approaches towards verifying programs that manipulate pointers: separation logic by Reynolds, O'Hearn, and others; parametric shape analysis by Sagiv, Reps, and Wilhelm; and pointer assertion logic by Møller and Schwartzbach.

Talk #16a and #16b

Title: A Functional Correspondence between Evaluators and Abstract Machines (Parts 1+2)
Speaker: Mads Sig Ager
Time and place:
Part 1: Thursday, February 24, 2005, at 14:15 in Turing.016
Part 2: Friday, February 25, 2005, at 13:15 in Turing.016

Abstract:

Evaluators are interpreters for expressions in a programming language. Abstract machines are deterministic transition systems for executing expressions. Evaluators and abstract machines for the same programming language are usually developed independently and subsequently proved to be equivalent.

In these two talks we present a functional correspondence between evaluators and abstract machines. The basic observation is that a recursive function over an inductively defined datatype can be turned into a transition system using well-known program transformations: lambda lifting, closure conversion, continuation-passing style transformation and defunctionalization. If the recursive function is an evaluator the resulting transition system is an abstract machine.

Part 1 (Thursday @ 14:15): The first talk will be concerned with the basic observation and its consequences for constructing abstract machines for pure languages. For example, we show how the construction yields known abstract machines that have been independently designed, and how it yields new abstract machines. We also show how the construction enables one to ``reverse-engineer'' the evaluator corresponding to an abstract machine.

Part 2 (Friday @ 13:15): The second talk will be concerned with the construction of abstract machines for impure languages starting from monadic evaluators and any computational effect expressed as a monad. Again, we show that the construction yields known abstract machines that have been independently designed as well as new abstract machines. We also use the correspondence to characterize properly tail recursive stack inspection as a lifted state monad. This characterization enables us to mechanically construct abstract machines for languages with properly tail recursive stack inspection combined with other computational effects.

Talk #15

Title: Bigraphs and Reactive XML - an XML-centric model of computation?
Speaker: Thomas Hildebrandt (ITU)
Time and place: Thursday, February 17, 2005, at 15:15 in Turing.016

Abstract:

So-called XML-centric models of computation have been proposed as an answer to the demand for interoperability, heterogeneity and openness in globally distributed applications.

Recently, the theoretical model of Bigraphical Reactive Systems has been introduced as a meta-model for reactive systems with semi-structured state. We present an XML representation of bigraphical reactive systems called Reactive XML. It may be seen as an open, XML-centric model of computation with a solid theoretical foundation given by the theory of bigraphical reactive systems. In particular, the theory provides a formal denotation of composition and general transformations of XML documents with links. On the other hand, Reactive XML provides a concrete understanding of the theoretical model of bigraphical reactive systems.

We report on a prototype for Reactive XML, describing how Reactive XML reactions can be carried out in praxis. In particular, we describe how the abstract notion of evaluation contexts may be represented concretely (and generalised) by XPath expressions. The prototype is currently being extended to a distributed, peer-to-peer setting based on XMLstore, ultimately allowing distributed XML-centric applications to coordinate through computations on shared XML data.

The talk is based on an ITU technical report TR-2005-56 available online here.

Talk #14

Title: Domain-Specific Languages
Speaker: Torben Mogensen (DIKU)
Time and place: Friday, February 11, 2005, at 14:15 in Turing.016

Abstract:

A domain-specific language is a programming language designed for a specific domain of problems and uses concepts from this domain. The intention is to ease cooperation between domain experts and programmers, as the methods used by experts are more easily made into programs and the programs are more easily understood by the domain experts. This reduces the risk of misunderstandings and the consequent errors and reprogramming. Furthermore, it is possible to build domain-specific constraints into the language so these can be verified statically, whereby yet another source of errors can be eliminated.

Classical examples of domain-specific languages are database query languages like SQL and text formatting languages like LaTeX and HTML.

A program in a domain-specific language is not only something that can be executed, but can also be used as documentation, specification or as subject for automatic analysis.

Ideally, a domain-specific language is designed in cooperation between domain expters and programming language designers, as you thereby achieve the best integration of domain knowledge and expressibility.

The talk will discuss design and implementation of domain-specific languages and give a detailed look at a language for cashflow reengineering and a language for die-rolls in games.

Talk #13

Title: XACT: XML in Java
Speaker: Anders Møller
Time and place: Friday, February 4, 2005, at 13:15 in Turing.016

Abstract:

XACT is a Java-based system for programming XML transformations. This talk will give a brief overview of the design of XACT and of the program analysis techniques we have developed for providing static validity guarantees.

This is ongoing, joint work with Aske Simon Christensen, Christian Kirkegaard, and Michael Schwartzbach.

Talk #12

Title: An Overview of Research in Wheels
Speaker: Olivier Danvy
Time and place: Friday, January 28, 2005, at 13:15 in Turing.016

Abstract:

At the turn of November 2004, I successively visited the University of Chicago, the United States Military Academy at West Point, and the IBM T. J. Watson Research Center in Upstate New York. Visits abroad always open new intellectual horizons, and this one was no exception. In particular, I was very impressed by Mark Jones's talk at West Point about research in wheels, an engineering discipline that appears to have rather striking parallels with parts of our own research in computer science.

The goal of this presentation is to give a brief overview of this active research area (motivation, goals, achievements so far, which actually include an analogue of our designer-user-maintainer diagram, artefacts, and current challenges). The talk is meant to initiate a discussion among the attendees in order to assess the extent to which the lessons learned in this research area are relevant to us in our own research areas.

Press coverage:
"La roue, il en connaît un rayon."
-- Le Monde, édition du 4 novembre 2004

Talk #11

Title: Lambda: The ultimate little language
Speaker: Olin Shivers
Time and place: Friday, January 14, 2005, at 13:15 in Benjamin.122 (Store Auditorium)

Abstract:

The "little languages" approach to systems programming is flawed: inefficient, fragile, error-prone, inexpressive, and difficult to compose.

A better solution is to embed task-specific sublanguages within a powerful, syntactically extensible, universal language, such as Scheme. I demonstrate two such embeddings that have been implemented in scsh, a Scheme programming environment for Unix systems programming. The first embedded language is a high-level process-control notation; the second provides for Awk-like processing. Embedding systems in this way is a powerful technique: for example, although the embedded Awk system was implemented with 7% of the code required for the standard C-based Awk, it is significantly more expressive than its C counterpart.

Talk #10

Title: Bottom-up β reduction: uplinks and λ-DAGs
Speaker: Olin Shivers
Time and place: Thursday, January 13, 2005, at 13:15 in Ada.018

Abstract:

Terms of the lambda-calculus are one of the most important data structures we have in computer science. Among their uses are representing program terms, advanced type systems, and proofs in theorem provers. Unfortunately, heavy use of this data structure can become intractable in time and space; the typical culprit is the fundamental operation of beta reduction.

If we represent a lambda-calculus term as a DAG rather than a tree, we can efficiently represent the sharing that arises from beta reduction, thus avoiding combinatorial explosion in space. By adding uplinks from a child to its parents, we can efficiently implement beta reduction in a bottom-up manner, thus avoiding combinatorial explosion in time required to search the term in a top-down fashion.

I will present an algorithm for performing beta reduction on lambda terms represented as uplinked DAGs; describe its proof of correctness; discuss its relation to alternate techniques such as Lamping graphs, the suspension lambda-calculus (SLC) and director strings; and present some timings of an implementation.

Besides being both fast and parsimonious of space, the algorithm is particularly suited to applications such as compilers, theorem provers, and type-manipulation systems that may need to examine terms in-between reductions---i.e., the "readback" problem for our representation is trivial.

Like Lamping graphs, and unlike director strings or the suspension lambda-calculus, the algorithm functions by side-effecting the term containing the redex; the representation is not a "persistent" one.

The algorithm additionally has the charm of being quite simple; a complete implementation of the core data structures and algorithms is 180 lines of fairly straightforward SML.

2004

Talk #9

Title: A Calculus for Trust Management
Speaker: Marco Carbone
Time and place: Friday, December 10, 2004, at 14:15 in Turing.016

Abstract:

We introduce ctm, a process calculus which embodies a notion of trust for global computing systems. In ctm each principal (location) is equipped with a policy, which determines its legal behaviour, and with a protocol, which allows interactions between principals and the flow of information from principals to policies. We elect to formalise policies using a datalog-like logic, and to express protocols in the process algebra style. This yields an expressive calculus very suitable for the global computing scenarios, and provides a formalisation of notions such as trust evolution. For ctm we define barbed equivalences and study their possible applications.

This is joint work with M. Nielsen and V. Sassone, and is also a test-talk for FSTTCS'2004.

Talk #8

Title: XSugar: Reversible Stylesheets
Speaker: Claus Brabrand
Time and place: Monday, November 29, 2004, at 14:15 in Turing.016

Abstract:

XSLT stylesheets may be used to provide an alternative and more legible syntax for XML documents. However, such transformations are not reversible since no tool exists to automatically parse the alternative syntax back into XML.

We present XSugar, which is a reversible stylesheet language for XML. An XSugar specification is built around a context-free grammar for the alternative syntax and gives a template-based translation into XML. The XSugar tool can then provide three services:

a static guarantee that all XML documents generated from alternative syntax are valid according to a given XML schema;
a translation from alternative syntax into XML; and
a reverse translation from XML into alternative syntax (provided certain injectivity requirements are satisfied).

The well-formedness of both translations are statically checked.

Thus, XSugar is useful for providing an XML syntax for an existing language or for providing an alternative syntax for an existing XML language.

This is on-going joint work with Anders Møller and Michael Schwartzbach.

Talk #7

Title: The Maude MSOS Tool
Speaker: Fabricio Chalub (Universidade Federal Fluminense, Niteroi, Brazil)
Time and place: Friday, November 19, 2004, at 14:15 in Turing.016

Abstract:

Modular SOS (MSOS) is a dialect of Plotkin's SOS developed by Peter Mosses that solves the modularity problem left open by Plotkin. The first goal of this talk is to present the Maude MSOS Tool, a Maude implementation of MSOS, developed together with Christiano Braga, along with MSOS-SL, a specification language for MSOS.

The Maude MSOS Tool is a formal tool that implements a mapping between MSOS and rewriting logic (RWL) a reflective logic very suitable as a semantic framework. Maude is one high-performance implementation of rewriting logic with built-in support for RWL's reflection. It is precisely the reflective capabilites of RWL, implemented in the Maude system, that allow us to create an executable environment for MSOS thus giving rise to the Maude MSOS Tool.

The second goal is to show the recent evolution of MSOS-SL, based on the interaction with Peter Mosses during our visit to Aarhus, and how these modifications will be integrated on the Maude MSOS Tool environment

Talk #6

Title: A Formal Framework for Concrete Reputation-Systems [ presentation ]
Speaker: Karl Krukow
Time and place: Friday, November 12, 2004, at 14:15 in Turing.016

Abstract:

In a reputation-based distributed system, principals record information about their interactions with other principals. This behavioural information is used to guide future decisions about interaction. In many reputation systems this behavioural information is heavily abstracted, which has certain advantages, but also means that a lot of (possibly interesting?) information is lost.

We provide a formal framework for defining a class of "concrete" reputation systems which takes an opposite approach. The advantage of our concrete representation is that there is enough information present that one can formally verify precise properties of past behaviour. We give a language, based on linear temporal logic, for specifying such properties, and show that the problem of verifying that a "past behaviour" satisfies a property (model checking) is efficiently decidable.

This is joint work with Vladimiro Sassone, University of Sussex, and Mogens Nielsen.

Talk #5

Title: Approximating Context-Free Grammar Ambiguity
Speaker: Claus Brabrand
Time and place: Friday, November 5, 2004, at 14:15 in Turing.016

Abstract:

Context-free grammar ambiguity is undecidable.

However, just because it’s undecidable, doesn’t mean there aren’t (good) approximations! Indeed, the whole area of static analysis works on "side-stepping undecidability".

We exhibit a characterization of context-free ambiguity which induces a whole framework for (over-)approximation.

In particular, we give an approximation based on the [Mohri-Nederhof, 2000] regular approximation of context-free grammars and show how to boost the precision even further.

Talk #4

Title: Demand-Driven Type Inference with Subgoal Pruning: Trading Precision for Scalability
Speaker: S. Alexander Spoon
Time and place: Friday, October 29, 2004, at 14:15 in Ada.018

Abstract:

After two decades of effort, type inference for dynamically typed languages scales to programs of a few tens of thousands of lines of code, but no further. For larger programs, this paper proposes using a kind of demand-driven analysis where the number of active goals is carefully restricted. To achieve this restriction, the algorithm occasionally "prunes" goals by giving them solutions that are trivially true and thus require no further subgoals to be solved; the previous subgoals of a newly pruned goal may often be discarded from consideration, reducing the total number of active goals. A specific algorithm DDP is described which uses this approach. An experiment on DDP shows that it infers precise types for roughly 30% to 45% of the variables in a program with hundreds of thousands of lines; the percentage varies with the choice of pruning threshold, a parameter of the algorithm. The time required varies from an average of one-tenth of one second per variable to an unknown maximum, again depending on the pruning threshold. These data suggest that 50 and 2000 are both good choices of pruning threshold, depending on whether speed or precision is more important.

Talk #3

Title: Modular Language Descriptions" [ presentation ]
Speaker: Peter Mosses
Time and place: Wednesday, October 13, 2004, at 14:15 in Ada.018

Abstract:

Formal semantic descriptions of full-scale programming languages can be notoriously difficult to write, as well as to read. Writing a description of a language usually starts from scratch: reuse from previous language descriptions requires first locating a relevant one, then manually copying bits of it -- perhaps with extensive reformulation. Semantic descriptions are often intricate and intimidating documents to read, requiring a good grasp of the formalism used, as well an understanding of the interplay between the parts of the description concerned with different language constructs. Evolution of semantic descriptions, to cope with small changes or extensions to the described language, may require global reformulation.

In other words: however elegant the theoretical foundations of semantic descriptions may be, their pragmatic aspects are often reminiscent of programming large systems before modern software engineering techniques were introduced. A good dose of 'semantics engineering' is needed...

The most extreme modularization imaginable in semantic descriptions is when each individual programming construct is described as a separate and independent component. Two frameworks have recently been adapted specifically to support extreme modularization: Action Semantics (a hybrid of operational and denotational semantics, developed since the end of the 80's -- not to be confused with the action semantics of UML); and Modular SOS (MSOS), a variant of Structural Operational Semantics in which labels on transitions are fully exploited.

[This is a rehearsal of an invited talk to be given at GPCE 2004 later this month. The audience is not assumed to be familiar with the details of particular semantic frameworks.]

Talk #2

Title: Thoughts on the unification of two protocol-security approaches
Speaker: Jesus Almansa
Time and place: Friday, October 8, 2004 at 14:15 in Turing.016

Abstract:

We explore the possibility of proving that security in the Universal Composability framework (UC) be equivalent to security in the probabilistic polynomial-time calculus ppc. Security is defined under active and adaptive adversaries with synchronous and authenticated communication. In detail, we define an encoding from machines in UC to processes in ppc and try to show UC is fully abstract in ppc. To that end, we restrict security in ppc to be quantified not over all possible contexts, but over those induced by UC-environments under encoding. This result would not be "overly permissive" as a security definition in ppc, since the threat and communication models we assume are meaningful in both practice and theory.

Talk #1

Title: On Type Inference in the Intersection Type Discipline
Speaker: Pascal Zimmer
Time and place: Friday, October 1, 2004, at 14:15 in Turing.016

Abstract:

We introduce a new unification procedure for the type inference problem in the intersection type discipline. We show that unification exactly corresponds to reduction in an extended lambda-calculus, where one never erases arguments that would be discarded by ordinary beta-reduction. We show that our notion of unification allows us to compute a principal typing for any strongly normalizing lambda-expression. We also relate our results to previous approaches and study possible extensions to references and recursion.

[ Pre-talk discussion: "P = NP <=> N = 1 or P = 0" ]		[ 25^th π-λ speaker ]		[ "Piece of cake" ]
[ 25^th π-λ anniversary cake ]		[ "Divide & conquer" ]

The Pi-Lambda Seminar

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

Previous Talks

2007

Talk #65

Talk #64

Talk #63

Talk #62

Talk #61

Talk #60

Talk #59

Talk #58

Talk #57

Talk #56

Talk #55

Talk #54

Talk #53

Talk #52

Talk #51

Talk #50

Talk #49

Talk #48

Talk #47

Talk #46

Talk #45

2006

Talk #44

Talk #43

Special BRICS Pi-Lambda Seminar

Talk #42

Talk #41

Talk #40

Talk #39

Talk #38

Talk #37

Talk #36

Talk #35

Talk #34

Talk #33

Talk #32

2005

Talk #31

Talk Frequency

Talk #30

Talk #29

Workshop Relevant to π-λ

Talk #28

Joint talk with JuniorKlubben

Talk #27

Talk #26

Talk #25, Anniversary Talk

Talk #24

Talk #23

Talk #22

Talk #21

Talk #20

Talk #19

Talk #18

Talk #17

Talk #16a and #16b

Talk #15

Talk #14

Talk #13

Talk #12

Talk #11

Talk #10

2004

Talk #9

Talk #8

Talk #7

Talk #6

Talk #5

Talk #4

Talk #3

Talk #2

Talk #1