KnowledgeBase » SEMINAR » ID = 740

Coinduction in Coq

by Abhishek Anand
2014

This is continuation of the Seminar on CoInductive types, which was held 3 weeks ago. Abhishek will continue the discussion of Coq's CoInductive types and conclude this part by explaining a well-known CoInductive construction, which shows that type preservation does not hold in Coq.

He will then switch gears and show how to define the Howe's computational equality in Coq using CoInduction. He will discuss the proof that this definition is equivalent to another, perhaps simpler one which does not use CoInduction. Finally, he will explain where the proof will break if one added some non-deterministic constructs to Nuprl.