Dependency Tracking and Dependent Types

Dependency tracking is a static analysis that determines how computations depend on their inputs. Dependent types, on the other hand, allow static types to depend on and be determined by program values. This dissertation describes my work on designing expressive dependently typed systems where useful features such as relevance tracking and termination tracking are supported uniformly through the mechanism of dependency tracking. First, it presents System DE, a dependently typed language that leverages dependency tracking to split the language into two fragments: a flexible programming language that supports general recursion and a restricted proof language that can be used to extrinsically reason about program equivalence in a consistent way. Second, it presents DCOI, an extension of Barendregt's pure type systems with a general form of dependency tracking. DCOI leverages dependency information for run-time erasure and compile-time irrelevance. By internalizing indistinguishability, a level-indexed equivalence relation found in dependency tracking, DCOI gives programmers more control during equational reasoning. Third, it demonstrates that DCOIOmega, an instantiation of DCOI with a predicative universe hierarchy, is suitable as a program logic. It establishes logical consistency and normalization with a logical predicate. From normalization, it derives the decidability of type conversion. Finally, it presents a proof technique for the decidability of type conversion that combines a minimal logical predicate and syntactic results about confluence that are type-system agnostic. The proof technique is not only amenable to mechanization, but also extensible to DCOI's untyped, level-annotated equational theory and eta-laws for functions and pairs. All type systems and metatheoretic results described in this dissertation have been fully mechanized in the Rocq theorem prover.

Author dc:creator

• Liu, Yiyun

Advisor dc:contributor.advisor

• Weirich, Stephanie

• Computer Sciences

Language dc:language.iso

en

Repository record dc:identifier.uri

https://repository.upenn.edu/handle/20.500.14332/62715

OAI identifier oai:identifier

oai:repository.upenn.edu:20.500.14332/62715