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.
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.
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.
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.
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.
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.)
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.
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.
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
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.
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" ]
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.
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:
It will be shown that human languages
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:
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.
