it's dark because you're trying too hard 🐢
A list of books, a list of things I want to read, a list of things I've been up to. When I'm not computer sciencing, I spend my time making clothes and music. I like analog photography:
- A teeny tiny `rabiés` dictionary
- [WIP] FP madness
- EuroLLVM '26
- it's a long way to automata if you want to coinduct
- what is homotopy type theory?
- [WIP] writing and induction principle
- who subtypes subtyped definitions?
- 2025 takeaways
- ItaLean'25
- categories
- proving the correctness of a parallel prefix sum circuit
- writing a paper
- OOPSLA'25
- HASE'25
- population count
- recursive definitions in lean
- knaster-tarski theorem
- silent failures
- an inductive approach to spacer
- acl2
- lean-mlir misc
- 2024 takeaways
- theory of latency-insensitive design
- Big Spec '24
- PLDI'24
- the essence of bluespec
- modern automata theory
- hw design with/for ml
- cell morphing: from array programs to array-free horn clauses
- CGO'24
- learning semantic representations to verify hardware designs
- omega tactic in lean4
- high-level abstractions and modular debugging for FPGA design validation
- formal verification at higher levels of abstraction
- buechi, lindenbaum, tarski: a program analysis appetizer
- what are the semantics of hardware
- fsm anomaly detection using formal analysis
- abstract interpretation from buechi automata
- finite presentations of infinite structures: automata and interpretations