A demo implementation of a simple dependently-typed language

Trap AI web scrapers in an endless poison pit.

papers of Per Martin Löf

Functional programming with fewer indirections

alsa-scarlett-gui is a Gtk4 GUI for the ALSA controls presented by the Linux kernel Focusrite USB Drivers

Latest driver development code for sound/usb on Linux

The Helium compiler, Helium-as-a-library, and the texthint interpreter

An open source desk widget using affordable TFT displays and an ESP32 (:

A free, browser-based simulator of spintronic circuits.

A property based testing framework for Kotlin

A DSL for cellular automata running on the GPU using Margolus neighborhoods

An i-conic repository.

Haskell interface to automated theorem provers

A hip inductive theorem prover!

Elea (as developed for my PhD)

Equational laws for free

Supercompiler for theorem provers

Tools for musicians to practice more efficiently

SC Mini is a "minimal" positive supercompiler

Supercompilation by Evaluation: archived for posterity. See http://github.com/batterseapower/chsc for the latest developments.

Public repository for Advanced Programming

Hazel, a live functional programming environment with typed holes

Very controlled natural language tactics for Lean

Educational Proof Assistant for Type Theory

A friendly functional language for finding counterexamples 🎯

Agda to C compiler

Mirror of the Glasgow Haskell Compiler. Please submit issues and patches to GHC's Gitlab instance (https://gitlab.haskell.org/ghc/ghc). First time contributors are encouraged to get started with th…

Raylib bindings for Lean4