Prime numbers for Coq

Implementation of CARVe in Rocq

my phd manuscript

Type theories as quotient inductive-inductive-recursive types

🧊 An indexed construction of semi-simplicial and semi-cubical sets

Collection of Automated Reasoners

A tool-agnostic formal specification language for OCaml.

This repository contains the mechanisation of testing theory à la De Nicola and Hennessy.

Small Docker images containing Agda

Run 1ML in your browser

Par (⅋) is an experimental concurrent programming language. It's an attempt to bring the expressive power of linear logic into practice.

Demo for dependent types + runtime code generation

Command-like expressions for real infinite-precision calculations

A specialized audio CD-ripper optimized for track recovery.

LanguageTool Integration for Typst for spell and grammer check

A verification toolchain for Rust programs

Sized types and coinduction in Safe Agda

A faust-to-fpga compiler toolchain

an educational compiler intermediate representation

Mechanizations of Type Theories

Calculating Graph-Based Compilers

A lightweight and full-featured cross-platform desktop client for self-hosted music servers

A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory

Freyd category semantics for SSA in Lean 4