Canonicity proof for indexed inductive-recursive types

An implementation of Functional Reactive Programming

A teaser of Agda REPL 2025 Edition (WARNING: messy code)

Demo for high-performance type theory elaboration

Accompanying formalisation for the paper "Type theory in type theory using a strictified syntax"

Monadic effects and equational reasoning in Rocq

A proof assistant for higher-dimensional type theory

🩺 A library for compiler diagnostics

A Logical Relation for Martin-Löf Type Theory in Agda

A Logical Relation for Martin-Löf Type Theory in Agda

antifunext

Mechanizations of Type Theories

Distributions of Agda executable compiled into WebAssembly.

Containers can be made into a Cartesian Differential Category

Formalization of the polymorphic lambda calculus and its parametricity theorem

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…

Formalization of normalization by evaluation for the fine-grain call-by-value language extended with algebraic effect theories

LLNCS style files for LaTeX

Fix of the original Springer LNCS LaTeX class

Contextual Typing, formalized in Agda

[For generating patches for {Agda,ALS} WASM] Agda is a dependently typed programming language / interactive theorem prover.

A formalization of the theory behind the mugen library

Dynamic linking and runtime evaluation of Haskell, and C, including dependency chasing and package resolution.

Meta-programming utilities for Agda.

Datatype-generic programming meets elaborator reflection