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/agda-sizedIO
IO using sized types and copatterns
gallais/aGdaREP
Implementing grep in Agda
gallais/typing-with-leftovers
Self-contained repository for the eponymous paper
gallais/pearl-binary-search
Functional Pearl: Certified Binary Search in a Read-Only Array
gallais/type-scope-semantics
A self-contained repository for the paper Type and Scope Preserving Semantics
gallais/agdarky
Agda suffices: software written from A to Z in Agda
gallais/agdARGS
Dealing with Flags and Options
gallais/metamorphismsinagda
gallais/STRINaGda
Dependent Stringly-Typed Programming
gallais/agda-pretty-notgreedy
Port of Bernardy's Functional Pearl: A Pretty But Not Greedy Printer
gallais/idris-dhcli
Declarative Hierarchical Command Line Interfaces
gallais/agda-categories
A new Categories library
gallais/agda-fragment
Algebraic proof discovery in Agda
gallais/dddp
Deferring the Details and Deriving Programs
gallais/EGTBS
being the introduction to co-de-Bruijn metasyntax
gallais/hello-idris2
A template for idris projects
gallais/homebrew-core
🍻 Default formulae for the missing package manager for macOS
gallais/idris-frex
gallais/idris2-mode
Idris2 syntax highlighting, compiler-supported editing, interactive REPL and more things for Emacs.
gallais/martin-lof
papers of Per Martin Löf
gallais/mcb
Mathematical Components (the Book)
gallais/nary
Self-contained repository for the corresponding TyDe'19 paper
gallais/newtype
gallais/polymode
Framework for Multiple Major Modes in Emacs (core library)
gallais/prettiest
The Prettiest Printer
gallais/schmitty
Agda bindings to SMT-LIB2 compatible solvers.
gallais/setup-scheme
Github Actions CI / CD setup for Scheme
gallais/SPLV20
SPLV20 course notes
gallais/strong-normalization
Formalizations of strong normalization proofs
gallais/TypesWhoSayNi
being the materials for a paper I have in mind to write about the bidirectional discipline