🎉 My thesis is officially submitted! 🎉 (this will be my tweet thread lmao) 

🎉 My thesis is officially submitted! 🎉
Sized Dependent Types via Extensional Type Theory: hdl.handle.net/2429/82209
I syntactically model Sizey ᴍᴄType Theory (STT) with higher-rank, bounded sizes in an extensional CIC (CIC🄔). A little more detail in 🧵 0/5

If you're familiar with sized types in Agda, there's 2 big features:

  • Higher-rank quantification (e.g. (∀α. τ) → σ) so you can pass around size-preserving functions
  • Bounded quantification (e.g. ∀α < s. τ) to make pattern-matching work and to avoid "semicontinuity" reqs 1/5

These two in particular are important bc a bunch of past work have one or the other (or neither, like our preprint on CIC*) but not both! So one of the goals of STT is to be a foundation for sized dependent types with both features and good metatheory, i.e. consistency 2/5

Proven w/ a syntactic model into CIC🄔: If well-typed STT terms translate to CIC🄔 terms with the translated type, then consistency of CIC🄔 implies that of STT
A neat thing is that fixpoints are well-founded induction on sizes bc they use bounded sizes
(Slide from SRC talk) 3/5

Since ∞ < ∞ isn't wf, I exclude ∞ from STT (that's what makes Agda's sized types inconsistent)
I talk a little about problems with that and failed solution attempts (some of it in my earlier blog post ionathan.ch/2021/08/04/sized-t)
So replacing ∞ is still an open problem 👀 4/5

But to conclude:
✅ Sizey ᴍᴄType Theory
✅ higher-rank and bounded sizes
✅ logical consistency
✅ syntactic model of sized dependent types works!
❌ ∞ bad. but ∞ useful... 5/5


so I posted about my thesis but not the paper. I see how it is

Sign in to participate in the conversation

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.