joom/hezarfen

a theorem prover for intuitionistic propositional logic in Idris, with metaprogramming features

foreverbell/verified

Coq formalizations and proofs of (data) structures and algorithms.

anton-trunov/coq-lecture-notes

Coq Lecture Notes (WIP)

jespercockx/agda-lecture-notes

Agda lecture notes for the Functional Programming course at TU Delft

barry-jay-personal/tree-calculus

Proofs in Coq for the book Reflective Programs in Tree Calculus

JBakouny/Scallina

A Coq-based synthesis of Scala programs which are correct-by-construction

ghostdogpr/purelogic

Direct-style pure domain logic for Scala

blanchette/interactive_theorem_proving_2024

Files associated with the course Interactive Theorem Proving at LMU SoSe 2024