Abstracts for Logic and Computation Seminar Speakers

1998-1999

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.

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.

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)

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.

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.]

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).

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]

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.

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.

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).

Return to the Logic and Computation Group Page

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