andreasabel/agda-scope andreasabel/agda-scope

  • Stars
    star
    3
  • Rank 3,963,521 (Top 79 %)
  • Language
    Haskell
  • Created over 5 years ago
  • Updated almost 3 years ago
Twitter logo Share LinkedIn logo Share Facebook logo Share
andreasabel/agda-scope
github

andreasabel

Reviews

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

Repository Details

Notes and prototypes concerning Agda's scope checker

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

proposal-agda-tutorial

Proposal for an Agda tutorial
Makefile
10
star
8

cabal-clean

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

universal-algebra

Formalization of some universal algebra in Agda
Agda
9
star
10

agda-automata

Formalisation of automata in Agda
Agda
8
star
11

shift-reset-dsl

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

ObjTT

Haskell
6
star
13

Sit

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

continuous-normalization

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

sized-types

Stuff concerning sized types.
TeX
5
star
16

fix-whitespace-action

Run fix-whitespace on your repo.
4
star
17

risc386

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

lambda-definability

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

pi-calculus

Agda formalization concerning processes
Agda
3
star
20

loop

Uwe Schรถnings LOOP language
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