\gdef\jty{\:\mathrm{ty}} \gdef\jprop{\:\mathrm{prop}} \gdef\jtrue{\:\mathrm{true}} \gdef\yields{\vdash} \gdef\ms#1{\mathsf{#1}} \gdef\Open#1{{\Large \circ}{#1}} \gdef\Close#1{{\Large \bullet}{#1}} \gdef\OpenEta{\eta^{\circ}} \gdef\CloseEta{\eta^{\bullet}} \gdef\isStatic#1{\mathrm{isStatic}(#1)} \gdef\isDynamic#1{\mathrm{isDynamic}(#1)} \gdef\ite#1#2#3{\mathbf{if}\:\:#1\:\:\mathbf{then}\:\:#2\:\:\mathbf{else}\:\:#3}

Abstract interpretation

for

Semi-dependent type theories

December 9, 2025, Berkeley Seminar

Owen Lynch