A Heap-Bounded Assembly Language

  Adriana Compagnoni
Stevens Institute of Technology

Monday, December 10, 2001,
4:31PM     DRL 4C8

The pioneering work of Necula and Lee on Proof-Carrying Code motivated recent developments in typed intermediate languages and typed assembly languages that enforce various security policies during code execution.

In this talk we present ongoing joint work with David Aspinall on the development of a typed assembly language for safe memory space reuse, to be used in a Proof Carrying Code environment.

We present a typed assembly language, HBAL, which has a type system with features for managing space usage. In contrast to other typed assembly languages, HBAL allows memory areas to be reused for values of differing types. We ensure type safety by using a type system with linearity constraints to prevent aliasing of heap locations, together with special pseudo-instructions for altering types at isolated points in the code. The reuse discipline is controlled by compilation from a high-level language, and we demonstrate a compilation from a prototypical first-order functional language, LFPL, due to Hofmann.

Signed binary expansions

  Peter Freyd
University of Pennsylvania

Monday, November 26, 2001,
4:31PM     DRL 4C8

Workshop on the best known method for "infinite precision" real arithmetic and its connection with the construction of the reals as a co-inductive type.

The Girard-Reynolds Isomorphism

  Philip Wadler
Avaya Labs

Monday, November 19, 2001,
4:31PM     DRL 4C8

The second-order polymorphic lambda calculus, F2, was independently discovered by Girard and Reynolds. Girard additionally proved a representation theorem: every function on natural numbers that can be proved total in second-order intuitionistic propositional logic, P2, can be represented in F2. Reynolds additionally proved an abstraction theorem: for a suitable notion of logical relation, every term in F2 takes related arguments into related results. We observe that the essence of Girard's result is a projection from P2 into F2, and that the essence of Reynolds's result is an embedding of F2 into P2, and that the Reynolds embedding followed by the Girard projection is the identity. The Girard projection discards all first-order quantifiers, so it seems unreasonable to expect that the Girard projection followed by the Reynolds embedding should also be the identity. However, we show that in the presence of Reynolds's parametricity property that this is indeed the case, for propositions corresponding to inductive definitions of naturals, products, sums, and fixpoint types.

Undecidability of the optimistic protocol completion
for a 'monadic' class of communication protocols

  Max Kanovich
University of Pennsylvania

Monday, November 5, 2001,
4:31PM     DRL 4C8

Monday, November 12, 2001, (continued)
4:31PM     DRL 4C8

One could claim that the undecidability of the problem of optimistic protocol completion in the absence of an intruder is not so interesting, since the standard security protocol settings include some model of the intruder, who, for instance, can control the network, and can duplicate and delete messages (but not the state of protocol participants). But, many of the approaches for analyzing and reasoning about protocols based on certain formal specification languages, and, prior to analysis of protocol properties related to unreliable broadcast, we have to show that our formal specification of a given protocol meets the protocol rules and conventions at least under ideal conditions when no one interferes with network transmission.

I will show that the optimistic protocol completion is undecidable even for the class of protocols with two participants such that either of them is a finite automaton provided with one register to store one atomic message, and no compound messages are in the use.

An Approach to Model Theory for Finite Structures

  Charles Steinhorn
Vassar

Monday, October 29, 2001,
4:31PM     DRL 4C8

This is joint work in progress with Dugald Macpherson (Leeds). The point is to develop a model theory for classes of finite structures that bears a similarity to contemporary model theory for classes of infinite structures, in which some notion of dimension typically plays a central role. We thus refer to the classes we study as, "classes of finite structures with dimension and measure." Our definition of dimension and measure is directly inspired by the paper, "Definable sets over finite fields," by Chatzidakis, van den Dries, and Macintyre (Crelle 1992). Only the most basic familiarity with model theory will be supposed.

Coinduction and real analyis

  Peter Freyd
University of Pennsylvania

Monday, October 22, 2001,
4:30PM     DRL 4C8

Physicists know how to integrate over all possible paths, computer- vision experts want to assign probabilities to arbitrary scenes, and numerical analysts act as if some continuous functions are more typical than others. In these three disparate cases, a more flexible notion of integration is being invoked than is possible in the traditional foundations for mathematics. If allowed to enter a highly speculative mode, such as the intersection of category theory and computer science, we may bump into some solutions to the problem.

An Algebraic Approach to Combining Stochastic Systems

 Paulo Mateus
IST - Universidade Tecnica de Lisboa

Monday, October 15, 2001,
4:31PM     DRL 4C8

Combining transition systems can be easily achieved with limits, subobjects and fibrations. However, applying this dogma to stochastic systems leads to several hurdles. In fact, the suitable notion of morphism between probability spaces fails to be closed under composition, and hence, we obtain a non-category!

After covering the notions of weak categories in the iterature, we end up with Freyd's framework on paracategories. Then, we recover the notion of limit and fibration via adjunctions. This is achieved in two different ways, both capitalizing on the cartesian closed category of paracategories. On one hand, we generalize Lawvere's comma construction and define adjunction through isomorphism. On the other hand, based on the monoid classifier Delta, we internalize paracategories, and then consider the notion of enriched-adjunction which ensues. The latter reformulation can be interpreted in any category which admits the construction of a bicategory of partial maps. We conclude by applying the established results to the fibred paracategories of stochastic systems.

Language Support for Program Generation:
Semantics, Implementation, and Applications

 Zhe Yang
University of Pennsylvania

Monday, October 1, 2001,
4:32PM     DRL 4C8

This talk will present my dissertation work, which develops programming languages and associated techniques for sound and efficient implementations of algorithms for program generation. First, we develop a framework for practical two-level languages. In this framework, we demonstrate that two-level languages are not only a good tool for describing program-generation algorithms, but a good tool for reasoning about them and implementing them as well. We pinpoint several general properties of two-level languages that capture common proof obligations of program-generation algorithms:

- - To prove that the generated program behaves as desired, we use an erasure property to reduce the two-level proof obligation to a simpler one-level proof obligation.

- - To prove that the generated program satisfies certain syntactic constraints, we use a type-preservation property for a refined type system that enforces these constraints.

In addition, to justify concrete implementations, we use a native embedding of a two-level language into a one-level language. We present two-level languages with these properties both for a call-by- name object language and for a call-by-value object language with computational effects, and demonstrate them through two classes of non-trivial applications: one-pass transformations into continuation- passing style and type-directed partial evaluation for call-by-name and for call-by-value.

Next, to facilitate implementations, we develop several general approaches to programming with type-indexed families of values within the popular Hindley-Milner type system. Type-indexed families provide a form of type dependency, which is employed by many algorithms that generate typed programs, but is absent from mainstream languages. Our approaches are based on type encodings, so that they are type safe. We demonstrate and compare them through a host of examples, including type-directed partial evaluation and printf-style formatting.

Finally, upon the two-level framework and type-encoding techniques, we recast a joint work with Bernd Grobauer, where we formally derived a suitable self application for type-directed partial evaluation, and achieved automatic compiler generation.

Proof Mining: uncovering the computational content of proofs

 Ulrich Kohlenbach
BRICS, University of Arhus

Wednesday, September 19, 2001, 4:30PM    
DRL 4C6

With the term 'proof mining' we denote the activity of transforming a prima facie non-constructive proof into a new one from which certain computational information can be read off which was not visible beforehand. Already in the 1950's Georg Kreisel realized that logical techniques from proof theory -- originally developed for foundational purposes -- can be put to use here. In recent years, a more systematic proof theoretic approach to proof mining in numerical analysis emerged yielding new quantitative (and even qualitative) numerical results in approximation theory and fixed point theory and providing a bridge between mathematical numerical analysis and the area of computability (and complexity) in analysis which has mainly been developed by logicians (and complexity theorists). Although proof mining has been applied also to e.g. number theory and combinatorics, the area of numerical (functional) analysis is of particular interest since here non-effectivity is at the core of many principles (like compactness arguments) which are used to ensure convergence. In mathematical terms this non-computability often is an obstacle to obtain a quantitative stability analysis and rates of convergence.

We will give a survey and discuss two recent applications concerning 1) New uniform bounds for theorems of Ishikawa and Borwein-Reich-Shafrir on the asymptotic regularity of non-expansive mappings, which yield even new qualitative results, and 2) Fully explicit description of the rate of strong unicity for best L_1-approximations of continuous functions by polynomials (joint work with Paulo Oliva).

Pretending Atomicity Based on a Common Locking Discipline

 Scott Stoller
SUNY at Stony Brook

Monday, April 23, 2001, 4:30PM    
Moore 554

When locks are used to protect some shared data structures following a common locking discipline, then, roughly speaking, it is safe to pretend that each thread executes atomically, i.e., without interruption by other threads, except at acquire operations and at accesses to unprotected shared data structures. Traditional methods that justify pretending atomicity require checking whether the locking discipline is followed in the original (fine-grained) system. In some contexts, this defeats the purpose of pretending atomicity. We show how to justify pretending atomicity by checking whether the locking discipline is followed in the coarse-grained system.

Formalizing Anonymity Using Group Principals

 Paul Syverson
Naval Research Laboratory

Monday, April 2, 2001, 4:30PM    
Moore 554

In this talk I will introduce the concept of a group principal, an entity that is composed of some number of ordinary atomic principals. I will discuss a number of different classes of group principals. These appear to be naturally useful for looking at security. I will describe an associated epistemic language and logic that can be used to abstractly represent, for example, threshold-group principals. The language can also represent adversaries that are more complex and often weaker than those typically assumed to have complete control and knowledge of the network. A sample application area of the language is the epistemic characterization of anonymity properties. Anonymity protection properties afforded by systems or protocols can be formulated in this language in terms of intruder knowledge about actions by group principals.

From the rules of logic to the logic of rules

Prof. Jean-Yves Girard
CNRS Institut de Mathematiques de Luminy

Monday, March 7, 2001, 4:30PM    
Class of 1949 Auditorium in Houston Hall (2nd floor)

Prof. Girard's lecture will discuss some developments in logic and proof theory during the twentieth century. These issues will be investigated in relation to computer science. The lecture is aimed at a wide audience, including graduate and undergraduate students in mathematics, computer science, philosophy, linguistics, and cognitive science. The lecture will be given in English.

Prof. Girard is one of the leading logicians in the world today. His contributions include the polymorphic lambda-calculus (system F), the theory of dilators, linear logic, and ludics. He is an associate member of the French Academy of Sciences. Prof. Girard's visit to Penn is jointly sponsored by the Penn Mathematics Department and the French Institute of Science and Technology.

Prof. Girard is visiting Penn in conjunction with the 2001 Annual Meeting of the Association for Symbolic Logic, which will be held at Penn, March 10-13. Please see the web site http://www.ircs.upenn.edu/asl2001/ for further information.

Formalizing Security Requirements for Group Key Distribution Protocols

 Catherine A. Meadows
Naval Research Laboratory

Monday, February 26, 2001, 4:30PM    
Moore 554

Secure group protocols, intended for such applications as key distribution for secure multicast, have become of great practical interest in recent years. However, their security requirements are somewhat different from those of traditional pairwise key distribution protocols, and are not always easy to formalize. In this talk we describe our ongoing work in the formalization and analysis of the Group Domain of Interpretation (GDOI), a secure multicast protocol being developed by the MSec Working Group in the Internet Engineering Task Force, with particular attention to our work in developing a requirements specification using the NRL Protocol Analyzer Temporal Requirements Language (NPATRL). We show how our work in specifying and reasoning about these requirements is leading us to develop a calculus for building and analyzing security requirements for cryptographic protocols.

Safe Ambients: Controlling Interference in Ambients

 Davide Sangiorgi

Monday, February 19, 2001, 4:30PM    
Moore 554

Two forms of interferences are individuated in Cardelli and Gordon's Mobile Ambients (MA): plain interferences, which are similar to the interferences one finds in CCS and pi-calculus; and grave interferences, which are more dangerous and may be regarded as programming errors. To control interferences, the MA movement primitives are modified. On the new calculus, the Safe Ambients (SA), a type system is defined that: controls the mobility of ambients; removes all grave interferences. Other advantages of SA are: a useful algebraic theory; programs sometimes more robust (they require milder conditions for correctness) and/or simpler. These points are illustrated on several examples.

The talk is based on joint work with Francesca Levi (University of Pisa)

Authenticity by Typing in Security Protocols

 Alan Jeffrey,
DePaul University

Monday, February 12, 2001, 5:15 PM    
Moore 554

Understanding the correctness of cryptographic authenticity protocols is a difficult problem. We propose a new method for verifying authenticity properties of protocols based on symmetric-key cryptography. First, we code the protocol in the spi calculus of Abadi and Gordon. Second, we specify authenticity properties expected of the protocol by annotating the code with correspondence assertions in the style of Woo and Lam. Third, we figure out types for the keys, nonces, and messages of the protocol. Fourth, we mechanically check that the spi calculus code is well-typed. We have a type safety result that ensures that any well-typed program is robustly safe. It is feasible to apply this method by hand to several well-known cryptographic protocols; hence the method is considerably more efficient than previous analyses of authenticity for the spi calculus. Moreover, the types for protocol data serve as informative documentation of how the protocol works. Our method led us to the identification of problems in an authentication protocol due to Woo and Lam, previously discovered by Abadi, Anderson and Needham.

Joint work with Andrew D. Gordon

Partially Additive Categories and Fully Complete Models of Linear Logic

 Esfandiar Haghverdi,
University of Pennsylvania

Monday, January 29, 2001, 4:30 PM     Part 1
Monday, February 5, 2001, 4:30 PM     Part 2
Moore 554

Traditional completeness theorems are with respect to provability, whereas full completeness is with respect to proofs. In a categorical setting this amounts to asking for the unique free functor from the free category representing the logic to the model category be full. Thus, full completeness establishes a tight connection between syntax and semantics compared to completeness.

In this talk, we will present a class of new models for the multiplicative fragment of linear logic based on the partially additive categories (PAC) of Manes and Arbib. PAC's have become important structures in studying several aspects of iteration and fixed point theories, geometry of interaction and semantics of programming languages. We utilize two important constructions to construct models of multiplicative linear logic based on PACs, namely the Int construction of Joyal, Street and Verity and double glueing construction of Loader, Hyland and Tan. Finally, we prove full completeness for these models. The semantic framework for the latter result is the proofs-as-dinatural transformations paradigm of Bainbridge-Freyd-Scedrov-Scott.

The talk consists of two parts, in Part I we will mainly introduce the basic mathematical tools and notions of importance for our results and in Part II we will focus on the presentations of the main results.