Transparent file encryption in git

A purely functional programming language with first class types

Formal proof of the Four Color Theorem [maintainer=@ybertot]

A formalization of System Fω in Agda

Formalizations of Gradually Typed Languages in Agda

Algebraic, staged parsing for OCaml: typed, compositional, and faster than yacc

Agda is a dependently typed programming language / interactive theorem prover.

justfont collaborates with calligrapher Daphne to release Elffont (精靈文), a unique typeface blending Bopomofo phonetic symbols with a mystical "Elvish" style.

Extensions to the cubical stdlib category theory for categorical logic/type theory

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

Reading group for Cisinski's higher categories and homotopical algebra

Examples of technical drawing with John Hobby's MetaPost language

A Rust/WASM implementation of homotopy.io

A graduate course on formalized mathematics at the Faculty of Mathematics and Physics, University of Ljubljana, Fall semester 2024/25

A formalized construction of coslice colimits

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

Open Source Continuous File Synchronization

Formalizing the fact that countable choice implies postnikov effectiveness in HoTT

Public-facing information about WITS

formalization of an equivariant cartesian cubical set model of type theory

antifunext

This is the project repository for Darwin, a typeface for books and articles, with a focus on scientific writing.

A proof assistant for higher-dimensional type theory

My forest of notes!

forked from git.sr.ht/~jonsterling/forester-base-theme

A complete proof in Agda of the Church-Rosser theorem for untyped λ-calculus formalizing the methods by Komori-Matsuda-Yamakawa (2014) and the proof by Nagele-van Oostrom-Sternagel (2016); reuses t…