1 option
Dependency tracking and dependent types Yiyun Liu
- Format:
- Book
- Thesis/Dissertation
- Author/Creator:
- Liu, Yiyun, author.
- Language:
- English
- Subjects (All):
- Computer science.
- Computer engineering.
- Information science.
- 0984.
- 0464.
- 0723.
- Local Subjects:
- Computer science.
- Computer engineering.
- Information science.
- 0984.
- 0464.
- 0723.
- Genre:
- Academic theses
- Physical Description:
- 1 online resource (195 pages)
- Contained In:
- Dissertations Abstracts International 87-12A
- Place of Publication:
- Ann Arbor : ProQuest Dissertations and Theses, 2026
- Language Note:
- English
- Summary:
- 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 DCOIω, 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 η-laws for functions and pairs.All type systems and metatheoretic results described in this dissertation have been fully mechanized in the Rocq theorem prover
- Notes:
- Source: Dissertations Abstracts International, Volume: 87-12, Section: A.
- Advisors: Weirich, Stephanie Committee members: Pierce, Benjamin C; Zdancewic, Stephen A.; Tannen, Val; Tabareau, Nicolas
- Ph.D. University of Pennsylvania 2026
- Vendor supplied data
- Local Notes:
- School code: 0175
- ISBN:
- 9798247973157
- Access Restriction:
- Restricted for use by site license
The Penn Libraries is committed to describing library materials using current, accurate, and responsible language. If you discover outdated or inaccurate language, please fill out this feedback form to report it and suggest alternative language.