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
ssa
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/fbip-demos
Demos to test out Lean's functional but in place.
bollu/LeanAllocatorAdversary
An adverserial allocation pattern against the Lean4 memory allocator
bollu/lent-2024-logic-and-proof
Lean notes for "Logic & Proof" : Cambridge Tripos Part 1B, Lent 2024
bollu/ReProver
Retrieval-Augmented Theorem Provers for Lean
bollu/2024-lean4-borrowing
Fork of the Lean4 compiler for borrowing changes.
bollu/ariadne.lean
A port of the ariadne rust error printing library to lean: https://docs.rs/ariadne/latest/ariadne/
bollu/debruijn-ssa
bollu/deep-prosody
Reading Homer while being a linguistic midwit, and so using LLMs to figure out syllables, pentameter, and prosody.
bollu/FStar
A Proof-oriented Programming Language
bollu/generalized-rewriting.lean
bollu/heartbeat-trajectoid
bollu/lamr
Logic and Mechanized Reasoning
bollu/lean4
Lean 4 programming language and theorem prover
bollu/leanid
A ghcid style half-of-an-IDE for 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/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/PolCert
A verified polyhedral scheduling validator in Coq.
bollu/quenya.lean
A Lean4 library to build and manipulate ELF files.
bollu/ShapeUp-public
A 3D Modeler Made in a Week
bollu/std4
Standard Library for Lean 4
bollu/taichi
Productive & portable high-performance programming in Python.
bollu/tracy
Frame profiler