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!