A Coq mechanization of the Karp-Miller algorithm based on Kruskal-AlmostFull

Quasi morphisms for Almost Full relations

Coq library for rose trees

The Fan theorem for inductive bars and a constructive variant of König's lemma

Kruskal and Higman type tree theorems for the Kruskal-AlmostFull library

Library of basic results about Almost Full relations in Coq

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