An implementation of circular buffer on flash memory for ESP32

Clean, minimal, accessible reproduction of DeepSeek R1-Zero

Formalized: Intuitionistic Propositional Calculus (IPC) plus Atomic Law of the Excluded Middle (ALEM) is Classical Propositional Calculus (CPC)

An axiom-free formalization of category theory in Coq for personal study and practical work

Differentiable Cosmological Forward Model

An implementation of lambda weak omega in Coq, with report.

Single file Lambda Calculus implementations demonstrating various type system features and interpretation techniques

A collection of tools for writing technical documents that mix Coq code and prose.

Coq course at Chalmers CSE

Completeness and Decidability of Modal Logic Calculi [maintainer=@chdoc]

Formalization of Category Theory in Coq.

A toolkit for enforcing logical specifications on neural networks

EPIT 2020 - Spring School on Homotopy Type Theory

The 2021/22 edition of Strathclyde's Functional Programming course in Haskell

A dictionary for Tolkien's languages

💻📖 Laws, Theories, Principles and Patterns that developers will find useful. #hackerlaws

OpenStreetMap's Blinking Beacons

A command-line tool and Rust library with Python bindings for generating regular expressions from user-provided test cases

Text generation language

Formalization of type theory

"A Basis for Event-Driven Programming" based on Linear Temporal Type Theory

A quick reference for mapping Coq tactics to Lean tactics

SwiftLaTeX, a WYSIWYG Browser-based LaTeX Editor

A simple Bash alarm clock script.

A project management service with pure functional programming paradigm in the heart.