Discover @andreasabel Open Source projects

Andreas Abel (@andreasabel)

andreasabel

Stars
335
Global Rank 81,422 (Top 3 %)
Followers 264
Following 3
Registered about 13 years ago
Most used languages

Haskell
41.2 %

Agda 35.3 %

TeX
14.7 %

Makefile 2.9 %

Assembly
2.9 %

HTML
2.9 %
Location 🇸🇪 Sweden
Country Total Rank 944
Country Ranking

Agda 4

TeX
11

Haskell
12

Makefile 36

Assembly
56

HTML
1,801

miniagda

A prototypical dependently typed languages with sized types and variances

strong-normalization

Formalizations of strong normalization proofs

helf

Haskell implementation of the Edinburgh Logical Framework

ipl

Agda formalization of Intuitionistic Propositional Logic

java-adt

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

agda2lagda

Simple conversion from Agda text to literate Agda text.

proposal-agda-tutorial

Proposal for an Agda tutorial

cabal-clean

Remove outdated compilation artefacts left by cabal v2-build

universal-algebra

Formalization of some universal algebra in Agda

agda-automata

Formalisation of automata in Agda

shift-reset-dsl

A DSL for shift and reset in Agda

ObjTT

Sit

Prototypical type checker for Type Theory with Sized Natural Numbers

continuous-normalization

Evaluation of typed terms in Agda using the Delay monad.

sized-types

Stuff concerning sized types.

fix-whitespace-action

Run fix-whitespace on your repo.

risc386

Interpreter for symbolic 386 assembler (small fragment) written in Haskell

lambda-definability

Lambda-definability and NBE for simply-typed lambda-calculus and maybe beyond

pi-calculus

Agda formalization concerning processes

loop

Uwe Schönings LOOP language

agda-scope

Notes and prototypes concerning Agda's scope checker

agda-meeting-38-swansea

plt-agda

A compiler for a fragment of C using well-typed syntax and well-typed JVM instructions

aplas14

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

parametrized-modules

A core calculus for parametrized modules

applicative

Haskell's applicative functors are multi-category functors

sbv-quarter-circle-puzzle

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

cubical

Agda formalization of cubical sets.

ini

Quick and easy INI configuration files for Haskell

ci-executable-static

Test building static binary via Github workflow

agda-issues

Statistics from the Agda issue tracker

truthtable

Normalization for truth table natural deduction

ppdp20-www

Webpage and CFP for PPDP 2020

red-black-tree-left-leaning

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

constraint-based-type-inference

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