Models of dependent type theory

An elisp package manager

An LSP client for Emacs implemented in Rust.

An editing environment for LaTeX mathematical documents

Transient interface for managing and interacting with projects

Demo for dependent types + runtime code generation

list and sexp navigation for tex modes

Formalizing the fact that countable choice implies postnikov effectiveness in HoTT

A Lean4 Formalization of Polynomial Functors

Write C shims from within Lean code.

Lecture notes and exercises for the advanced course on Categorical Realizability at the Midlands Graduate School (MGS) 2024 and the European Summer School on Logic, Language and Information (ESSLLI…

Python scripts that build optimal routes for node collection

Mirror of ocaml-forester

An experimental proof assistant based on a type theory for synthetic ∞-categories.

Latex documentation of our understanding of the synthetic /internal theory of the Zariski-Topos

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

Work in progress on semi-simplicial types

Cerberus C semantics

The math library of Lean 4

Yet another modal editing on Emacs / 猫态编辑

Experiment with synthetic domain theory in cubical agda

drom is a wrapper over opam/dune in an attempt to provide a cargo-like user experience. It can be used to create full OCaml projects with sphinx and odoc documentation. It has specific knowledge of…

A garden of small programming language implementations 🪴

A proof search and construction framework (based on refinery)

An embedding of ZFC into Agda

being an operating system for typechecking processes

agda blogging based on 1lab

Verified, Incremental, Binary Editing with Synthesis