Bibliothèques écrites en Agda

La bibliothèque standard Agda.

Une bibliothèque expérimentale pour Cubical Agda.

Manifestations logiques de concepts topologiques, et d'autres choses. Cette version adopte le point de vue univalent.

Compilation du code Agda en Haskell lisible.

Formalisation Agda de l'Introduction to Homotopy Type Theory (par HoTT-Intro).

Total Parser Combinators dans Agda.

Formalisation des langages réguliers en Agda: expressions régulières, automates à états finis, preuve d'équivalence, preuve du lemme de pompage..

Rédaction d'un devoir universitaire dans lequel je parle de classes de types et de types dépendants.

Un modèle Agda, configuré pour Gitpod (www.gitpod.io) pour vous offrir des environnements de développement éphémères pré-construits dans le cloud.

Encodage Agda des catégories prémonoïdales.

Le jeu de la vie de Conway à Agda..