An experimental language exploring computation and meaning through term unification, with logic-agnostic types.

Editor for .pxattr files (Collision Data used in Rockfish/Kero Blaster/KeroM(Pitest)

🧊 Чиста система з всесвітами

smarter git mergetool for clojure and edn

Abstract binding trees (abstract syntax trees plus binders), as a library in Agda

papers of Per Martin Löf

Pattern is an extensible combinator-based pattern match and substitution library. It's amazingly powerful.

GPU-accelerated compiler

OPAQUE protocol, a secure asymmetric password authenticated key exchange (aPAKE) that supports mutual authentication in a client-server setting without reliance on PKI and with security against pre…

A garden of small programming language implementations 🪴

"Evil will always triumph, because good is dumb." -- Spaceballs (1987)

Agda formalisation of second-order abstract syntax

A modern supercompiler for call-by-value functional languages

Research on integrating datalog & lambda calculus via monotonicity types

build-once run-anywhere c library

Next generation of ClojureCLR under development.

antifunext

Pattern matching for Clojure

Experimental implementation of Cubical Type Theory

An introduction to programming language theory in Agda

C in four functions

A CLI to add common aliases and features to deps.edn-based projects

Go tools, libraries and other code

A minimalist, general-purpose programming language based on meta-programming and parse tree rewrites

A collection of resources for learning type theory and type theory adjacent fields.

LaTTe : a Laboratory for Type Theory experiments (in clojure)

A modern proof language

A massively parallel, optimal functional runtime in Rust