Pinned Repositories
blaze
Haskell re-implementation of STOKE, the stochastic superoptimizer
bollu.github.io
code + contents of my website, and programming life
cellularAutomata
a collection of cellular automata written in Haskell with Diagrams
mathemagic
Toybox of explanations of mathematics. Initial focus on (discrete) differential geometry
notes
Latex notes on papers, courses, ideas: Pure math and computer science.
SCEV-coq
LLVM's loop analysis theory (Scalar Evolution) formalized in Coq
sublimeBookmark
a better bookmark system for SublimeText
timi
A visual interpreter of the template instantiation machine to understand evaluation of lazy functional languages
tiny-optimising-compiler
A tiny *optimising* compiler for an imperative programming language written in haskell
lean-mlir
A minimal development of SSA theory
bollu's Repositories
bollu/bollu.github.io
code + contents of my website, and programming life
bollu/elide
Elide: Elegant Metamodal Lean4 IDE.
bollu/lean4-entemology
Where we collect lean4 bugs
bollu/smol
smol IDE for a smol language that permits insane static analysis because smol
bollu/dotfiles
my dotfiles for easy access
bollu/lent-2024-logic-and-proof
Lean notes for "Logic & Proof" : Cambridge Tripos Part 1B, Lent 2024
bollu/optics
optics and refraction simulation in C++
bollu/xdsl
A Python Compiler Design Toolkit
bollu/2024-lean4-borrowing
Fork of the Lean4 compiler for borrowing changes.
bollu/debruijn-ssa
bollu/Decker
A multimedia sketchpad
bollu/ELFSage
A toy ELF parser/validator
bollu/lamr
Logic and Mechanized Reasoning
bollu/lean-sys
Rust bindings for the Lean 4 proof assistant
bollu/lean4
Lean 4 programming language and theorem prover
bollu/leanid
A ghcid style half-of-an-IDE for lean
bollu/LNSym
Armv8 Native Code Symbolic Simulator in Lean
bollu/madoko
Madoko is a fast markdown processor for high quality academic and technical articles
bollu/matchgoal.lean
Match goal tactic for lean
bollu/MicroHs
Haskell implemented with combinators
bollu/nixpkgs
Nix Packages collection & NixOS
bollu/paper-pearl-zippy-ssa-rewriting
A proof pearl on using zippers to encode SSA rewriting
bollu/paper-proof-pearl-zippy-rewriting
The one with the zipper for region rewriting
bollu/pointerchase.lean
The one where bollu bends well founded induction for convenient pointer chasing APIs
bollu/PolCert
A verified polyhedral scheduling validator in Coq.
bollu/quenya.lean
A Lean4 library to build and manipulate ELF files.
bollu/raylean
Lean4 bindings for raylib
bollu/ShapeUp-public
A 3D Modeler Made in a Week
bollu/std4
Standard Library for Lean 4
bollu/tracy
Frame profiler