ionchy/rqual
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
research qualifier https://www.cis.upenn.edu/graduate/program-offerings/doctoral-program/requirements/#:~:text=Research%20Qualifier
45 commits 1 branch 0 tags 3.9 MiB
Find a file
Exact
Jonathan Chan e8c7e11c5d Use Git LFS for PDFs
2025-01-01 14:54:14 -05:00
.vscode Initial commit 2024-10-30 16:29:17 -04:00
.gitattributes Use Git LFS for PDFs 2025-01-01 14:54:14 -05:00
.gitignore Initial commit 2024-10-30 16:29:17 -04:00
jsgrf.pdf Use Git LFS for PDFs 2025-01-01 14:54:14 -05:00
jsgrf.tex Added JSGRF version 2024-11-19 15:33:39 -05:00
latexrun Initial commit 2024-10-30 16:29:17 -04:00
main.bib Markus comments 2024-11-14 18:22:50 -05:00
main.pdf Use Git LFS for PDFs 2025-01-01 14:54:14 -05:00
main.tex Added JSGRF version 2024-11-19 15:33:39 -05:00
README.md Update abstract to remove 'propose' 2024-11-05 11:42:50 -05:00

README.md

Research Qualifier – Jonathan Chan – 21 November 2024, 15:30

Title: Internalizing Extensions in Lattices of Type Theories
Date: 21 November 2024
Time: 15:30
Location: Singh 313
Committee: Steve Zdancewic (chair), Stephanie Weirich (advisor), Benjamin Pierce

Abstract:
While many proof assistants are founded upon common theoretical ground, they will also feature further extensions and axioms that augment their reasoning power. The individual theories based on each extension are individually sound, but how type checkers handle their interactions at compile time is not formally described. Furthermore, the way proof assistants currently enable extensions can be too coarse and imprecise when it comes to guarantees about the features a top-level definition may use.

A first step towards a framework of extensions could use the Dependent Calculus of Indistinguishability (DCOI) to formalize granular and precise extension tracking. DCOI is a type system with dependency tracking, where terms and variables are assigned dependency levels alongside their types. These dependency levels form a lattice that describes which levels are permitted to access what. This report explores how extensions could correspond to dependency levels, and how the lattice would describe how extensions are permitted to interact.