A Complement of My Thesis: Naming Conventions and Choice of Proof Assistants
An explanation of why I separate decidability analysis and algorithmic analysis into Agda and Coq in the technical work of my master's thesis.
Subtyping with Algebra
Study subtyping in an algebraic approach!
Comparison Between Different DOTs
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.