Patrick Bahr

compdata. Haskell library implementing "Data Types a la Carte"

calc-comp. Coq proofs for the paper "Calculating Correct Compilers"

AsyncRattus. Haskell

Rattus. A modal FRP language embedded in Haskell.

McCarthy-Painter. Coq proof for the paper "Compiling a Fifty Year Journey"

equivalence. Haskell

reg-machine. Coq & Haskell code for Calculating Correct Compilers II

compdata-param. Haskell library implementing parametric compositional data types.

guarded-lean. Guarded recursive types in Lean

alacarte-idris. Data Types a la Carte in Idris

monadic-compiler-calculation. Agda

alfred. Haskell library for writing workflows for Alfred 2.

compdata-dags. Compositional Data Types on DAGs

compdata-automata. Tree automata on Compositional Data Types

cps-defun. Coq proofs for the paper "Cutting out Continuations"

calculating-compilers-for-concurrency. Agda formalisation for "Calculating compilers for concurrency"

idris-raytracer. simple ray tracer implemented in Idris

calc-graph-comp. Calculating Graph-Based Compilers

partial-comp-calc. Partial Compiler Calculation

projection. Projection function for arbitrarily nested binary product types.

graph-comp. Coq proofs for the paper "Proving Correctness of Compilers Using Structured Graphs"

calc-comp-rel. Coq proofs for the paper "Calculating Certified Compilers for Non-Deterministic Languages"

abc-puzzle. Generate instances of the ABC Logic Puzzle.