Wednesday, December 8, 2021 - 2:00pm to 3:30pm
Location:In Person Newell-Simon 3305
Speaker:ZHIBO CHEN, Masters Student https://www.linkedin.com/in/zhibo-chen-8052a7133
Towards a Mixed Inductive and Coinductive Logical Framework
The invention of logical frameworks enables computers to check formal proofs. The main methodology of the logical framework LF and various extensions of LF is to reduce proofs to terms and proof checking to type checking. Formally, we define an encoding relation between the objects of the informal proof system and the objects of the logical framework, and we prove that the encoding is adequate in the sense that the encoding relation is a compositional bijection. Then, to check whether the proof is valid, we just need to check whether the encoded proof term is of the correct judgment type.
Despite the success of the logical framework LF and its extensions, there is one class of proofs that present difficulties when one tries to encode them. Infinitary proof systems, and circular proof systems in particular, provide natural ways to carry out induction and coinduction. However, since terms of LF and its extensions are all finite, there cannot be a direct natural encoding of infinitary proofs into those systems.
In order to solve this problem, we designed CoLF^1, the first order fragment of a novel mixed inductive and coinductive logical framework. We develop two type theories in succession, one with non-dependent types and the other with simple-dependent types. Each type theory consists of three components, a semantic theory of infinite terms, a semantic theory of rational terms in which type checking is decidable, and a syntactic theory, in which type checking is actually implemented. We then present two case studies, one on a subtyping system for recursive types, and the other on a calculus for circular proofs with inductive and coinductive definitions, and we explore to which extent that these systems have natural representations in CoLF1.
Frank Pfenning (Chair)