Termination Checking In The Presence Of Mixed Induction And Coinduction
Stc
Date: 2010-06-24
Time: 11:00
Room:
BBL 023
Speaker: Steven Keuchel
Title: Termination checking in the presence of mixed induction and coinduction
Abstract
Nowadays coinduction is widely used in computer science to formally
define and reason about potentially infinite structures. Amongst other
things it is used for streams and other infinite data types, describing
communication systems and concurrency and defining subtyping relations
for recursive types. Purely coinductive defined structures might
be too infinite, so that a mix of induction and coinduction becomes
necessary. In Agda, a dependently typed functional programming language
and proof assistant, one can define and reason about programs working
on mixed inductive and coinductive data types. At the same time Agda
strives to be a total language: all programs must terminate. In this
talk an introduction to codata and corecursion is given and the
termination checking process currently used in Agda for functions
using mixed inductive and coinductive data is described.
