andreasabel/proposal-agda-tutorial andreasabel/proposal-agda-tutorial

  • Stars
    star
    10
  • Rank 1,807,489 (Top 36 %)
  • Language Makefile
  • Created about 6 years ago
  • Updated about 6 years ago
Twitter logo Share LinkedIn logo Share Facebook logo Share
andreasabel/proposal-agda-tutorial
github

andreasabel

Reviews

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

Repository Details

Proposal for an Agda tutorial

More Repositories

1

miniagda

A prototypical dependently typed languages with sized types and variances
Haskell
95
star
2

strong-normalization

Formalizations of strong normalization proofs
TeX
34
star
3

helf

Haskell implementation of the Edinburgh Logical Framework
Haskell
24
star
4

ipl

Agda formalization of Intuitionistic Propositional Logic
TeX
22
star
5

java-adt

A tool to create immutable algebraic data structures and visitors for Java (such as abstract syntax trees).
Haskell
17
star
6

agda2lagda

Simple conversion from Agda text to literate Agda text.
Haskell
14
star
7

cabal-clean

Remove outdated compilation artefacts left by cabal v2-build
Haskell
9
star
8

universal-algebra

Formalization of some universal algebra in Agda
Agda
9
star
9

agda-automata

Formalisation of automata in Agda
Agda
8
star
10

shift-reset-dsl

A DSL for shift and reset in Agda
Agda
6
star
11

ObjTT

Haskell
6
star
12

Sit

Prototypical type checker for Type Theory with Sized Natural Numbers
Haskell
6
star
13

continuous-normalization

Evaluation of typed terms in Agda using the Delay monad.
Agda
5
star
14

sized-types

Stuff concerning sized types.
TeX
5
star
15

fix-whitespace-action

Run fix-whitespace on your repo.
4
star
16

risc386

Interpreter for symbolic 386 assembler (small fragment) written in Haskell
Assembly
4
star
17

lambda-definability

Lambda-definability and NBE for simply-typed lambda-calculus and maybe beyond
Agda
4
star
18

pi-calculus

Agda formalization concerning processes
Agda
3
star
19

loop

Uwe Schรถnings LOOP language
Haskell
3
star
20

agda-scope

Notes and prototypes concerning Agda's scope checker
Haskell
3
star
21

agda-meeting-38-swansea

Agda
3
star
22

plt-agda

A compiler for a fragment of C using well-typed syntax and well-typed JVM instructions
Agda
2
star
23

aplas14

Agda and LaTeX sources for APLAS 2014 paper on strong normalization of guarded STLC
Agda
2
star
24

parametrized-modules

A core calculus for parametrized modules
Haskell
2
star
25

applicative

Haskell's applicative functors are multi-category functors
TeX
2
star
26

sbv-quarter-circle-puzzle

Solve a grid-based partitioning puzzle with SMT using Haskell's sbv library
Haskell
1
star
27

cubical

Agda formalization of cubical sets.
Agda
1
star
28

ini

Quick and easy INI configuration files for Haskell
Haskell
1
star
29

ci-executable-static

Test building static binary via Github workflow
Haskell
1
star
30

agda-issues

Statistics from the Agda issue tracker
Haskell
1
star
31

truthtable

Normalization for truth table natural deduction
TeX
1
star
32

ppdp20-www

Webpage and CFP for PPDP 2020
HTML
1
star
33

red-black-tree-left-leaning

Left-leaning red-black trees in Agda (insertion and deletion) with static ordering and balancing invariants
Agda
1
star
34

constraint-based-type-inference

Agda formalization of constraint-based type inference for the simply-typed lambda-calculus
Agda
1
star