@a_breakin_glass I had been investigating certain type systems recently, but I was interested mostly in dependent type systems such as found in Coq or ATS