Automatic code generation for Scala functions and expressions via the Curry-Howard isomorphism

Type inference algorithms and intuitionistic propositional theorem provers solving type inhabitation problems

Proof search for intuitionistic propositional logic using Dyckhoff's LJT.

Analytic tableau based minimal model generator, model checker and theorem prover for first-order logic with modal extensions

Open source F# mathematical logic library.

A theorem prover for intuitionistic propositional logic

Kripke semantics

A twitter bot that decides whether a formula is an intuitionistic validity and tweets the result.

Public companion repo for the Goodman-Veselov SKY kernel manuscript: Lean-to-SKY kernel slice, verification artifacts, and benchmark evidence.

Graphical Tableaux Prover for Propositional-, First Order Predicate-, Intuitionistic Propositional- and Intuitionistic First Order Predicate Logic

papers of Per Martin Löf

Intuitionistic and classical propositional logic library

Some pretty old experiments in intuitionistic logic using Agda

Trying to build logic & proof system library on TypeScript.

A natural deduction prover in Gentzen's system.

Material sobre de lógica constructiva para bosquejar un curso introductorio de pregrado

Selected logical aspects of apophatic theology | The PhD thesis in philosophy written in 2022 (in Polish) under the supervision of Adam Olszewski.

Codebase for my MS thesis formalizing the commutative ring axioms of the integers in Agda

Machine-checked formalization of Gheorghiu's 'Support is Search' theorem (arXiv:2603.13018v1) in Lean 4 — 74 theorems proving the relationship between base-extension support semantics and proof search for IPL, plus a compiled refutation of the standalone implication-forward schema on atomic-base kernels.

Attempting to make the concept of executable thoughts an actuality