The invention of logical frameworks enables computers to check formal proofs. The main methodology of the logical framework LF and various exten- sions 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¹ , 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 implementable. 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 CoLF¹.

90 pages

Thesis Committee:
Frank Pfenning (Chair)
Karl Crary

Srinivasan Seshan, Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu