Swansea University
Computer Science

Photo of Fredrik Nordvall Forsberg

phone: (+44) (0)7787 959866
email: csfnf@swansea.ac.uk
office: Room 500

Fredrik Nordvall Forsberg
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP

Additional material for Inductictive-inductive definitions

Formalisation in Agda

We have formalised our development in Agda. As we are implementing an extension of type theory, we had to switch off both the positivity and the termination checker.

You can either download the agda file indind.agda, or have a look at the HTML version.

Extended version of article

The extended version differs from the submitted article in the following ways:

The extended version can be downloaded here.

E-mail page maintainer