Top 84 Agda open source projects

Agda is a dependently typed programming language / interactive theorem prover.

I'm putting Palmgren's Constructive Sheaf Semantics into Agda. Defines sheaves via Grothendieck pretopologies.

Agda formalisation of dual-context constructive modal logics.

A tool for formally verifying Haskell code in Agda

No description, website, or topics provided.

A workshop on learning Agda with minimal prerequisites.

being the materials for CS410 Advanced Functional Programming in the 2014-15 session

The theory of algebraic graphs formalised in Agda

Cartesian Cubical Type Theory

A simple, untyped, terminating functional language that is fully compatible with optimal reductions.

A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory

The notes for 320

Code for keep an investment trade journal

being the materials for CS410 Advanced Functional Programming in the 2015/16 session

Refinement types + dependent types = ❤️

A slow-paced introduction to reflection in Agda. ---Tactics!

Files for the tutorial "Correct-by-construction programming in Agda" at POPL '19 in Cascais

Agda libraries relevant to Moonad

Mtac in Agda

Self-contained repository for the eponymous paper

Staged compilation with dependent types

Using Type-Level Programming in Rust to Make Safer Hardware Abstractions

Implementation for ICFP 2020 paper

A builder for LaTeX, knitr, literate Agda, literate Haskell and Pweave that automatically builds dependencies.

A library and case-study for linear, intrinsically-typed interpreters in Agda

Mechanization of Hazelnut, as submitted to POPL 2017

Specification of Agda.

Attracting mathematicians (others welcome too) with no experience in proof verification interested in HoTT and able to use Agda for HoTT

wherein I implement several substructural logics in Agda

A fast, small, safe, gradually typed embeddable scripting language derived from Lua

Constructive Galois connections

Formalizations of Gradually Typed Languages in Agda

Constructive Interpretations of HoTT

Translation of, and commentary on, Joyal's classic paper "Une théorie combinatoire des séries formelles" (A combinatorial theory of formal series)

Nat, Fin, Vec

Juvix empowers developers to write code in a high-level, functional language, compile it to gas-efficient output VM instructions, and formally verify the safety of their contracts prior to deployment and execution.

The Evolution of a Typechecker

apkg - package manager for Agda

Inline, type safe X86-64 assembly programming in Agda

being an experiment with potato power

being the materials for a paper I have in mind to write about the bidirectional discipline

Paper about polynomial functors, regular expressions, matrices of types, derivatives, semirings, and other cool stuff

A library for doing generic programming in Agda

Abstract binding trees (abstract syntax trees plus binders), as a library in Agda

No description, website, or topics provided.

Automatically exported from code.google.com/p/trellys

being a collection of Agda-facilitated ramblings

Deciding Presburger arithmetic in agda

Research material of Erik Palmgren (1963–2019)

Proof automation – for Agda, in Agda.