PAR on Thursday, July 15th

09:00‑10:00 Session 1
Location: IF G.07
09:00 Alexander Krauss
Recursive Definitions of Monadic Functions

Using standard domain-theoretic fixed-points, we show how to define recursive functions that are formulated in monadic style, for monads that provide a notion of abnormal termination. Unlike in the general case, the unconditional recursive specification is never inconsistent, even if the function is partial. This is particularly useful for recursive programs that manipulate a heap, using the imperative programming extension of Isabelle/HOL. The construction is easy to automate, and suitable induction principles can be derived automatically.

10:30‑12:30 Session 2
Location: IF G.07
10:30 Andreas Abel
Integrating Sized and Dependent Types

Sized types are a modular and theoretically well-understood tool for checking termination of recursive and productivity of corecursive definitions. The essential idea is to track structural descent and guardedness in the type system to make termination checking robust and suitable for strong abstractions like higher-order functions and polymorphism.

To study the application of sized types to proof assistants and programming languages based on dependent type theory, we have implemented a core language with explicit handling of sizes. New considerations were necessary to soundly integrate sized types with dependencies and pattern matching, which was made possible by modern concepts such as inaccessible patterns and parametric function spaces.

11:00 Thorsten Altenkirch and Nils Anders Danielsson
Termination Checking Nested Inductive and Coinductive Types

In the dependently typed functional programming language Agda one can easily mix induction and coinduction. The implementation of the termination/productivity checker is based on a simple extension of a termination checker for a language with inductive types. However, this simplicity comes at a price: only types of the form νX.μY.F X Y can be handled directly, not types of the form μY.νX.F X Y. We explain the implementation of the termination checker and the ensuing problem.

11:30 Nils Anders Danielsson
Beating the Productivity Checker Using Embedded Languages

Some total languages, like Agda and Coq, allow the use of guarded corecursion to construct infinite values and proofs. Guarded corecursion is a form of recursion in which arbitrary recursive calls are allowed, as long as they are guarded by a coinductive constructor. Guardedness ensures that programs are productive, i.e. that every finite prefix of an infinite value can be computed in finite time. However, many productive programs are not guarded, and it can be nontrivial to put them in guarded form.

This paper gives a method for turning a productive program into a guarded program. The method amounts to defining a problem-specific language as a data type, writing the program in the problem-specific language, and writing a guarded interpreter for this language.

12:00 Tarmo Uustalu
Antifounded coinduction in type theory

Venanzio Capretta, Varmo Vene and I have previously studied antifounded algebras as a a category-theoretic formulation of antifounded coinduction. These are the dual of wellfounded coalgebras, a category theorist's take on wellfounded induction, closely related to the Bove-Capretta method for justifying function definitions by general recursion in type theory.

In this talk, we discuss one possible type-theoretic approach to antifounded coinduction.

14:00‑15:00 Session 3
Location: IF G.07
14:00 Conor McBride
Djinn, monotonic

I'll give a talk about modular presentations of recursion schemes, with application to Dyckhoff's proof search algorithm.

15:30‑17:30 Session 4
Location: IF G.07
15:30 Claudio Sacerdoti Coen and Silvio Valentini
General recursion and formal topology

It is well known that general recursion cannot be expressed within Martin-L\"of's type theory and that various approaches have been proposed to overcome this problem still maintaining the termination of the computation of the typable terms. In this work we propose a new approach to this problem based on the use of inductively generated formal topologies.

16:00 Aaron Stump, Vilhelm Sjöberg and Stephanie Weirich
Termination Casts: A Flexible Approach to Termination with General Recursion

This paper proposes a type-and-effect system called Teqt, which distinguishes terminating terms and total functions from possibly diverging terms and partial functions, for a lambda calculus with general recursion and equality types. The central idea is to include a primitive type-form ``Terminates t'', expressing that term t is terminating; and then allow terms t to be coerced from possibly diverging to total, using a proof of Terminates t. We call such coercions termination casts, and show how to implement terminating recursion using them. For the meta-theory of the system, we describe a translation from Teqt to a logical theory of termination for general recursive, simply typed functions. Every typing judgment of Teqt is translated to a theorem expressing the appropriate termination property of the computational part of the Teqt term.

16:30 Issam Maamria and Michael Butler
Rewriting and Well-Definedness within a Proof System

Term rewriting has a significant presence in various areas, not least in automated theorem proving where it is used as a proof technique. Many theorem provers employ specialised proof tactics for rewriting. This results in an interleaving between deduction and computation (i.e., rewriting) steps. If the logic of reasoning supports partial functions, it is necessary that rewriting copes with potentially ill-defined terms. In this paper, we provide a basis for integrating rewriting with a deductive proof system that deals with well-definedness. The definitions and theorems presented in this paper are the theoretical foundations for an extensible rewriting-based prover that has been implemented for the set theoretical formalism Event-B.

17:00 Gavin Mendel-Gleason and Geoff Hamilton
Cyclic Proofs and Coinductive Principles

It is possible to provide a proof for a coinductive type using a corecursive function coupled with a guardedness condition. The guardedness condition, however, is quite restrictive and many programs which are in fact productive and do not compromise soundness will be rejected. We present a system of cyclic proof for an extension of System $F$ extended with sums, products and (co)inductive types. Using program transformation techniques we are able to take some programs whose productivity is suspected and transform them, using a suitable theory of equivalence, into programs for which guardedness is syntactically apparent. The equivalence of the proof prior and subsequent to transformation is given by a bisimulation relation.