A comparison of formulations of modal type systems in Kripke and Fitch styles

An explanation of why I separate decidability analysis and algorithmic analysis into Agda and Coq in the technical work of my master's thesis.

Study subtyping in an algebraic approach!

A comparison between different versions of Dependent Object Types (DOTs). The thought put in this blog might or might not be published in the future, but nonetheless something worth mentioning before I entirely forget about it.