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.
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" ] |
 [ 25th π-λ speaker ] |
 [ "Piece of cake" ] |
|||
 [ 25th π-λ 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.