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

FAQ about Madrid for digital nomads

antifunext

formalization of an equivariant cartesian cubical set model of type theory

Alexander Grothendieck's 1972 talk at CERN, on scientific research

Implementation of Span(Graph) via the State(-) construction

An implementation of a simple Neural network in Idris using category theory.

RASP-L in Haskell for my fellow rascals

A proof assistant for higher-dimensional type theory

List of Treewidth solvers, instances, and tools

Tools for exploring logic through Lorenzen dialogue games.

A prototype programming language with polymorphic reachability types that track freshness, sharing and separation.

Master Thesis code: Implementing Game Comonads in Finite Model Theory using Dependent Types in Idris

Implementation of Lstar algorithm in Haskell

Bshouty's CDNF algorithm

Efficient SAT-based theorem prover for Intuituionistic Propositional Logic

Implementation of the paper "Modular Sumcheck Proofs with Applications to Machine Learning and Image Processing"

Formal power series in mathomp

Resumption and Reactive-Resumption Monads for the Haskell programming language.

Implementing integer matrix inversion with SAT solver

Simple CDCL algorithm implementation in Kotlin

Technical interpretation of Girard's transcendental syntax

Facilities for generating dependently-typed data

x86 C compiler written in untyped lambda calculus

A type theory with native support for Polynomial Functors.

Experiments with nominal types in HoTT Agda