LaTTe : un laboratoire d'expériences pour la théorie des types

Équipe : APR

LaTTe est un assistant de preuve basé sur la théorie des types. La caractéristiques principale de LaTTe est d'être conçu comme une bibliothèque (contrairement à la plupart des assistants conçus comme des outils indépendants) complètement intégrée dans le langage et l'écosystème Clojure. Cela permet la diffusion et l'échange de contenus mathématiques élaborés de façon collaborative sur Internet. L'assistant fournit également un langage à domaine spécifique pour les preuves déclaratives, basé sur le style "fitch" de preuves pour la déduction naturelle. L'outil est développé au sein de l'équipe APR en collaboration avec l'équipe Whisper (Pierre-Evariste Dagand).

Responsable : Frédéric PESCHANSKI
https://github.com/fredokun/LaTTe