Abstracts of the lectures at the School in Logic and Computation

Heriot-Watt University, Edinburgh

10-13 April 1999

ULTRA logo ULTRA group
Useful Logics, Types, Rewriting,
and Applications		 UKII logo 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 syntax-independent constructions of fully abstract models for a spectrum of programming languages ranging from purely functional languages to languages with non-functional features such as control operators and references. There are also applications to the semantics of branching quantifiers and ``independence-friendly'' 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 Martin-Lof'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 Russell-Prawitz second order representation of the logical operations on the impredicative type Prop, rather than the Curry-Howard propositions-as-types 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: proof-checking
  • First the mission of the proof-checking 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 non-trivial 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 Dezani-Ciancaglini 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, Levy-Longo trees, Bohm trees, Bohm trees modulo finite or infinite eta-expansions. 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 non-deterministic 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 Higher-order 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 Turing-complete, so such programs compute everything computable: all the partial recursive functions. A classic Turing-incomplete 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 higher-order 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 ``read-only,'' i.e., constructor-free programs, and RW stands for ``read-write.''

    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.

    Jan-Willem 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 first-order 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 Fraenkel-Mostowski permutation model of set theory with atoms (FM-sets) can serve as the semantic basis for a meta-logic for specifying and reasoning about formal systems involving name-binding, alpha-conversion, capture-avoiding substitution, etc. Working in a suitable axiomatization of FM-sets, we show that this setting can express statements quantifying over `fresh' names and we use this to give a novel set-theoretic interpretation of name abstraction. Inductively defined FM-sets invovling this abstraction set-former (together with cartesian product and disjoint union) can correctly encode object-level syntax modulo alpha-conversion. 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 syntax-manipulating functions (such as capture-avoiding 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 Curry-Howard Isomorphism: Remarks on Recursive Types
  • The second-order lambda-calculus can be extended by Church-style recursive types in various ways. We discuss and compare several such definitions from the point of view of the Curry-Howard 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 higher-order logic.

    Maintained by Fairouz Kamareddine ( ),