Leibniz equivalence and Liskov substitutability library for Scala.
A Proof Checker for Constructive Logic
Agda formalization of Martin-Löf intensional type theory, following the Type Theory course by M.E. Maietti and I. Blechschmidt at Università di Padova
Yet anOther Logic Kernel
An interactive browser-based type language and type-checker grounded in the Curry-Howard correspondence (propositions as types), covering intuitionistic propositional logic with natural deduction rules of inference. Users can write lambda calculus terms, check their types, and explore the derivation tree side-by-side with the ... · Built with Manus
PoC compiler for the Incredible Proof Machine (http://incredible.pm)
Add a description, image, and links to the propositions-as-types topic page so that developers can more easily learn about it.
To associate your repository with the propositions-as-types topic, visit your repo's landing page and select "manage topics."