La bibliothèque Lambdapi est une implémentation en logique intuitionniste du premier ordre de types de données tels que les ensembles, la logique propositionnelle, l'égalité de Leibniz, la logique du premier ordre, les booléens et les nombres naturels, ainsi que des listes polymorphiques.