Abstracts for Logic and Computation Seminar Speakers


September 23 (IRCS)

Parallel Reductions in Lambda-Calculus

Masako Takahashi

Tokyo Institute of Technology

In this work, after reevaluating the significance of the notion of parallel reduction in Tait and Martin-L"of style proofs of the Church- Rosser theorems, we show that the notion of parallel reduction is also useful in giving short and direct proofs of some other fundamental theorems in reduction theory of lambda-calculus; among others, we give such simple proofs of the standardization theorem for beta- reduction (a special case of which is known as the leftmost reduction theorem for beta-reduction), the quasi-leftmost reduction theorem for beta-reduction, the postponement theorem of eta-reduction (in beta-eta-reduction), and the leftmost reduction theorem for beta-eta-reduction. The lecture will include introductory and expository material and it will be accessible to graduate students.

September 24 (IRCS)

Lambda-Representable Functions over Free Structures

Masako Takahashi

Tokyo Institute of Technology

In this work we revisit lambda-representability in the simple type system of functions over free structures as well as those over the sets of first-order terms. We first prove a characterization theorem for lambda-representable functions over the sets of first-order terms. Then based on the result we obtain two characterizations of lambda- representable functions over free structures, one of which is a byproduct of our new proof of a Zaionc result. The central notion of our characterizations is a variant of primitive recursion scheme which is similar but different from Zaionc limited primitive recursion. The lecture will include introductory and expository material and it will be accessible to graduate students.

October 26

Modal logics lacking booleans: bisimulations and model theoretic behavior

Natasha Kurtonina

University of Pennsylvania

I will begin with a short discussion of model-theoretic methods for determining why some first order property is or is not expressible in a modal language. In particular, I will be focus on languages lacking some or all booleans. One can find this type of languages for example in the field of substructiral logics; in temporal logics, combining points and intervals may lead us to a restrictive use of boolean negation; in Knowledge Representation various description logics can be translated into sub-boolean modal logics. I will address the general question: How can a sub-boolean language be characterized in terms of unique model-theoretic behavior? In standard modal logic when analyzing expressive power, one seeks a semantic notion of equivalence between models providing a "closest fit". The notion of bisimulation does the job. However, standard bisimulation automatically preserves all booleans, and therefore does not have enough discriminative power to characterize sub-boolean languages. Thus, we need weaker notions of simulations that still allow us to prove nice preservations and invariance results familiar from standard modal logic. I will suggest a picture that describes the correlation between each boolean connective and a related kind of simulation, thus we can better understand "the contribution" of each connective in the full case. Then I will discuss some methods of proving and disproving modal and first order definability.

Note: Part of the talk will reflects a joint work with Maarten de Rijke (University of Amsterdam)

November 2

GJ: Making Java easier to type, and easier to type

Philip Wadler

Bell Labs, Lucent Technologies

The best way to program is to get someone else to do it for you: exploit a reusable library. Many classes, especially reusable ones, are best thought of as generic; for instance, a list is generic in its element type. Java 1.1.6 comes with a Collections Library, including lists, similar to the Standard Template Library for C++. Such classes are easy to define in Java, but not so easy to use. The definer implements a class List where the elements are of type Object. The user has to remember what kind of list it is, and to add casts from Object to the element type where appropriate.

GJ extends Java with generic types. Typing is more precise: one may replace the uninformative List by the more precise, say, List. And there is less to type: no extra casts to insert. Many common errors are caught by the compiler rather than left lurking until run-time. The mechanism looks like templates in C++, but has greater power (you can specify what interface a type should implement) and fewer drawbacks (no risk of code bloat).

GJ contains Java as a subset, and the GJ compiler may be used as a Java compiler. GJ compiles into Java bytecodes, so it runs wherever Java runs. GJ is fully forward and backward compatible: new GJ code may use legacy Java libraries; and legacy Java code may be linked with new GJ libraries. Legacy Java libraries may be retrofitted with GJ types, even if the source is unavailable; in particular, the Java Collections Library has been augmented with generic types. The GJ compiler is itself written in GJ.

GJ was designed so that it could be incorporated into a future Java release, although whether this will happen is unclear. Compatibility with GJ was a design consideration for the new Java Collections Libary.

GJ is freely available over the web from www.cs.bell-labs.com/~wadler/pizza/gj/

GJ is joint work with Martin Odersky at the University of South Australia, and Gilad Bracha and Dave Stoutamire at Sun.

November 9

Modules in LOOM: Classes are not enough

Kim Bruce

Williams College (on leave at Princeton)

Designers of object-oriented languages generally seem to assume that modules are not needed in class-based languages. In contrast, we argue that while there is some overlap in the uses of each, modules provide important advantages over classes in supporting programming in the large. To illustrate these ideas, we present the design of a module construct for our language LOOM which integrates well with the object-oriented paradigm.

We discuss and illustrate the advantages of these modules over a class-only approach. In particular, we illustrate the advantages of modules in supporting better control over information hiding, including the support of access controls like C++'s friends. We criticize the Java package design as being too weak to support the kind of abstraction normally desired with modularity.

Our module construct builds on the earlier Modula-3 module design and on previous theoretical work with bounded existential types.

[Joint work with Leaf Petersen (now at CMU) and Joe Vanderwaart.]

November 16

Some Computer-Related Conundrums

Anatol Holt

Universita di Milano
Steam engines are "energy machines"; are computers "information machines"? What clearly understandable concept of "information" makes this so (or not so)? What - if anything - does "information" have to do with "computing" - in the sense of finding numerical answers to numerical problems? Or with word processing, flight training, chess playing?

Brief biography: Anatol Holt's first two degrees were in Mathematics (Harvard and MIT); a decade later, a PhD in Descriptive Linguistics from the University of Pennsylvania. In 1953, together with the late William J. Turanski, he developed the world's first programming environment (known as "Generalized Programming"); it ran on UNIVACs I and II. In the '60s and early '70s he helped to develop and promote Petri nets. In 1979, together with Paul Cashman, he developed the world's first "coordination system"; it ran on the ARPANET to support military software development. Anatol Holt has engaged in many R&D activities, sponsored by the Airforce, ARPA, and in-dustry. More recently, in Milano Italy he has been teaching and writing books: "Organized Activity and Its Support by Computer" (Kluwer Academic Publishers, Dordrecht Holland), and "Ripensare il Mondo - il Computer e Vincoli Sociali" (Dunod/Masson, Paris).

November 30

Towards a Formal Foundation for UML-RT

Radu Grosu

University of Pennsylvania (and TU Muenchen)
The unified modeling language (UML) developed under the coordination of the Object Management Group (OMG) is one of the most important standards for the specification and design of object-oriented systems. This standard is currently tuned for real-time applications in the form of a new proposal, UML for Real-Time (UML-RT), by Rational Software Corporation and ObjecTime Limited. Because of the importance of UML-RT, ObjecTime Limited, Technische Universitaet Muenchen and the University of Bucharest started a joint project investigating its formal foundation. In this talk I will present part of this foundation, namely the theory of flow and interaction graphs. This theory not only has nice mathematical properties, it also has a nice visual form which could be read and validated by engineers from ObjecTime Limited.

Jan 18

Foundations for Virtual Types

Atsushi Igarashi

University of Pennsylvania (and U. Tokyo)
Virtual types have been proposed as a notation for generic programming in object-oriented languages---an alternative to the more familiar mechanism of parametric classes. The tradeoffs between the two mechanisms are a matter of current debate: for many examples, both appear to offer convenient (indeed almost interchangeable) solutions; in other situations, one or the other seems to be more satisfactory. However, it has proved difficult to draw rigorous comparisons between the two approaches, partly because current proposals for virtual types vary considerably in their details, and partly because the proposals themselves are described rather informally, usually in the complicating context of full-scale language designs.

Work on the foundations of object-oriented languages has already established a clear connection between parametric classes and the polymorphic functions found in familiar typed lambda-calculi. Our aim here is to explore a similar connection between virtual types and dependent records.

We present, by means of examples, a straightforward model of objects with embedded type fields in a typed lambda-calculus with subtyping, type operators, fixed points, dependent functions, and dependent records with both ``bounded'' and ``manifest'' type fields (this combination of features can be viewed as a measure of the inherent complexity of virtual types).

Using this model, we then discuss some of the major differences between previous proposals and show why some can be checked statically while others require run-time checks. We also investigate how the partial ``duality'' of virtual types and parametric classes can be understood in terms of translations between universal and (dependent) existential types. [Joint work with Benjamin Pierce]

Jan 25

Migration = Cloning ; Aliasing

Uwe Nestmann

In Obliq, a lexically scoped, distributed, object-based programming language, object migration was suggested as creating a (remote) copy of an object's state at the target site, followed by turning the (local) object itself into an alias, also called surrogate, for the just created remote copy. There is no proof that object migration in Obliq is safe in any sense.

We consider the creation of object surrogates as an abstraction of the above-mentioned style of migration. We introduce ějeblik, a distribution-free subset of Obliq, and provide an intuitive configuration-style semantics. Based on it, we motivate why surrogation is neither safe in Obliq, nor can it be so in full generality in Repliq, our proposal of a repaired Obliq. We briefly sketch how to prove a positive result for Repliq using a semantics by translation into pi-calculus, and argue why it suffices for practical purposes.

Feb 8

The Undecidability of Propositional Linear Logic Without Variables

Max Kanovitch

Russian State University for the Humanities, Moscow, and U. Penn
Linear logic was introduced by Girard as a resource-sensitive refinement of classical logic. It turned out that full propositional linear logic is undecidable (Lincoln, Mitchell, Scedrov, and Shankar) and, hence, it is more expressive than (modalized) classical or intuitionistic logic. Here we focus on the study of the simplest fragments of linear logic, such as the one-variable and constant-only fragments (the latter contains no variables at all). Here we prove that all these extremely simple fragments of linear logic (one-variable, bottom-only, and even unit-only) are exactly of the same expressive power as the corresponding full versions with an unbounded number of variables.

In particular, 1. On the level of multiplicatives only we get NP-completeness. 2. Enriching this basic set of connectives by additives yields PSPACE-completeness. 3. Using in addition the modal operator !, we can prove undecidability of each of these three fragments.

Feb 22

Contractible graphs and fair games

Hongde Hu

U. Penn
Abstract. A graph G is total if every maximal clique of G meets all maximal stable sets. Total graphs can be seen as models of linear logic. Most of this lecture will be about connections between total graphs and game semantics of linear logic. In particular, we will discuss the relation between total graphs and fair games (introduced by J. M. E. Hyland and C.-H.L. Ong). We will also show that a graph is P_{4}-free (called contractible) if and only if its induced subgraphs are total.

March 15

Workflow, Transactions, and Logic

Anthony Bonner

U. Toronto and U. Penn
Database programming languages have traditionally focussed on specifying queries, updates and transactions. Although suitable for traditional applications, this focus ignores a key problem of many new applications: the need to combine transaction programs into larger business processes. Such applications include workflow management, office automation, cooperative work, and manufacturing control, among others. To address this need, we have developed Transaction Datalog (abreviated TD), a logic-based language that integrates data modelling (queries and updates) with process modelling (concurrency and communication). This talk provides an overview TD, including its logical semantics, its computational complexity, and its applications to workflow. In the process, we show that TD is fundamentally different from traditional database languages.

April 16

What is a Recursive Module?

Robert Harper

A hierarchical module system is an effective tool for structuring large programs. Strictly hierarchical module systems impose an acyclic ordering on import dependencies among program units. This can impede modular programming by forcing mutually-dependent components to be consolidated into a single module. Recently there have been several competing proposals for module systems that admit cyclic dependencies, but it is not clear how these proposals relate to one another, nor how they might be integrated into the ML module system. I will present a type-theoretic analysis of the notion of a recursive module in the framework of the ``phase-distinction'' calculus of higher-order module systems, extended with a new form of signature, called a recursively-dependent signature, for recursive modules. [This talk represents joint work with Karl Crary and Sidd Puri.]

April 29

Parallel functional programming: the OcamlP3l experiment

Roberto Di Cosmo

Ecole Normale Superieure, Paris
Writing parallel programs is not easy, and debugging them is usually a nightmare. To cope with these difficulties, a structured approach to parallel programs using skeletons and template based compiler techniques has been developed over the past years by several researchers, including the P3L group in Pisa.

In a skeleton based parallel programming model a set of skeletons, i.e. of second order functionals modeling common parallelism exploitation patterns are provided to the user/programmer. The programmer must use the skeletons to give parallel structure to his/her application and he/she uses a plain sequential language to express the sequential portions of the parallel application as parameters to the skeletons. He/she has no other way to express parallel activities but skeletons: no explicit process creation, scheduling, termination, no communication promimitives, no shared memory, no notion of being executing a program onto a parallel architecture at all.

All these details relative to parallel execution are actually dealt with by the skeleton compiler and/or run time system.

OamlP3lis a programming environment that allows to write parallel programs in Ocaml (http://pauillac.inria.fr/ocaml) according to the skeleton model supported by the parallel language P3L (http://www.di.unipi.it/susanna/p3l.html), provides seamless integration of parallel programming and functional programming and advanced features like sequential logical debugging (i.e. functional debugging of a parallel program via execution of the architecture at allparallel code onto a sequential machine) of parallel programs and strong typing, useful both in teaching parallel programming and in the building of full-scale applications, like protein folding research (http://www-lifia.info.unlp.edu.ar/~german/instances.htm).

May 13

Verification of control flow based security properties

Tommy Thorn

A fundamental problem in software-based security is whether local security checks inserted into the code are sufficient to implement a global security property. We introduce a formalism based on a two-level linear-time temporal logic for specifying global security properties pertaining to the control-flow of the program, and illustrate its expressive power with a number of existing properties. We define a minimalistic, security-dedicated program model that only contains procedure call and run-time security checks and propose an automatic method for verifying that an implementation using local security checks satisfies a global security property. For a given formula in the temporal logic we prove that there exists a bound on the size of the states that have to be considered in order to assure the validity of the formula: this reduces the problem to finite-state model checking. Finally, we instantiate the framework to the security architecture proposed for Java (JDK~1.2).

Return to the Logic and Computation Group Page

Comments about this page can be sent to bcpierce@saul.cis.upenn.edu.