Awesome

Repository of logic definitions for Lambdapi

• TFF: polymorphic first-order logic (with a few definitions and theorems on natural numbers and polymorphic lists)

• U: theory introduced in Axioms for Mathematics

• Zenon: logic files used by the automated theorem prover ZenonModulo

• PTS: Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo