Nathan Guermond

arkdown-llm.

emacs-application-framework. EAF, an extensible framework that revolutionizes the graphical capabilities of Emacs

GoI-Visualiser. A tool for web browsers that simulates execution of the dynamic GoI abstract machine for the lambda-calculus.

czf-in-mahlo. A formalisation of Aczel's constructive set theory CZF in Agda with a Mahlo universe

centaur-tabs. Emacs plugin aiming to become an aesthetic, modern looking tabs plugin

ShiTT2. A dependently-typed language with indexed inductive types supported.

ligature.el. Display typographical ligatures in Emacs

abella-vscode. VSCode Extension for Abella

adelfa. An interactive proof assistant for reasoning about specifications written in the Edinburgh Logical Framework

polonius-proof. Verify naive = datafrog-opt, in rust/polonius

raven. Modern scientific computing for OCaml

scantailor-advanced. ScanTailor Advanced is the version that merges the features of the ScanTailor Featured and ScanTailor Enhanced versions, brings new ones and fixes.

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

agda-core. A work-in-progress core language for Agda, in Agda

ltunify. Tool for working with Logitech Unifying receivers and devices (mirror)

pl-conf. TypeScript

chalk. An implementation and definition of the Rust trait system using a PROLOG-like logic solver

OMicroB. An OCaml generic virtual machine for microcontrollers

FLT. Ongoing Lean formalisation of the proof of Fermat's Last Theorem

equational_theories. A project to map out the relations between different equational theories of Magmas.

unicorn. Purely functional GUI algebra

autosubst. Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]

slipshow. An engine for displaying slips, the next-gen version of slides

polytt. A type theory with native support for Polynomial Functors.

parapoly. A LaTeX-typeset reproduction of Reynolds' "Types, Abstraction and Parametric Polymorphism"

typst. A markup-based typesetting system that is powerful and easy to learn.

minttea. A fun little TUI framework for OCaml

call-cc-krivine. A Krivine machine for the call-by-name reduction of lambda calculus (+ call/cc) expressions in Haskell.

tex2png. Convert TeX and LaTeX to PNG images.

opam-bundle. A tool that creates stand-alone source bundles from opam packages

ppx_interact. Interactive breakpoints!

ocaml-forester. Mirror of ocaml-forester

open-games-engine. Haskell implementation of open games

opam-nix. Turn opam-based OCaml projects into Nix derivations

camyll. Static site generator

ocaml-multicont. multi-shot continuations in OCaml

HVM2. A massively parallel, optimal functional runtime in Rust

teyjus. An efficient implementation of the higher-order logic programming language Lambda Prolog

yocaml. YOCaml is a static site generator, mostly written in OCaml

hsubst. Hereditary substitution without eta-expansion.

nano-emacs. GNU Emacs / N Λ N O - Emacs made simple

chemacs2. Emacs version switcher, improved

bogue. GUI library for ocaml based on SDL2

ocaml-effects-tutorial. Concurrent Programming with Effect Handlers

DynamicalSystemsBook. TeX

lr-agda. Logical relations proof in Agda

SciLean. Scientific computing in Lean 4

extlint. An extensible linter for OCaml programs.

doi2bib. Smalls CLIs to get a bibtex entries from a DOI, an arXiv ID or a PubMed ID and to pretty print bibtex entries (or files)

SWIPL-OCaml. SWI-Prolog Bindings for OCaml: https://kiranandcode.github.io/SWIPL-OCaml/swipl/index.html

HOU. Higher Order Unification implemented in in Nipkow's described method

ocaml-hashcons. OCaml hash-consing library

links. Links: Linking Theory to Practice for the Web

fpm. Effing package management! Build packages for multiple platforms (deb, rpm, etc) with great ease and sanity.

ocaml-algebra. Small but neat OCaml library of (abstract) algebraic structures

ocaml-bindlib. Efficient binder representation in OCaml

ocaml-linenoise. Self-contained OCaml bindings to linenoise, easy high level readline functionality in OCaml

mainline. A continuation of the free version of ukuu.

bogue. GUI library for ocaml based on SDL2

react. Declarative events and signals for OCaml

lablqml. Interfacing Qt/QML with OCaml. Formely known as lablqt

Mezzano. An operating system written in Common Lisp

irmin. Irmin is a distributed database that follows the same design principles as Git

lablgtk. LablGTK 2 and 3: an interface to the GIMP Tool Kit

girards-paradox. A "implementation" of Girard's paradox in OCaml

owl. Owl - OCaml Scientific Computing @ https://ocaml.xyz

alcotest. A lightweight and colourful test framework

zed. Abstract engine for text edition in OCaml

notty. Declarative terminal graphics for OCaml

strawberry. :strawberry: Strawberry Music Player

ocolor. Print with style in your terminal using Format's semantic tags

HOL. Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.

lisp8x. Lisp for the TI-83+ line of graphing calculators

lablgl. LablGL: an openGL interface for OCaml

theoremprover-museum.github.io. HTML

zipperposition. An automatic theorem prover in OCaml for typed higher-order logic with equality and datatypes, based on superposition+rewriting; and Logtk, a supporting library for manipulating terms, formulas, clauses, etc.

opium. Sinatra like web toolkit for OCaml

elpi. Embeddable Lambda Prolog Interpreter

mirage. MirageOS is a library operating system that constructs unikernels

UniMath. This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.

aprolog. αProlog