• Stars
    star
    15
  • Rank 1,371,379 (Top 28 %)
  • Language Agda
  • License
    GNU General Publi...
  • Created over 6 years ago
  • Updated over 5 years ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

Agda suffices: software written from A to Z in Agda

More Repositories

1

agdarsec

Total Parser Combinators in Agda
Agda
123
star
2

idris-tparsec

TParsec - Total Parser Combinators in Idris
Idris
93
star
3

generic-syntax

A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs
Agda
68
star
4

potpourri

Where my everyday research happens
Agda
53
star
5

agda-sizedIO

IO using sized types and copatterns
Agda
33
star
6

aGdaREP

Implementing grep in Agda
Agda
32
star
7

agda-presburger

Deciding Presburger arithmetic in agda
Agda
31
star
8

typing-with-leftovers

Self-contained repository for the eponymous paper
Agda
29
star
9

pearl-binary-search

Functional Pearl: Certified Binary Search in a Read-Only Array
Idris
28
star
10

agda-nbe

Formalizing nbe in agda
25
star
11

thesis

Syntaxes with Binding, Their Programs, and Proofs
Makefile
23
star
12

type-scope-semantics

A self-contained repository for the paper Type and Scope Preserving Semantics
Agda
21
star
13

idris-tmustache

Total Logic-Less Templating Library
Idris
12
star
14

agdARGS

Dealing with Flags and Options
Agda
8
star
15

proof-search-ILLWiL

A self-contained repo for the ILLWiL paper
Agda
7
star
16

great-library-of-idris

A crowd-sourced list of papers using Idris
7
star
17

CS410-2024

Content of the CS410 lectures
Agda
6
star
18

dot-analysis

Analysing dependency graphs produced by Agda
Haskell
5
star
19

idris-free

Various Free-X experiments
Idris
4
star
20

MiniAgda-mode

An emacs mode for MiniAgda
Emacs Lisp
3
star
21

gallais.github.io

My website, now generated using Hakyll
Haskell
3
star
22

metamorphismsinagda

Haskell
3
star
23

STRINaGda

Dependent Stringly-Typed Programming
Agda
3
star
24

syntax-with-binding

A Generic Treatment of Syntaxes with Binding in Haskell
Haskell
2
star
25

ocaml-sparse-matrix

Implementation of Sparse Matrices in Ocaml using Batteries
OCaml
2
star
26

countdown

Haskell
1
star
27

agda-pretty-notgreedy

Port of Bernardy's Functional Pearl: A Pretty But Not Greedy Printer
Agda
1
star
28

coolcat

not a wiki
Lua
1
star
29

conkysh

An excuse to have a bit of fun with the Haskell X11 bindings
Haskell
1
star
30

idris-dhcli

Declarative Hierarchical Command Line Interfaces
Idris
1
star
31

sleepp

A sleep with a progress bar
Haskell
1
star
32

word-arithmetic

Arithmetic on unsigned integers, in Haskell
Haskell
1
star
33

dailyprogrammer

Solutions to problems found on /r/dailyprogrammer
Haskell
1
star