In Agda geschriebene Bibliotheken

Die Agda-Standardbibliothek.

Eine experimentelle Bibliothek für Cubical Agda.

Logische Manifestationen topologischer Konzepte und andere Dinge. Diese Version übernimmt den univalenten Standpunkt.

Kompilieren von Agda-Code zu lesbarem Haskell.

Agda-Formalisierung der Einführung in die Homotopietypentheorie (von HoTT-Intro).

Gesamtparser-Kombinatoren in Agda.

Formalisierung regulärer Sprachen in Agda: reguläre Ausdrücke, endliche Automaten, Beweis der Äquivalenz, Beweis des Pumping-Lemmas.

Schreiben von College-Aufgaben, in denen ich über Typklassen und abhängige Typen rede.

Eine Agda-Vorlage, konfiguriert für Gitpod (www.gitpod.io), um Ihnen vorgefertigte, kurzlebige Entwicklungsumgebungen in der Cloud bereitzustellen.

Agda-Kodierung prämonoidaler Kategorien.

Conways Spiel des Lebens in Agda..