KnowledgeBase » SEMINAR » ID = 738

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.