# * Topics in Type Theory *

## by Abhishek Anand, Robert L. Constable, Mark Bickford

2014

During this semester we will organize some PRL seminars to

explore foundational issues in type theory. The explorations will

at several points involve comparisons among the type theories of

Agda, Coq, and Nuprl.

This week Abhishek, Bob, and Mark will talk about co-inductive types

and co-induction principles as well as the meaning of induction and

co-induction. They will also discuss cases when these principles are

essential even though their computational content is trivial. They will

compare co-induction in Coq and Nuprl.