Workshop in Termination and Type Theory

Göteborg 14-15 November 2002

EC TYPES Working Group (IST-1999-290001-TYPES)


Talks and Abstracts

Participant: Andreas Abel (joint work with Ralph Matthes and Tarmo Uustalu)
Talk: Generalized Iteration and Coiteration for Higher-Order Nested Datatypes
Abstract:

We solve the problem of defining generalized iteration (generalized in the direction of generalized folds by Bird and Paterson) and its dual for inductive and coinductive constructors (nested datatypes) of {\em arbitrary} rank by appropriately generalizing Mendler-style (co)iteration. Characteristically to Mendler-style schemes of disciplined (co)recursion, the schemes we propose do not rest on notions like positivity or monotonicity of a constructor and facilitate programming in a natural and elegant style close to programming with the customary \texttt{letrec} construct, where the typings of the schemes, however, guarantee termination. For rank~2, a smoothened version of Bird and Paterson's generalized folds and its dual are achieved, for rank 1, the schemes instantiate to Mendler's original (re)formulation of iteration and coiteration. Several examples demonstrate the power of the approach. Strong normalization of our proposed extension of system~$\Fomega$ of higher-order parametric polymorphism is proven by a reduction-preserving embedding into pure~$\Fomega$.


Participant: Klaus Aehlig
Talk: Types for Finitely Iterated Inductive Definitions
Abstract:

We consider the fragment of the polymorphic lambda calculus (``System F'') where all types are built (up to alpha-conversion) from a single type variable only. This fragment is expressible enough for most ``real world'' data structures including the finite tree classes. It is shown how this fragment can be reduced to finitely iterated inductive definitions.


Participant: Thorsten Altenkirch
Talk: Generalized General Recursion
Abstract:


Participant: Gilles Barthe
Talk: Type-based Termination of Recursive Definitions --- The Calculus of Constructions
Abstract:


Participant: Ulrich Berger
Talk: Proving Termination by Update-induction
Abstract:


Participant: Yves Bertot
Talk: Type-theoretic Functional Semantics
Abstract:

We describe the operational and denotational semantics of a small imperative language in type theory with inductive and recursive definitions. The operational semantics is given by natural inference rules, implemented as an inductive relation. The realization of the denotational semantics is more delicate: The nature of the language imposes a few difficulties on us. First, the language is Turing-complete, and therefore the interpretation function we consider is necessarily partial. Second, the language contains strict sequential operators, and therefore the function necessarily exhibits nested recursion. Our solution combines and extends recent work by the authors and others on the treatment of general recursive functions and partial and nested recursive functions. The first new result is a technique to encode the approach of Bove and Capretta for partial and nested recursive functions in type theories that do not provide simultaneous induction-recursion.

A second result is a clear understanding of the characterization of the definition domain for general recursive functions, a key aspect in the approach by iteration of Balaa and Bertot. In this respect, the work on operational semantics is a meaningful example, but the applicability of the technique should extend to other circumstances where complex recursive functions need to be described formally.


Participant: Frederic Blanqui
Talk: Type Theory and Rewriting
Abstract:

I will present general syntactic conditions ensuring the strong normalization of the Calculus of Constructions extended with functions and predicates defined by higher-order rewrite rules.


Participant: Ana Bove (joint work with Venanzio Capretta)
Talk: Modelling General Recursion in Type Theory
Abstract:

General recursive algorithms satisfy no syntactic condition that guarantees termination and therefore there is no direct way of formalising such algorithms in type theory. On the other hand, functional programming impose no restrictions on recursive programs, and then writing a general recursive algorithm is straightforward. However, there is no powerful framework that allows us to reason about the correctness of functional programs.

The goal of this talk is to present a method that combines the advantages of both programming styles when formalising general recursive algorithms. In this way, a short algorithm that can be proven correct by using the expressive power of type theory would be obtained.


Participant: Venanzio Capretta
Talk: General Recursion via Coinductive Types
Abstract:

The talk presents a formalization of partial recursive functions in Type Theory. To every type A we associate a coinductive type A' of possibly infinite computations of type A. A recursive function from A to B is represented by an element of A -> B'.


Participant: Pietro Di Gianantonio (joint work with Marino Miculan)
Talk: A Unifying Approach to Recursive and Co-recursive Definitions
Abstract:

In type theory based logical frameworks, recursive and co-recursive definitions are subject to syntactic restrictions that ensure their termination and productivity. These restrictions however greately decrease the expressive power of the language. In this work we propose a general approach for systematically defining fixed points for a broad class of well given recursive definition. This approach unifies the ones based on well-founded order to the ones based on complete metrics and contractive functions, thus allowing for mixed recursive/corecursive definitions. The resulting theory, implemented in the Coq proof assistant, is quite simple and hence it can be used broadly with a small, sustainable overhead on the user.


Participant: Arne John Glenstrup
Talk: Size-change Termination Principle in Partial Evaluation
Abstract:


Participant: Felix Joachimski
Talk: Normalization for eta-Expansion in Pure Type Systems
Abstract:

We give a detailed analysis of the interaction between beta-reduction and eta-expansion in the simply-typed lambda-calculus that leads to a modular and purely syntactic proof of strong normalization of the combination of the two reductions. It is shown how this technique extends to beta-normalizing functional Pure Type Systems with a restricted variant of Barthe's formulation of eta-expansion.


Participant: Ralph Matthes
Talk: Strong Normalization for Nested (Co-)Recursion
Abstract:


Participant: Conor McBride (joint work with James McKinna)
Talk: Seeing and Doing
Abstract:

Many algorithms of much less complexity than a bootstrapping interpreter fail, at first glance, to fit the restrictive paradigm of `structural recursion', in which termination is guaranteed by typechecking. The reason is that the structures of these algorithms are not visible in the programs which implement them. The traditional `separation of concerns' approach to this problem is to recover these structures `after the fact' by ad hoc termination proofs. However, dependent types can equip data with much more visible structure. This suggests that we should also consider the possibility of implementing algorithms by new programs which make enough of their structure visible to get termination `for free'.


Participant: James McKinna (joint work with Conor McBride)
Talk: Views for Recursion
Abstract:


Participant: Tarmo Uustalu
Talk: Recursion Schemes from Comonads a la Mendler
Abstract:

Uustalu, Vene and Pardo and Bartels have shown that a number of seemingly unrelated advanced disciplined recursion schemes are instances of a generic scheme parameterized by a comonad and a distributive law of the base functor of the inductive type of interest over the comonad. What is more, it even suffices to have a functor instead of the comonad; in that case, a comonad (the cofree comonad of the functor) shows up in the background. It makes sense to try to support these semantically justified generic schemes in a typed lambda calculus via language primitives. This, however, is a bit tricky, since the straightforward codings employing positivity or monotonicity of a type constructor are not really elegant. We show that N. P. Mendler's approach to coding disciplined recursion schemes, in which neither notion is needed, is fruitfully applicable also to comonad-specified recursion.


Participant: Paul J. Voda
Talk: What Do We Gain by Integrating a Programming Language with a Theorem Prover?
Abstract:

Beside the obvious gains of having a good declarative semantics for the programming language (Why to integrate otherwise?) and of computer-aided proofs of properties of programs (such as their conformance with their specifications) we can design the language with a massively extensible syntax.

We will first illustrate the current state of art with the programming language CL designed and implemented in Bratislava. The formal theory of CL is the simplest of formal theories: Peano Arithmetic (PA). Definitions of functions and predicates are just formulas of PA which conservatively extend PA by definitions. Although a first-order language, CL is not a toy language because it has been used for six years now in the undergraduate teaching at the University of Bratislava. Up to 300 students pass yearly through the four courses based on CL.

CL has a wide set of pattern matching constructs which go far beyond the ones known from the functional programming languages. The advantage of pattern matching over the traditional case (if-then-else) constructs lies in the vastly increased readability of programs. In addition, the programs obtain a mathematical look and feel. We will illustrate this point with a brief demo of CL during the talk. The current implementation of CL has a fixed set of pattern matching constructs (we call them discriminators ).

The main topic of the talk is a proposal of how to make pattern matching extensible. User-defined discriminators must be proved correct in PA before they can be used in definitions of functions and predicates. Since discriminators can be conditional (the ones implemented in the current CL are unconditional), they may be used in definitions only when their conditions are met. This must be again demonstrated by a proof (by so-called proof obligations).


Participant: David Wahlstedt
Talk: A Small Language with Dependent Types, General Recursion and Size-change Termination
Abstract:



If you have any further questions, please mail bove@cs.chalmers.se.

Page last modified on November 12, 2002 by Ana Bove.