Isaac Elliott

qtt. Quantitative Type Theory implementation

sized-hkts. Higher kinded polymorphism in a language with unboxed, statically sized datatypes.

sage. Efficient parser combinators for Haskell

cbpv. A usable type system for call by push-value

idris-but-its-c. Idris, but it's C

parametricity-proofs. Proofs of the number of inhabitants of polymorphic functions

lambdapi. Educational implementation of dependent types

meta-lambda. Lambda Calculus with quote and unquote

ipso. A functional scripting language.

closure. Closure calculus implementation

ccc. Using lambda calculus as the syntax for cartesian closed categories, ala Conal Elliott.

indexed-paths. A library for working with free categories

stg-llvm. Attempting to compile STG to LLVM

mini-adapton. miniAdapton in Haskell

nix-docs. Reference documentation for (a teensy part of) Nix

typed-cfg. Well-typed compile time parser generator

rows. A language with polymorphic records and variants, using HMF inference.

eden. Experimenting with GHC's Backpack technology to create modular programming language representations

agda-safe-sized-types. Sized types and coinduction in Safe Agda

spacemacs-neuron. A spacemacs layer for neuron

edit-log. Structured editing of a programming language via a log

lang. learning how 2 compile, like seriously

bide. An attempt at understanding Conor McBride's bidirectional typing discipline

phil. A pure functional language that compiles to PHP

idris-tictactoe. TicTacToe using dependent types

reactive-data. A framework for building fine-grained reactive datatypes

como. Contextual Modal Type Theory, formalization and implementation

idris-lambda-reflection. Reflecting simply-typed lambda calculus into Idris

tell. The MonadTell type class, and related monad transformers and utilities.

classy-lc. Modular lambda calculus using Backpack and prisms

phil2-editor. Attempt at a terminal-based structural editor using Reflex and Brick

pl0-haskell. PL/0 compiler written in Haskell

imp. This is not the droid you're looking for

stencil. Shareable programmable project templates

biscope. scopes over bifunctors

humblr. Proof-of-concept Haskell blog platform

linearlambda. Linear lambda calculus implementation

learn-vulkan. Learning to use Vulkan and building a high-level interface to `vulkan-api` along the way

pattern-unification. Learning pattern unification

definable-syntax. A programming language with very few reserved keywords

hover-pill. A game I made to learn Bevy, a Rust game engine.

top-down-hindley-milner. Haskell

monoidal-lens. Optics built using monoidal categories

certified-lc. use coq to verify stlc in a way that extracts to good haskell

unification. An alternative to `unification-fd`, using the `equivalence` library

java-hindley-milner. Implementation of Hindley-Milner type inference in Java

rust-wasm-gol. Learning Rust + WebAssembly

leeft-idr. Attempting to build type preserving lambda lifting

haskell-typecheck-combinators. A type checker monad and combinators

reflex-parser. What would functional-reactive parser combinators look like?

ranged. Integers with type-level ranges

ray-tracing-in-one-weekend. Ray tracing in one weekend, in Rust

psbt. Build tool for PureScript written in Haskell

spiddy. What happens when I try to build a performant compiler?

humblr-frontend. Single page app frontend for humblr written using Purescript

template-monoid. A datatype for combining monoidal values with effects.