Discover bollu/lent-2024-logic-and-proof Open Source project

A tiny *optimising* compiler for an imperative programming language written in haskell

179

tiny-optimising-compiler

a better bookmark system for SublimeText

154

sublimeBookmark

A CLI in haskell to quickly move through the filesystem

129

teleport

HTML

108

simplexhc

compiler with polyhedral optmization for a lazy functional programming language

A visual interpreter of the template instantiation machine to understand evaluation of lazy functional languages

timi

Rust

blaze

Haskell re-implementation of STOKE, the stochastic superoptimizer

Jupyter Notebook

notes

Latex notes on papers, courses, ideas: Pure math and computer science.

Sublime text plugin for live value watching for interpreted languages

SublimeRealityCheck

An elegant implementation of discrete diffgeo in haskell

discrete-differential-geometry

optimising compiler for Haskell's intermediate representation (STG) to LLVM IR

simplexhc-cpp

bollu learns implementation of dependent typing

minitt

Jupyter notebook for the Lean4 programming language

lean-to

WARD is a minimal, performant infinite whiteboard app for wacom tablets

ward

coremlir

Encoding of GHC Core inside MLIR

Pure haskell encoding of MLIR for printing, parsing, and mutating MLIR within haskell

mlir-hs

A minimal in MLIR dialect along the lines of STG to represent laziness.

LLVM

koans

Short pieces of code that are "plays" - mostly haskell, sometimes math / other things

Snippets that explore how linkers work, one flag at a time.

linker-koans

Makefile

rete

An implementation of the rete algorithm from 'Production Matching for Large Learning Systems'

PolyMage is a domain-specific language and optimizing code generator for auto-parallelisation

polymage

A catalog of broken Haskell programs to improve error messages

hask-error-messages-catalog

diffgeo

A formalization of synthetic differential geometry in Coq using infinitesimal analysis

Coq

quantum-course-exercises

Solutions to coursework in Q#

soundsynth

Bollu learns physically based sound sythesis

algorithms implemented in C++, written in the arthur whitney style

Reimplementation of llama.cpp in Lean4

llama.lean

IIIT-H-Code

code written for assignments and whatnot at IIIT-H

myriad

A library for manifold algorithms, as I learn discrete diferential geometry and general relativity

Dependence Analysis for Haskell code using the polyhedral framework

dependence-analysis-hask

elide

Elide: Elegant Metamodal Lean4 IDE.

A semantics for the types of loops that can be modelled by polyhedral compilation techniques, developed in Coq.

polyir

Coq

TaleOfTwoDialects

nontrivial lowering examples for MLIR that are ignored by the MLIR tutorials

My solutions to the software foundations book

software-foundations-solutions

HTML

qoc

Quite Obfuscated Constructions

game to experiment with Rust, Carmack's ideas

equinox

Rust

lean4-entemology

Where we collect lean4 bugs

There are many OSes, this one is mine

minos

Makefile

mlir-hoopl-rete

rewrites for MLIR with hoopl / rete

MLIR

smol

smol IDE for a smol language that permits insane static analysis because smol

shakuni

An exploration of minimality and parallelism in probabilstic programming languages.

Jupyter Notebook

pico-mlir

A mini language written using MLIR + MAKEFILES! so you get to see all the commands, no CMake magic.

PolyBench/C from http://web.cse.ohio-state.edu/~pouchet/software/polybench/

polybench-c

pisigma

A reference copy of PiSigma: dependent types with without the sugar

Egraphs & ematching in Lean

lean.egraphs

library / CLI as a swiss-army knife for low level bit fiddling debugging.

biter

Demos to test out Lean's functional but in place.

fbip-demos

A copy of the hugs haskell98 implementation; hoping to eliminate bitrot

hugs

bindings to SDL2 (Simple DirectMedia library) in Lean

sdl2.lean

dotfiles

my dotfiles for easy access

Vim Script

master-thesis

My master's thesis on NLP and representation learning

LLVM's loop analysis theory (Scalar Evolution) formalized in Coq

SCEV-coq

Makefile

warren

The warren abstract machine for Pascal, in Hakell

Slides for my talk at functional conf 2019 on probabilistic programming

functionalconf-2019-slides-probabilistic-programming

A personal fork of the Polly-LLVM project

polly

ppcg

A fork of the original PPCG with debug code: http://repo.or.cz/w/ppcg.git

mips-bsv

an implementation of a MIPS processor in BlueSpec System Verilog

Bluespec

haskell-tutorial

Files for a haskell tutorial I'm teaching at IIIIT-Hyderabad

Try to JIT Free monads in Haskell.

freejit

Slides for haskell exchange 2020 talk on smallpt

slides-haskell-exchange-2020-smallpt

A fork of the LLVM project for personal use

llvm

LLVM

dataflow

A view of dataflow architectures, with a modern haskell perspective

Deltas: An algebraic theory of diffs in haskell

paper-deltas

Lisp interpreter in Haskell

hask-lisp-interp

A repo for work between Alok Debnath and Siddharth Bhat

alok-bollu

sicm

structure and interpretation of classical mechanics

Scheme

CASette

Mixtape of computer algebra system (CAS) algorithms

Documenting the PhD slog, one day at a time

captainslog

amalgam

amalgam ~ composite | A small library for interactive symbolic number theory explorations in haskell

Game on using text generation to trigger empathy

gde-game

polymorphic type inference with unification from the Dragon book

unification

An implementation of warren, the abstract machine for Prolog. Is a transcription of the lecture notes "warren's abstract machine a tutorial reconstruction"

warren-cpp

procedurally generated 2d shooter

proGenY

Tiny haskell library to prettyprint sparklines onto the CLI!

clisparkline

tabled typeclass resolution implementation

polybench-hs

Polybench HS

tabledtypeclass

implementation of the paper "functional fluids on surfaces"

functional-fluids-on-surfaces

Equality saturation for fun and profit

sunnyside

Rust

optics

optics and refraction simulation in C++

gutenberger

fast vectorized presburger automata

Haskell bindings to Stockfighter using Servant

hs-stockfighter

The one where bollu decompiles attention models

decompile-transformer

Jupyter Notebook

musquared

Demand-agnostic managed language compiler using MLIR

Smallpt rewrite that's fast!

smallpths

Minimal fortran-ish language with LLVM backend, written for a compilers course

tinyfort

Me messing around with language models, trying to make NLP run on commodity hardware with weird ideas.

languagemodels

haikus

detect haikus

A dumping ground for short Lean programs that demonstrate a point: a kōan

lean-koans

Implementation of geometric algebra primitives

geometric-algebra

A formalisation of propogators as ekmett speaks about them on the livestream: https://www.twitch.tv/ekmett

propogators-coq

Coq

pegasos-svm

An implmentation of the pegasos SVM learning algorithm

Competitive coding solutions

ppsspp-help

Help for ppsspp

CSS

competitive

quchen's prettyprinter library, stolen and stripped of other code for GHC.

prettyprinter-core

For of terrorjack/GHC to hack on austerius

ghc-asterius

A lisp interpreter in C++ for fun :)

lispInterpreter

Code written using BlueSpec Verilog, general FPGA messing around for my course

FPGA-playground

Bluespec

100

absint

abstract interpreters for a tiny SSA language in haskell