lambda-prolog

Embeddable Lambda Prolog Interpreter

Rocq plugin embedding Elpi

My portfolio contains a lexer generator, a parser generator, my own λProlog interpreter, and several meta-theorems for the propositional logic with their proofs written in Coq.

Project Putting All Power!

λProlog inside Lean 4: write tactics, commands and proof search as logic programs, share types with Lean both ways, get kernel-checked proofs

99 λProlog Problems (eventually)

Interactive theorem proving in ELPI

An Ugly, untested and mostly unsatifying translator from λProlog code to Latex inference rules