Janus Troelsen#neuhier I previously lived in Darmstadt, but now I live in Mexico. I participate in a Discord-based reading group for the Types and Programming Languages book, we just finished covering Simply Typed Lambda Calculus. If interesting, please let me know and I can help get you up to speed and you can join us.
HoldMyType@janus how about stratified lambda calculus - axiom of restricted comprehension?
System F stratification — polymorphic λ-calculus where types and terms live at different levels
Predicative stratification — Coq/Agda style universes (Type₀ : Type₁ : Type₂ ...) to avoid Girard's paradox
Elementary Affine Logic / Bounded Linear Logic — stratification to control complexity (terms reduce in bounded time
/Quasi related /not vetted
https://mathstodon.xyz/@xameer/116249300428180520
Predicative stratification — Coq/Agda style universes (Type₀ : Type₁ : Type₂ ...) to avoid Girard's paradox
Elementary Affine Logic / Bounded Linear Logic — stratification to control complexity (terms reduce in bounded time
/Quasi related /not vetted
https://mathstodon.xyz/@xameer/116249300428180520
HoldMyType (@[email protected])
@[email protected] how about stratified lambda calculus - axiom of restricted comprehension?