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. 2020/06/20 - Parser Lexer for two-dimensional syntax (in Alex)
  2. 2020/05/16 - Arend Language extensions of Arend
  3. 2020/05/14 - Arend Functional programming language -- Arend
  4. 2020/05/04 - Arend REPLs with Typed Holes
  5. 2020/03/03 - Tools Thoughts on literate programming tools
  6. 2020/01/19 - PLT Membership proofs and De Bruijn indices
  7. 2019/11/13 - Agda Thinking about tactics and Agda
  8. 2019/10/27 - Misc New blog structure & I'll delete some pages
  9. 2019/10/14 - Cubical Cold Introduction (3) -- Open Squares can be Capped
  10. 2019/10/01 - Cubical Cold Introduction (2) -- Inductive Types with Path Constructors
  11. 2019/08/20 - Cubical Cold Introduction (1) -- Squares and Diagonals
  12. 2019/08/01 - Cubical Cold Introduction (0) -- Paths and Intervals
  13. 2019/07/14 - PLT Structural typing and first-class case expressions
  14. 2019/06/20 - PLT Type inference under dependent type (meta variables)
  15. 2019/05/22 - Parser Interpreter without an AST
  16. 2019/04/21 - PLT Different styles of equality reasoning
  17. 2019/04/07 - PLT Fragmented Thoughts on Reducible Expressions
  18. 2018/12/06 - Agda Cubical Agda
  19. 2018/11/16 - PLT The World Over Dependent Types
  20. 2017/11/12 - Kotlin Tricks in using Kotlin `internal`