Intermediate Representation
We say that a language is compiled if the translator analyzes it thoroughly (rather than effecting some "mechanical" transformation), and if the intermediate program does not bear a strong resemblance to the source. These two characteristics—thorough analysis and nontrivial transformation—are the hallmarks of compilation.
We say that a knowledge point is comprehended if the you analyze it thoroughly (rather than echoing what the books say), and if the concept generated in your brain does not bear a strong resemblance to the text. These two characteristics—thorough analysis and nontrivial transformation—are the hallmarks of comprehension.

  1. 2019/08/20 - Cubical Cold Introduction (1) -- Squares and Diagonals
  2. 2019/08/01 - Cubical Cold Introduction (0) -- Paths and Intervals
  3. 2019/07/14 - PLT Structural typing and first-class case expressions
  4. 2019/06/20 - PLT Type inference under dependent type (meta variables)
  5. 2019/05/22 - Haskell Interpreter without an AST
  6. 2019/04/21 - PLT Different styles of equality reasoning
  7. 2019/04/07 - PLT Fragmented Thoughts on Reducible Expressions
  8. 2018/11/16 - PLT The World Over Dependent Types
  9. 2017/11/12 - Kotlin Tricks in using Kotlin `internal`