Friday 23 July 2021, 3:00 PM, online: Inductive Aspects of Set-Theoretic Models of Sized CIC, Yufeng Li (University of Waterloo, Canada).

In proof assistants such as Coq, termination of recursive definitions in the underlying theory, CIC, is crucial for the purposes of logical consistency and strong normalisation. However, under the presence of a general recursor, one often has to impose a complicated syntactic criterion on the recursor body to ensure the recursion is well-founded. Sized types provides an alternative, type-based method of ensuring termination. In this talk, I outline how to construct a set-theoretic model of CIC with sizes, focusing on the inductive part and challenges encountered along the way. The set-theoretic model outlined in the talk has also been extended with reducibility candidates, from which the logical consistency and strong normalisation of sized CIC was deduced.