Every Gist I've written.

Everything.md

The originality of these Gists varies drastically. Most are inspired by the work of others, in that case, all merit goes to the original authors. I have linked everything used as reference material on the Gists themselves.

Haskell

• Crégut's strongly reducing Krivine abstract machine
• Type-check STLC into a GADT
• Alex: indentation-sensitive lexer
• A-normalization (administrative normal form, ANF)
• Number of SK-combinator calculus terms of a given size
• Number of untyped lambda calculus terms of a given size
• Memoization using IORef
• Extremely simple Alex and Happy example
• Alex: strict and lazy bytestrings
• Alex: strict bytestring with user state
• Alex: strict text
• Another list monad
• Reverse State Monad
• Kappa calculus: the first-order fragment of typed lambda calculus
• Category theory in Haskell
• Lambda calculus to SKI combinators calculus compiler
• Simple CEK-style lambda calculus interpreter.
• Unpolished tactics for extrinsic (Curry-style) lambda calculus
• MonadUnliftIO
• CPS based lenses
• Functional references (also knows as lenses)
• fused-effects example
• Celular Automata (Rule 30)
• Seemingly impossible functional programs (Cantor spaces).
• CEK-style lambda calculus interpreter.
• Merge sort.
• Embedded Logic Programming Monad.
• Propositional Logic checker using the list monad for backtracking.
• CutList: Lists with Prolog-like Cut!
• A lean prover for minimal logic (related to Gentzen’s LJ sequent calculus)
• Simple unification.
• Simple unification-fd test.
• Exploring De Bruijn Indices.
• Higher Order Abstract Syntax parser and evaluator.
• Mini Parser Combinator.
• Catamorphisms, Anamorphisms, and Hylomorphisms.
• Minimal Type Theory with Universes and Pi Types.
• Doodle for better understanding Monads.
• Karen: an implementation of microKanren.
• Propositional Logic checker.
• Propositional Logic checker using "Continuations."
• The Calculus of Constructions.
• Mendler-Style Catamorphisms.
• Parse Simply Typed Lambda Calculus into a GADT.
• GADT implementation Simply Typed Lambda Calculus with Sum and Product types.
• Learning Haskell with Ninety-Nine Problems
• Haskell doodle made while reading about Twelf.
• Haskell doodle (F-Algebras, very short)
• Catamorphic Lambda Calculus Interpreter (doodle made while following a tutorial).
• Simply Typed Lambda Calculus with Type Checker (doodle made while reading a SO answer).
• Simply Typed Lambda Calculus with GADTs (doodle made while reading a SO answer).
• Simply Typed Lambda Calculus with GADTs and Singletons (doodle made while reading code that uses singletons).
• Unification of Trees (doodle made while reading a tutorial).
• Hindley-Milner Type Inference for Lambda Calculus (doodle made while reading a tutorial).
• Haskell doodle made while studying unification-fd's source code.
• Attempt to use unification-fd.
• Hindley-Milner type inference.
• Simple arithmetic expression parsec.
• Haskell doodle (dependently typed lambda calculus, very incomplete)
• Dependently Typed Red-Black Tree (incomplete, based on a great talk by Stephanie Weirich)
• Quick! Quicksort in Haskell!

Lean

• The admissibility of structural rules for the negative fragment of intuitionistic propositional logic
• Good recursors for mutually inductive types
• Normalization by Evaluation for Simply Typed Lambda Calculus
• Haskell style (i.e. using Type as a category) proof of the Yoneda lemma
• Two element set (with has_repr)
• A simple Galois connection.
• Stable propositions, i.e. (not necessarily decidable) propostions for which double negation elimination holds
• Discrete topology induced by a very simple metric space.
• Cofinite topology.
• Non-open infinite intersection of open sets.
• Unmeasurable set (incomplete).
• Simple proof of Cantor's theorem.
• Permutation group of a type.
• Soft Constraint Semirings.
• Images, preimages, subsets and their relation to injective and surjective functions.
• Lambda terms for natural deduction, sequent calculus and cut elimination
• Injective functions: right inverse and union of images
• Monomorphisms and epimorphisms in the category of sets.
• Untyped Lambda Calculus (various incomplete proofs)
• Let G be an infinite group and let H be a subgroup s.t. |H| < |G|. Then |G/H| = |G|.
• Provability Logic: □ and ⋄ modalities
• Various properties about convergent sequences
• Unit interval, ℝ/ℚ and ℝ/ℤ

Coq

• Lean quotients in Coq.
• Groups in Coq: uniqueness and cancellation.
• Injectivity, left inverses, and classical logic.
• Monomorphisms and Epimorphisms, Surjection and Injection.
• Injection, surjection, and inverses in Coq.
• The Axiom of Countable Choice
• Software Foundations: Functional Programming in Coq
• Software Foundations: Proof by Induction
• Software Foundations: Working with Structured Data
• Software Foundations: Polymorphism and Higher-Order Functions
• Software Foundations: More Basic Tactics
• Software Foundations: Logic in Coq
• Software Foundations: Inductively Defined Propositions
• Software Foundations: Total and Partial Maps
• Software Foundations: The Curry-Howard Correspondence
• Software Foundations: Induction Principles
• Software Foundations: Properties of Relations
• Software Foundations: Simple Imperative Programs
• Software Foundations: An Evaluation Function for Imp
• Software Foundations: More Automation

Agda

• Linear lambda calculus in Agda.
• Lambda calculus in Agda.
• Least fixpoint.
• Least and greatest fixpoints in Agda.
• Duality of propositional logic.
• Free variables in untyped lambda calculus.
• Normalization by Evaluation for Simply Typed Lambda Calculus
• Proof of function extensionality using interval type.
• The Agda Typeclassopedia: Functors
• The Agda Typeclassopedia: Applicative
• The Agda Typeclassopedia: Monad
• Proof that Peirce's Law is irrefutable in intuitionistic logic.
• A trivial proof that x + x is equal to 2 * x.
• Programming Language Foundations in Agda: Naturals
• Programming Language Foundations in Agda: Induction
• Programming Language Foundations in Agda: Relations
• Programming Language Foundations in Agda: Equality
• Programming Language Foundations in Agda: Isomorphism
• Programming Language Foundations in Agda: Connectives
• Programming Language Foundations in Agda: Negation
• Programming Language Foundations in Agda: Quantifiers
• Programming Language Foundations in Agda: Decidable
• Programming Language Foundations in Agda: Lists
• Programming Language Foundations in Agda: Lambda
• Programming Language Foundations in Agda: Properties
• Programming Language Foundations in Agda: De Bruijn
• Programming Language Foundations in Agda: More
• Programming Language Foundations in Agda: Bisimulation
• Programming Language Foundations in Agda: Inference
• Programming Language Foundations in Agda: Untyped
• Proof that addition (of Peano numbers) is associative in Agda.

C/C++

• Create an OpenGL context using Xlib and EGL
• Simple POSIX semaphore example.
• Peterson's algorithm in C.
• Strict alternation in C.
• Create a process in Windows.
• Multithreaded Fibonacci using POSIX threads.
• Inter-process communication using shared memory.
• fork and exec in C.
• Mirror a binary tree in C.
• Set implementation in C++ (using binary tree).
• Quick sort.
• Merge sort.
• Doubly linked lists (and stacks, and queues, and multiple sorting algorithms) in C++.
• Shell sort.
• Insert sort.
• Select sort.
• Queue in C++.
• Linked list.
• Brainfuck to C compiler.
• Noise!

Python

• Remove a specific tag from an HTML file.
• Simple Qiskit example.
• Various scheduling algorithms in Python.
• Server mediated inter-process communication.
• Extremely simple "distributed echo server" server in Python (Telnet clients should be able to connect to it)
• Inter-process communication using datagram sockets (i.e. UDP).
• Inter-process communication using stream sockets (i.e. TCP).
• fork and exec in Python.
• Type-checking decorator and bogosort.
• Simple WebSockets chat in Python.
• Simple encrypted UDP chat in Python.
• Furigana!

Configuration Files

• Minimal Neovim config.
• Minimal Bash config with infinite command history and better autocomplete settings.
• Minimal Emacs configuration.
• Gnome terminal config with fallback fonts
• Minimal VSCode config.
• radare2 config and cheatsheet.
• dwm config
• st config
• dmenu config
• Custom XDG user directories.
• Minimal xinitrc for dwm
• An extremely minimal vim color scheme.
• Glorious GHCi Configuration File!

Prolog

• Randomly generate typable SK-combinator calculus terms using Boltzmann samplers
• Generate typable SK-combinator calculus terms of a given size
• Randomly generate simply-typed lambda calculus expressions using Boltzmann samplers
• Generate simply-typed lambda calculus expressions of a given size
• Ninety-Nine Prolog Problems

JavaScript

• Simple Javascript timer
• Snake game in pure Javascript.

Java

• Example using semaphores in Java.
• Producer-Consumer example in Java.
• Starting a process with Java.

Twelf

• Twelf proof that addition commutes.

Racket

• Ninety-Nine Racket Problems

Scripts

• Merge completely different Git repositories
• Reference script for installing a GCC i386-elf toolchain.
• Helper scripts for VMs on a virtual network.

Assembly

• Fizz Buzz in assembly.
• Hello, world! (GNU Assembler & NASM)

SQL

• Oracle cursor example
• Triggers and sequences in Oracle Database.
• Simple Oracle Database schema.