Abstracts for Logic and Computation Seminar Speakers
The Relational Knowledge-Base Interpretation
and Feasible Theorem Proving for Intuitionistic Propositional Logic
Max I. Kanovich
Russian Humanities State University
A computational semantics is introduced for relational
knowledge bases. Our semantics naturally arises from practical
experience of relational databases and knowledge bases.
We show that intuitionistic logic is an adequate logic behind
the relational knowledge bases. In particular, based on a specific
calculus without contraction, an efficient prove-disprove algorithm
(a) the algorithm runs in linear deterministic space,
(b) for every 'natural' problem, the algorithm runs in polynomial
time, despite of the fact that, because of the PSPACE-completeness
of propositional intuitionistic logic, an exponential execution time
should be expected in the worst case. The point is that these
worst problems need maximal cross-linking of all their possible
The Operational Content of Intersection Types
Simonetta Ronchi della Rocca
University of Turin
Various aspects of the functional computation can be
modeled through (various kind of) lambda calculus. For example,
the call-by-name computation, the call-by-value one, the lazy one,
the relevant one. An operational semantics can be defined
for each one of these paradigmatic languages, starting from
the definition of a set of "values", and a notion of convergency.
A term converges if and only if it reduces (according to a
given reduction strategy) to a value. A notion of operational
equivalence between terms arises naturally, based on Leibnitz
equality. Namely, two terms M and N are operationally equivalent
if and only if every context behaves in the same way (with respect
to the convergency) when filled by either M or N.
Intersection type assignment systems give a tool for reasoning
about operational equivalence of terms. We define a type assignment
system being correct with respect to an operational equivalence
if and only if the fact that two terms can be typed with the
same types implies that they are operationally equivalent.
If also the inverse implication holds the system will be called
complete. For each one of the operational semantics induced by
the before listed computations a correct type assignment system
can be defined.
Computation Models Based on Linear Logic
In this overview
we discuss basic paradigms of traditional logical computation models
for programming language theory, including the proof-search
(logic-programming), reduction (typed-functional programming), and
term-rewriting (equational programming) paradigms. When we modify those
computation models by changing the underlying logic from a traditional
logic to linear logic, we show how the modified (linear logic-based)
computation models can capture the new important computational
concepts such as concurrency, resource-sensitivity, etc.
We also give some examples of logical analysis on process calculi,
proof-normalization, etc., using the framework of those linear-logical
An Introduction to the Distributed Join Calculus
University of Pennsylvania
This talk will be a self-contained introduction to the
distributed join calculus in the form of a tutorial.
As the internet is rapidly growing and new communication technologies
are becoming accessible, issues arise that are not accounted for by the
traditional models of computation. When computational agents can travel
between different sites in a global network, then matters of security
and the possibility of physical failure of connections and sites must be
In order to address these issues in a mathematical context, one needs a
programming paradigm that can express such concepts as locality and
failure, while being conceptually as simple as possible. One such
paradigm is the distributed join calculus, introduced in 1995 by Fournet
The join calculus is a concurrent, message-passing
calculus similar to Milner's pi-calculus, but more suitable for modeling
In the talk, I will begin by introducing the join calculus and its
semantics in terms of a chemical abstract machine. I will show examples
and discuss the relationship to other calculi such as the pi-calculus.
The material that I will present is taken from the two papers below. No
previous knowledge of distributed calculi is necessary.
An Introduction to Program Checking
University of Pennsylvania
Two traditional approaches for establishing program correctness are
verification and testing. In verification we seek to prove that
a program is correct and in testing we simply confirm that the
program performs correctly on a number of (carefully) chosen inputs.
Verification is difficult and testing does not produce satisfactory
mathematical guarantees about the correctness of programs.
Program checking provides a third alternative. Here we seek to
prove that the output of a program on any particular input is correct.
A program checker is itself a program that is run each time the
program being checked is run. Using randomness and interaction
(with the program being checked) the checker produces
probabilistic proofs of correctness of the output.
In this self-contained talk we will present a formal notion of
checking, give examples of checkers, examine connections
between checking and other notions in complexity theory,
and explore extensions and modifications of the basic
paradigm of checking.
The Security of Dynamic Linking with Static Typing
Java combines (mostly) static type checking with dynamic linking.
These features interact in security relevant ways. In this talk, we
explore their interaction, discussing two major bugs that led to the
complete penetration of the system. We then move to a formal model of
dynamic linking in PVS, and formally prove a key safety property about
our model. Other security-relevant "features" of Java will be
discussed. This is joint work with Dirk Balfanz, Ed Felten, and
Relational Queries over Interpreted Structures
It is a classical result in relational database theory that no
first-order query can express the property that the number of elements
in a database is even. This is proved by a straightforward application
of Ehrenfeucht-Fraisse games. If first-order expressions use the order
relation on database elements, parity remains inexpressible, but the
Ehrenfeucht-Fraisse argument is "exponentially harder". If database
elements are real numbers and operations +,* are used in queries, the
Ehrenfeucht-Fraisse argument cannot be done by an ordinary human
being. In fact, it is not even immediately clear that parity is still
The question whether parity test can be defined as a first-order query
with polynomial inequality constraints was asked by the late Paris
Kanellakis when he introduced the constraint database model. In this
talk, I'll review the constraint model which, for our purposes, can be
seen as doing relational theory over interpreted structures, for
example, the real field. I will also explain that the lack of ability
to deal with interpreted operations is a major gap between theoretical
and practical query languages. My main goal is to explain a new
collection of techniques for extending the standard results of
relational theory in such a setting.
In a more abstract way, this work can be viewed as doing finite model
theory when finite models live inside some infinite structures. I
demonstrate several techniques for combining the finite and the
infinite, and prove several complexity and expressivity bound for
various logics (first-order, second-order, fixpoint logics). By the
end of the talk, you'll see at least two different proofs of the
This is joint work with Michael Benedikt (Bell Labs), Guozhu Dong (U
of Melbourne), and Limsoon Wong (ISS, Singapore).
 M. Benedikt, G.Dong, L.Libkin, L.Wong. Relational expressive power
of constraint query languages. PODS'96.
 M. Benedikt, L.Libkin. On the structure of queries in constraint
query languages. LICS'96.
 M. Benedikt, L.Libkin. Languages for relational databases over
interpreted structures. In preparation.
Carnegie Mellon University
It is well known that it is easier to check a proof than to generate one.
In this talk, I make use of this fact to show how an operating system can
determine with certainty that it is safe to execute, in the kernel address
space, a binary supplied by an untrusted source. The kernel first defines
a safety policy and makes it public. Then, using this policy, an
application provides binaries in a special form called Self-Certified
Code, or simply SCC. Each SCC binary contains, in addition to the native
code, a safety certificate that is a formal proof of the code's safety
properties. The kernel can easily validate a certificate without using
cryptography and without consulting any external trusted entities. If the
validation succeeds, the code is guaranteed to respect the safety policy
without relying on run-time checks.
The main practical difficulty of SCC is in generating the certificates. To
see what is involved, I will describe our preliminary experience with a
collection of standard network packet filters, written in hand-tuned DEC
Alpha assembly language. Our SCC binaries are created automatically by a
special prototype assembler, and can be executed with no run-time overhead,
beyond a one-time cost of about 1 millisecond for validating the enclosed
certificates. The net result is that our packet filters are formally
guaranteed to be safe and are faster than packet filters created using
Berkeley Packet Filters, Software Fault Isolation, or safe languages such
as Modula-3. Finally, I will conclude with prospects for future work.
Linear Logic as a Logic Programming Language
University of Pennsylvania and University of Genoa
In recent years, proof theory has been used to motivate and justify the
design of a number of logic programming languages, including lambda Prolog
and its linear logic refinement Lolli. Lambda Prolog and Lolli are
sequential languages (lacking primitives for communication and
synchronization) but contain rich forms of abstractions (including modular
and higher-order programming). On the other hand, the linear logic
programming language LO (Linear Objects) of Andreoli and Pareschi has
primitives for concurrency but lacks abstractions. Since linear logic
provides a foundation for each of these languages, it seems sensible to
look inside it for a single logic programming language that contains these
other languages. In this talk I describe the logic programming language
Forum that modularly extends lambda Prolog, Lolli, and LO. In fact, Forum
is a particular presentation of all of linear logic for which goal-directed
search is complete. Forum contains primitives for concurrency and
abstractions. Forum been used to provide specifications for the
operational semantics of imperative and object-oriented programming
constructs, sequent calculus proof systems for object-level logics, and a
RISC-style, pipe-lined processor. I shall present several examples of
Forum specifications. This talk is largely self-contained and assumes only
familiarity with basic notions of the sequent calculus. [A home page for
Forum can be found at http://www.cis.upenn.edu/~dale/forum/.]
Operational Modal Logic
Steklov Mathematical Institute and Cornell University
Operational Modal Logic (OML) has been developed in order to fill a gap
in the foundations of knowledge presentation, where such a basic
notion as The Provability had been missing its complete modal description.
A "natural born" Goedel provability logic S4 (1933) had been lacking its exact
intended interpretation. The provability logic (Solovay, 1979) axiomatizes
a formal provability operator that cannot be regarded as a decent model
for The Provability; for example, the basic reflection property
"Provable F" implies "F"
fails for the formal provability logic.
In the traditional modal logic the necessity operator $\Box F$ often
stands for "there exists an evidence of F", thus hiding an existential
quantifier behind the modality. We demonstrate that for the logic S4
the corresponding class of Skolem type functions over "evidences"
admits a finite an observable operational basis: in fact, it suffices
to use three operations only. This allows to reformulate S4 and some other
classical modal logics in a purely operational manner where a modality
occurrence "necessarily F" is realized as "t is an evidence of F" for
a corresponding term t. In particular, there is an algorithm that recovers
a term assignment to modalities in an S4 proof. So, OML provides a
more rich language for the traditional modal logic.
This OML technique is applied to answer two old questions:
1. Modal logic S4, which was informally specified by Goedel in 1933 as
a logic for The Provability, meets its exact intended interpretation.
2. Brouwer - Heyting - Kolmogorov realizing operations (1931-32) for
intuitionistic logic Int also get exact interpretation as corresponding
propositional operations on proofs; both S4 and Int turn out to be
complete with respect to this proof realization.
The OML is nicely axiomatized and is shown to be decidable, arithmetically
complete and sufficient to realize every operation on proofs admitting
propositional specification in arithmetic. Hopefully, OML terms can
become useful in many other applications of modal logic.
On Non-Determinism in Queries, Machines and Languages
University of Pennsylvania
There are different levels of non-determinism. A query is non-deterministic
if it may have different possible outputs on a given input. For instance, the
query "give me the name of a postdoc in IRCS" is a non-deterministic query
(this year there there are 13 possible answers to that query). On one hand, a
non-deterministic query is definable in a non-deterministic language, that is
a language that admits a non-determinitic semantics (a formula may have
different interpretations). On the other hand, non-deterministic queries are
computable by non-deterministic Turing machines.
In this talk, I will present various levels of non-determinism in computations
on non-deterministic Turing machines with polynomial bounds on the resources.
Meanwhile, I will consider numerous query languages, implicit logic, choice
logic, and establish correspondences between all these formalisms for both
deterministic and non-deterministic queries.
A paper is available at
A Proof Method in Operational Semantics and its
Application to Hybrid Theorem Proving
The usual notion of equivalence of programs is
observational congruence: two programs are equivalent if one can be
replaced by the other in any containing program without affecting the
observable results of computation. Unfortunately, it can be quite
difficult to directly use the operational semantics of a programming
language to prove that two particular programs are equivalent under
this definition, even for many "obvious" equalities. However,
many languages admit a "coinductive" characterization of observational
congruence that is much easier to work with. This characterization is
a powerful tool for operational reasoning about program equivalence,
and furthermore is valid for some languages which do not yet have a
satisfactory denotational semantics.
The first part of this talk will focus on one of the main methods for
proving that a programming language admits this kind of
characterization. The method has been applied to a variety of
programming languages, including functional and imperative languages,
typed and untyped languages, and object-oriented languages.
The second part of the talk will cover a recent application of the
method in establishing the semantic foundations for a "hybrid"
interactive theorem prover. This hybrid system combines Nuprl and
HOL, two systems with very different logics. Nuprl is a constructive
type theory, where the basic semantic objects are untyped functional
programs, while HOL is essentially a classical set theory. The method
is used in giving an extension to Nuprl's semantics into which HOL's
semantics can be directly embedded. The hybrid Nuprl/HOL system
retains Nuprl's constructivity and expressive type system, and can
draw on the vast store of formal mathematics developed by the HOL user
community over the last decade. A prototype of the system has been
implemented and is currently being used to verify a complex cache
coherency protocol (among other things).
Adjustable Graphic-Based Clustering Method
Naval Research Laboratory
Clustering can be viewed as an inductive method that constructs a graph
representation (i.e., the model) for a given data set with nodes
features, the unknown (referred to here as the hidden node) denoting the
set of clusters and links indicating probabilistic relationships among
features and the unknown. The hidden node is used to interpret unusual
correlation embedded in a set of samples.
In this talk, I'll describe the clustering system I
have developed for experimenting with data organization from two
aspects: The first aspect is about the properties of the proposed
clustering method and the second aspect is on graphic-based
interpretation. In particular, we consider the following issues:
One issue that plagues existing clustering methods is the inefficiency
handling large data sets. This problem exists in both top-down and
clustering search. The proposed method combinatively uses different
of clustering and handles the new datum through iterative adjustment.
The second issue is the evaluation of clustering criteria
for the generated cluster hierarchy. The evaluation is carried out on
basis of statistical properties of the graphic model. To enhance the
in interpretation, we organize instances according to highly correlated
features. The merits of using a graph model will shown with an example.
A Brief Tour of Net Reductions, Geometry of Interaction,
and Optimal Implementations of Functional Programming Languages
University of Pennsylvania
In the 1970's Levy gave a lower bound to the cost of the
implementation of an higher-order FP language by its study on lambda
calculus optimal reductions. He foresaw that the lower bound would have
been reachable by a clever implementation of sharing, but he could not
give an algorithm. Only after more than ten years Lamping was able to
give a brilliant solution to Levy's outlook.
Lamping's breakthrough is a sophisticated graph reduction technique to
implement the sharing of lambda terms contexts. As shown more recently by
Gonthier, Abadi and Levy, the remarkable point of Lamping's algorithm
is that it surprisingly relates with Girard's Linear Logic and with
Girard's research on the mathematical foundations of operational
semantics through the so-called "Geometry of Interaction" (GOI).
This lecture series will not be overcharged with too many technical details.
It aims at providing a smooth introduction to the fascinating subject of
GOI and optimal reductions, showing some of the main results of them and
a taste of the really intriguing nature of optimality: a nice, tough
mathematical theory applied to a very practical problem.
The series will consist of two talks:
I. Nets: linear logic proof-nets and pure proof-nets for the lambda
calculus. Correctness criteria. Dynamics: can we eliminate the use of
boxes and give graph rewriting system with no global rules?
II. Sharing and optimal reductions. Paths and GOI. Local and
asynchronous implementation of the beta reduction.
Directions in Object-Oriented Programming Languages:
Type Systems and Language Development
Modern programming projects involve hundreds of programmers
and millions of lines of code. Object-oriented programming languages
(OOPL's) offer several powerful language features to help manage the
difficulties of such large-scale programming. Not surprisingly, these
powerful mechanisms interact in subtle ways, making good language
One of the most problematic issues has been the relationship between
subtyping and inheritance, two code-reuse mechanisms. Existing
languages combine the mechanisms, limiting subtyping to those object
types related via inheritance. This limitation greatly restricts the
subtype polymorphism of such languages, preventing code reuse. It
also forces programmers to use complex multiple inheritance mechanisms
to produce desired subtyping relationships. Past studies have pointed
out that subtyping and inheritance are conceptually distinct,
suggesting they should be separated. In this talk, I will argue that
the confusion regarding the relationship between subtyping and
inheritance stems from the fact that there are two different forms of
object type being used here. "Interface types", used in analytical
studies, specify only the messages their objects understand. Such
types are useful because they support a high degree of subtype
polymorphism, enabling code reuse. In contrast, "implementation
types", used in practice, constrain hidden aspects of their objects'
implementations, limiting polymorphism but enabling more efficient
message sending and more useful binary methods.
In this talk, I will present a provably sound type-theoretic
foundation for object-oriented languages that includes both interface
and implementation types, allowing the benefits of both forms of
object type to be realized in the same language. This framework
reveals that although subtyping and inheritance are distinct for
interface types, they are unified for implementation types. The
system also suggests that implementation types may be viewed as
*subtypes* of the interface types obtained by "forgetting" the
implementation constraints. This subtyping relationship enables
objects to be manipulated efficiently in contexts that know their
implementation constraints, while allowing them to be treated
polymorphically in contexts that know only interface information.
Almost surely consensus
University of South Florida
Random graphs of various kinds are being used in many places
these days. Theoretical biologists are looking at random
subgraphs of hypercubes, statisticians are looking at random
graphs in Euclidean space, and computer scientists are deep
in the traditional Erd\"os-R\'enyi model. And so on. In
many such models a nice graphical property will be almost surely true
(or almost surely false) on large graphs, where `nice' means `definable
in some nice logic': we say that this model has a `zero-one
law' for that nice logic. We will look at some useful models
that tend to produce sprawling, somewhat homogeneous graphs,
and show how to use `pebble games' to establish zero-one laws.
We will also talk about random graphs and the meaning of life.
Forcing and computational complexity
University of Illinois and University of Pennsylvania
In this talk I will first give an expository mini course on forcing,
nonstandard models of arithmetic and bounded arithmetic. I will not
assume any knowledge about them.
Then I will show that forcing on nonstandard model of bounded
arithmetic is closely related to the computational complexity problems,
e.g., P=NP problem, and fundamental one-way function problems in
Comparing Object Encodings
Benjamin C. Pierce
The past five years have seen an explosion of foundational models for
statically typed object-oriented programming. Many have been
presented as translations from high-level object notations to typed
lambda-calculi with subtyping, differing in technical details but
sharing underlying intuitions. This tutorial lecture develops a
uniform notational framework -- a typed lambda-calculus with
subtyping, higher-order polymorphism, existential types, and recursive
types -- and uses it to compare and contrast four previously studied
[Joint work with Kim Bruce and Luca Cardelli.]
Type inference in systems of recursive types
University of Pennsylvania
We present a new method for performing type inference in languages
with recursive types and subtyping. The method has been applied to a
class of lambda-calculus-based type systems, as well as an object type
system with record subtyping and variance annotations. A key
technical detail is that we define the subtyping relation using
simulations, which leads to a much simpler algorithm for subtyping
than previously known. This is joint work with Jens Palsberg.
Pizza into Java: Translating theory into practice
Pizza is a strict superset of Java that incorporates three ideas from
the functional programming community: parametric polymorphism, higher-order
functions, and algebraic data types.
Pizza is defined by translation into Java and compiles into the Java
Virtual Machine, requirements which strongly constrain the design
space. Nonetheless, Pizza fits smoothly to Java, with only a few rough
edges. This is joint work with Martin Odersky.
Meta-Pi: A Family of Specification Languages
University of Pennsylvania
A number of specification languages have been designed to aid in the
modelling of communication. One problem that users of such languages
frequently face is that the language doesn't provide all the operations
desired for a particular problem. Simulating these operations results in
unwieldy specifications, while extending the language requires extensive
proofs that the resulting language is sensible.
We address this issue by proposing the Meta-Pi family of specification
languages. Meta-Pi is a meta-language: a language in which you construct
other languages. In order to define a Meta-Pi language, one describes all the
operations one desires using a particular rule format. Any such language is
guaranteed to possess essential properties, such as respecting bisimulation.
The rule format is entirely syntactic -- one can determine whether an
operation is in the Meta-Pi format statically. This allows a specification
language to be easily tailored to a problem.
Coherence completions of categories
and game semantics for linear logic
University of Pennsylvania
Since linear logic was introduced by Jean-Yves Girard in 1987, many
different approaches of semantic paradigms for linear logic have been
developed, but no canonical theory has
emerged. In this two-lecture series we present coherence completions
of categories, with
the aim of developing a unified theory encompassing various semantics of
linear logic. We will first discuss all necessary background from
lattice theory and from category theory.
The starting point of the present work is based on
the softness in coherence spaces. The concept of softness appeared in the
study of free bicomplete categories as a categorical generalization of
Whitman's condition on lattice theory. Softness is a structural
rule concerning morphisms from limits into colimits.
In the case of lattice theory, limits and colimits are viewed as meets
and joins, respectively. In coherence spaces softness has the
the following consequence: each linear morphism from the conjunction (product)
into the disjunction (coproduct) factors throught either a product projection
or a coproduct injection. We show that the full subcategory of the category of
coherence spaces whose objects are generated from the singleton
space under products and coproducts is exactly the free bicomplete category of
the singleton under the zero object and products and coproducts.
The major step we take here is to extend coherence spaces to coherence
completions of categories. We show that if a category is a model of
linear logic, then so is its coherence completion. In order to interprete
the connectives of linear logic in the coherence completion, we present
the coherence completions as a monad on the category of categories and
A key idea explored in the present work is the enriched softness between
products and coproducts. This important feature is directly related to
the associativity of winning strategies of games. We show that
the enriched softness provides a convenient basis for game semantics.
Parts of this work are based on collaboration with André Joyal.
A Logic for Reasoning with Higher-Order Abstract Syntax
University of Pennsylvania
Logical frameworks based on intuitionistic or linear logics with
higher-type quantification have been successfully used to give
high-level, modular, and formal specifications of many important
judgements in the area of programming languages and inference systems.
Given such specifications, it is natural to consider proving
properties about the specified systems in the framework: for example,
given the specification of evaluation for a functional programming
language, prove that the language is deterministic or that the
subject-reduction theorem holds. One challenge in developing a
framework for such reasoning is that higher-order abstract syntax
(HOAS), an elegant and declarative treatment of object-level
abstraction and substitution, is difficult to treat in proofs
involving induction. In this talk I will present a meta-logic that
can be used to reason about judgements coded using HOAS; this
meta-logic is an extension of a simple intuitionistic logic that
admits quantification at higher types and simply typed lambda-terms
(key ingredients for HOAS) as well as induction and a notion of
definition. The latter concept of a definition is a proof-theoretic
device that allows certain theories to be treated as "closed" or as
defining fixed points. The resulting meta-logic can specify various
logical frameworks and a large range of judgements regarding
programming languages and inference systems. I will illustrate this
point through examples, including the admissibility of cut for a
simple logic and subject reduction, determinacy of evaluation, and the
equivalence of SOS and natural semantics presentations of evaluation
for a simple functional programming language.