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