Computing

Some articles on LLVM and Coq.

compilers (2015 — 2024)

• A tour of the LLVM backend
• An introduction to auto-vectorization with LLVM
• Deficiencies in LLVM's LoopVectorize
• Incrementally updating the Dominator
• Detecting loops
• Inside a register allocator
• An ABI-mismatch bug

coq (2020)

• Predicativity in Coq
• Equality in Mechanized Mathematics
• Lean versus Coq: The cultural chasm