Notes

type system of haskell with rank-2 extension is impredicative , allows partial types , whereas partial monads can be used for operational semantics

agda is predicative , so a type constructor can't quantify over the same universe it occupies

Say you have a set of objects and a set of relations which can exist among them, can you decidably tell how each of them is related to everyone else in their set? Always?

how ll you do this with

stratified lambda calculus - book

stratified lob theorem - paper

another paper , i can't name atm

cumulative vs non cumulative types

Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq