andreasabel/universal-algebra andreasabel/universal-algebra

  • Stars
    star
    9
  • Rank 1,939,727 (Top 39 %)
  • Language Agda
  • Created over 3 years ago
  • Updated about 3 years ago
Twitter logo Share LinkedIn logo Share Facebook logo Share
andreasabel/universal-algebra
github

andreasabel

Reviews

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

Repository Details

Formalization of some universal algebra in Agda

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

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