Top 84 Agda open source projects

Functional teaching language for use in a discrete mathematics course

Type Theory in Type Theory using Cubical Agda

Denotational-categorical design of verified hardware in Agda

A TACtic library for Agda

Compiling Agda code to readable Haskell

mirror of A simple type-theoretic language: Mini-TT

Where my everyday research happens

Like "Write Yourself a Scheme in 48 Hours", but in Agda

The Iowa Agda Library

Minimalistic dependent type theory with syntactic metaprogramming

A formalization of category theory in cubical Agda

Logical manifestations of topological concepts, and other things. This version adopts the univalent point of view.

Agda formalisation of NbE for λ□

A categorical semantics library in Agda.

AACMM's generic-syntax, but with QTT-style annotations

Functional Reactive Programming with Agda

A simple supercompiler formally verified in Agda

A universe of scope- and type-safe syntaxes (syntices?). Includes generic implementation of type-preserving renaming/substitution with all the proofs you could possibly need.

Simply typed lambda calculus in cubical agda

(λ) Category theory and lambda calculus, Bachelor's thesis

Formalization of Opetopes and Opetopic Sets in Agda

A collection of PLT researching

Deferring the Details and Deriving Programs

Agda proofs for some of the theorems in Robert Harper's Practical Foundations of Programming Languages.

Prototype implementations of systems based on setoid type theory

Category theory formalized in cubical agda

Algebraic proof discovery in Agda

being a bidirectional reformulation of Martin-Löf's 1971 type theory

Interactive and object-oriented programming in Agda using coinductive types

Companion code for "Why Dependent Types Matter" paper.

Agda libraries for the semantic web

being the lecture materials and exercises for the 2016/17 session of Advanced Functional Programming at Strathclyde

Two attempts at formalizing Löb's Theorem, (one based on http://lesswrong.com/lw/t6/the_cartoon_guide_to_l%C3%B6bs_theorem/)

System F-omega normalization by hereditary substitution in Agda