G. Allais

agdarsec. Total Parser Combinators in Agda

idris-tparsec. TParsec - Total Parser Combinators in Idris

generic-syntax. A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs

potpourri. Where my everyday research happens

agda-sizedIO. IO using sized types and copatterns

aGdaREP. Implementing grep in Agda

agda-presburger. Deciding Presburger arithmetic in agda

agda-nbe. Formalizing nbe in agda

typing-with-leftovers. Self-contained repository for the eponymous paper

pearl-binary-search. Functional Pearl: Certified Binary Search in a Read-Only Array

type-scope-semantics. A self-contained repository for the paper Type and Scope Preserving Semantics

thesis. Syntaxes with Binding, Their Programs, and Proofs

agdarky. Agda suffices: software written from A to Z in Agda

idris-tmustache. Total Logic-Less Templating Library

agdARGS. Dealing with Flags and Options

great-library-of-idris. A crowd-sourced list of papers using Idris

dot-analysis. Analysing dependency graphs produced by Agda

CS410-2024. Content of the CS410 lectures

proof-search-ILLWiL. A self-contained repo for the ILLWiL paper

idris-free. Various Free-X experiments

agda-tiling. Tiling DSL for Agda

MiniAgda-mode. An emacs mode for MiniAgda

STRINaGda. Dependent Stringly-Typed Programming

metamorphismsinagda. Haskell

gallais.github.io. My website, now generated using Hakyll

agda-pretty-notgreedy. Port of Bernardy's Functional Pearl: A Pretty But Not Greedy Printer

syntax-with-binding. A Generic Treatment of Syntaxes with Binding in Haskell

ocaml-sparse-matrix. Implementation of Sparse Matrices in Ocaml using Batteries

ncurses-idris. A hobby implementation of an ncurses binding for Idris 2

coolcat. not a wiki

sta-latex. Unofficial set of LaTeX classes, styles, and knick-knacks aimed at use within the University of St Andrews.

idris-dhcli. Declarative Hierarchical Command Line Interfaces

sleepp. A sleep with a progress bar

nary. Self-contained repository for the corresponding TyDe'19 paper

dailyprogrammer. Solutions to problems found on /r/dailyprogrammer

word-arithmetic. Arithmetic on unsigned integers, in Haskell

countdown. Haskell

conkysh. An excuse to have a bit of fun with the Haskell X11 bindings