Abstracts of the lectures at the School in Logic and Computation
HeriotWatt University, Edinburgh
1013 April 1999

ULTRA group Useful Logics, Types, Rewriting,
and Applications 

UKII
UK Institute of Informatics,
UK 
The list of abstracts is as follows:
Samson AbramskyUniversity of Edinburgh
Concurrent Games and Full Completeness for Linear Logic
Game semantics has emerged as a powerful paradigm for giving semantics
to a variety of logical
systems and programming languages. It has been used to prove full
completeness results 
completeness at the level of proofs, not merely provability  and to
give the first
syntaxindependent constructions of fully abstract models for a spectrum
of programming
languages ranging from purely functional languages to languages with
nonfunctional features
such as control operators and references. There are also applications to
the semantics of
branching quantifiers and ``independencefriendly'' logics, which have
connections to the
semantics of natural language.
In this talk we will present a concurrent games model of Linear Logic,
and a full completeness result will be described.
Peter Aczel University of Manchester
What is the logical strength of the Lego and Coq Type Theories?
Both the Lego and Coq computer systems implement versions of the
Calculus of Constructions that also incorporate the characteristic
features of MartinLof's Constructive Type Theory  inductive types
and type universes. Users of Lego and Coq are able to develop
constructive mathematics in these type theories via the
RussellPrawitz second order representation of the logical operations
on the impredicative type Prop, rather than the CurryHoward
propositionsastypes representation that is standard when developing
mathematics in Constructive Type Theory.
In my talk I will discuss the relationship between these two
representations of logic and present results that relate a variety of
type theories such as those implemented in Lego and Coq with
corresponding systems of classical and intuitionistic axiomatic set
theories.
Henk Barendregt Catholic University of Nijmegen
Mission possible: proofchecking
First the mission of the proofchecking project will be stated. It is
not very different form the formulation of de Bruijn and the one of
the QED, but emphasizes several points. Then some difficulties will be
mentioned. It is expected, nevertheless, that nontrivial examples of
the mission can be fulfilled before long.
Robert Constable Cornell University
Applications of Classes and Types to Practical Verifications
This talk will discuss the use of Nuprl's class theory
as it applies in verifying group communications.
Dirk van Dalen
Utrecht University
The Mathematical Universe according to Brouwer
Contrary to traditional reports, Brouwer was not presenting just a
particular constructive version of mathematics  he had conceived an
overall philosophical viewpoint that covered all the aspects of man and the
world.
In this lecture I will show how his mystical views of 1905 contained the
basis for his intuitionistic position. In particular the introduction of
choice sequences was a natural and unavoidable consequence of his earlier
notion of "causal sequence". The consequences of his fundamental views for
mathematics and logic will be discussed.
Mariangola DezaniCiancaglini
University of Turin
The Lambda Calculus in Different Scenarios
Looking at the lambda calculus as a theory of "programs", we are naturally
lead to define what is, in a lambda term, a "stable relevant minimal information"
directly observable in the term. This is the token of information which cannot be altered
by further reductions but can only be afdded upon. If one organises all the stable relevant minimal information which can be obtained from a computation and orders it according to the order it produced, then it is quite natural to obtain a tree representation of the information implicit in the original term. There are many representations in the literature, depending on the possible notions of stable
relevant minimal information, the most commonly used being Berarducci trees, LevyLongo trees, Bohm trees,
Bohm trees modulo finite or infinite etaexpansions.
In this talk, we will focus on the relations between the tree representations of
the terms and the observational equivalences inside calculi obtained by adding parallel and nondeterministic
features to the pure lambda calculus. We will consider many aspects for this as
can be seen in full abstract.ps
Neil Jones<
(Diku, DK):
The Expressive Power of Higherorder Types or, Life without CONS
We study the expressive power of functional programming language
features by characterizing decision problems solvable with various
combinations of operations on data: constructors and
destructors; the order of data values: 0, 1, or higher; and
program control structures: general recursion, tail recursion,
primitive recursion.
Many combinations are Turingcomplete, so such programs compute
everything computable: all the partial recursive functions. A classic
Turingincomplete language is got by restricting data to order 0
and control to ``fold.'' Such programs compute
the primitive recursive functions.
The table shows the effect of higherorder types on the
computing power of programs of type [Bool]>Bool. Each
entry is a complexity class: the collection of decision problems
solvable by programs restricted by row and column indices. RO
stands for ``readonly,'' i.e., constructorfree programs, and RW stands
for ``readwrite.''
Assaf Kfoury Boston
University
Some New Developments in Unification Related to Type Theory
Claude Kirchner Loria, Nancy:
Theorem Proving Modulo
Based on joint work with Gilles Dowek and Therese Hardin, ``Theorem
proving modulo'' is a way to remove computational arguments from
proofs by reasoning modulo a congruence on propositions. Such a
technique, issued from automated theorem proving, is of wider interest
because it permits to separate computations and deductions in a clean
way. I will first present a ``sequent calculus modulo'' that gives a
proof theoretic account of the combination of computations and
deductions.
Then, a complete proof search method, called ``Extended Narrowing and
Resolution'' (ENAR), for theorem proving modulo such congruences will
be presented. The completeness of this method is proved with respect
to the provability in sequent calculus modulo.
In many cases, rewrite rules and equations just relate terms. Applying
rewrite rules directly to propositions is of prime interest in many
examples, and I will show a few.
JanWillem Klop<
Free University of Amsterdam
Origin Tracking in Term Rewriting
This talk is about joint work with Roel de Vrijer and Inge Bethke.
Origin tracking involves looking at ancestors of
symbols and subterms in a reduction,
in a way that is more refined than the
classical notion of ancestor and descendant.
We present three applications of origin tracking
in term rewriting:
  in firstorder orthogonal term rewriting; we derive
the theorem of Huet and Le'vy about needed reductions;
  in lambda calculus; we give an origin tracking proof
of the Genericity Lemma;
  in infinitary lambda calculus; we give an origin tracking
proof of Berry's Sequentiality Theorem.
Andrew Pitts,
Cambridge University Computer Laboratory
A New Approach to Abstract Syntax Involving Binders
The FraenkelMostowski permutation model of set theory with atoms
(FMsets) can serve as the semantic basis for a metalogic for
specifying and reasoning about formal systems involving namebinding,
alphaconversion, captureavoiding substitution, etc. Working in a
suitable axiomatization of FMsets, we show that this setting can
express statements quantifying over `fresh' names and we use this to
give a novel settheoretic interpretation of name
abstraction. Inductively defined FMsets invovling this abstraction
setformer (together with cartesian product and disjoint union) can
correctly encode objectlevel syntax modulo alphaconversion. In this
way, the standard theory of algebraic datatypes extends to encompass
signatures invovling binding operators. In particular, there is an
associated notion of primitive recursion for defining
syntaxmanipulating functions (such as captureavoiding substitution,
set of free variables, etc) and a notion of proof by structural
induction, both of which remain pleasingly close to informal practice.
The talk is based on joint work with Jamie Gabbay (DPMMS, Cambridge
University).
Pawel Urzyczyn,
University of Warsaw
The CurryHoward Isomorphism: Remarks on Recursive Types
The secondorder lambdacalculus can be extended by Churchstyle
recursive types in various ways. We discuss and compare several
such definitions from the point of view of the CurryHoward
correspondence. This is possible because recursive types in system F
can be seen as propositional level counterparts (via dependency
erasing maps) of predicates defined as fixpoints in higherorder logic.
Maintained by
Fairouz Kamareddine
( ),