Lehr- und Forschungseinheit für Theoretische Informatik,
Institut für Informatik der Ludwig-Maximilians-Universität München

Verification of (Co)Iteration Schemes for Nested Datatypes in Coq

This is the homepage of the project work "Verification of (Co)Iteration Schemes for Nested Datatypes in Coq" made by Dulma Rodriguez and supervised by Ralph Matthes and Andreas Abel. It is an implementation of the systems developed in the paper "Iteration and Coiteration Schemes for Higher Order and Nested Datatypes" from Abel, Matthes and Uustalu in the proof assistant Coq.

Talks

1 July 2005
Presentation of the goals of the project at the Oberseminar der LFE Theoretische Informatik (slides)
13 January 2006
Presentation of the results of the project at the Oberseminar der LFE Theoretische Informatik (slides)

Download













Dulma Rodriguez