Pinned Repositories
agda-stdlib
The Agda standard library
agda-presburger
Deciding Presburger arithmetic in agda
agda-sizedIO
IO using sized types and copatterns
aGdaREP
Implementing grep in Agda
agdarsec
Total Parser Combinators in Agda
generic-syntax
A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs
idris-tparsec
TParsec - Total Parser Combinators in Idris
potpourri
Where my everyday research happens
typing-with-leftovers
Self-contained repository for the eponymous paper
Idris2
A purely functional programming language with first class types
gallais's Repositories
gallais/agdarsec
Total Parser Combinators in Agda
gallais/idris-tparsec
TParsec - Total Parser Combinators in Idris
gallais/generic-syntax
A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs
gallais/potpourri
Where my everyday research happens
gallais/agda-presburger
Deciding Presburger arithmetic in agda
gallais/thesis
Syntaxes with Binding, Their Programs, and Proofs
gallais/CS410-2024
Content of the CS410 lectures
gallais/great-library-of-idris
A crowd-sourced list of papers using Idris
gallais/dot-analysis
Analysing dependency graphs produced by Agda
gallais/idris-free
Various Free-X experiments
gallais/gallais.github.io
My website, now generated using Hakyll
gallais/coolcat
not a wiki
gallais/ncurses-idris
A hobby implementation of an ncurses binding for Idris 2
gallais/sleepp
A sleep with a progress bar
gallais/aeson
A fast Haskell JSON library
gallais/agda
Agda is a dependently typed programming language / interactive theorem prover.
gallais/agda-stdlib
The Agda standard library
gallais/agda2hs
Compiling Agda code to readable Haskell
gallais/idrall
Dhall bindings for Idris
gallais/Idris2
A purely functional programming language with first class types
gallais/idris2-elab-util
Utilities and documentation for exploring idirs2's new elaborator reflection.
gallais/idris2-table
A table library for Idris 2
gallais/linear-circuits
Linear Circuits but not as we know it: Using Linear Types to enforce wiring decisions.
gallais/ola-lang
A small imperative language with ML-style references to play with CHERI Capabilities & Session-Types.
gallais/packer-idris
Packer scripts for generating Virtual Box OVFs that have Idris preinstalled.
gallais/plfa.github.io
Introduction to programming language theory in Agda
gallais/splv23.github.io
gallais/velo-lang
gallais/Yaffle
A core language and API for dependently typed languages
gallais/zwift
Easily zwift on linux