The Pi-Lambda Seminar


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



Previous Talks



* 2007
* 2006
* 2005
* 2004
* All

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.