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:** 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.