agda

Star

Here are 146 public repositories matching this topic...

agda / agda

Star

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

programming-language dependent-types proof-assistant type-theory agda

Updated Aug 12, 2020
Haskell

HoTT / HoTT-Agda

Star

Development of homotopy type theory in Agda

agda homotopy hott univalence

Updated Feb 19, 2019
Agda

agda / agda-stdlib

Star

The Agda standard library

library proof agda

Updated Aug 10, 2020
Agda

EgbertRijke / HoTT-Intro

Star

An introductory course to Homotopy Type Theory

book coq mathematics agda formalization hott univalence

Updated Jul 24, 2020
Agda

martinescardo / HoTT-UF-Agda-Lecture-Notes

Star

Lecture notes on univalent foundations of mathematics with Agda

dependent-types type-theory agda lecture-notes mltt homotopy-type-theory univalent-foundations univalent-mathematics hott-uf martin-lof-type-theory univalence-axiom function-extensionality propositional-truncation univalent-type-theory

Updated Jun 29, 2020
Agda

copumpkin / categories

Star

Categories parametrized by morphism equality, in Agda

category-theory agda

Updated Aug 9, 2019
Agda

awesomo4000 / awesome-provable

Star

A curated set of links to formal methods involving provable code.

coq idris agda isabelle formal-verification isabelle-hol sel4 certified-programming

Updated Jul 23, 2019

ilya-klyuchnikov / ttlite

Star

A SuperCompiler for Martin-Löf's Type Theory

programming-language dependent-types coq type-theory idris agda supercompilation

Updated Jun 8, 2020
Scala

martinescardo / TypeTopology

Star

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

type-theory agda ordinal homotopy-type-theory univalent-foundations constructive-mathematics compact-type totally-separated-type injective-type searchable-set univalent-mathematics

Updated Aug 11, 2020
Agda

scott-fleischman / agda-from-nothing

Star

A workshop on learning Agda with minimal prerequisites.

dependent-types agda learning-agda

Updated May 26, 2016
Agda

alhassy / next-700-module-systems

Star

PhD research ;; What's the difference between a typeclass/trait and a record/class/struct? Nothing really, or so I argue.

language haskell lisp emacs modules records ocaml metaprogramming coq agda phd typeclasses first-class-citizens canonical-structures

Updated Jul 20, 2020
TeX

banacorn / agda-mode

Star

agda-mode on Atom

atom agda agda-mode

Updated Jul 30, 2020
Reason

algebraic-graphs / agda

Star

The theory of algebraic graphs formalised in Agda

algebra graph agda

Updated Jul 15, 2018
Agda

gallais / agdarsec

Star

Total Parser Combinators in Agda

parser-combinators agda

Updated Apr 16, 2020
Agda

gallais / generic-syntax

Star

A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs

semantic proof generic-programming agda

Updated Mar 7, 2020
Agda

fredefox / cat

Star

A formalization of category theory in cubical Agda

category-theory agda homotopy-type-theory

Updated May 24, 2020
Agda

alhassy / gentle-intro-to-reflection

Star

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

tutorial exercise tactics agda macro proof-pattern

Updated May 3, 2020
Agda

jespercockx / ataca

Star

A TACtic library for Agda

dependent-types metaprogramming tactics agda proof-search

Updated Mar 14, 2019
Agda

scott-fleischman / greek-grammar

Star

Modeling Ancient Greek Grammar

haskell morphology grammar greek phonology ancient-greek agda

Updated May 11, 2018
Agda

wenkokke / AutoInAgda

Star

Proof automation – for Agda, in Agda.

paper proof-assistant agda no-longer-maintained proof-automation

Updated Oct 8, 2018
Agda

oisdk / agda-ring-solver

Star

A fast, easy-to-use ring solver for agda with step-by-step solutions

agda interactive-theorem-proving agda-library

Updated Nov 21, 2019
Agda

gallais / agda-sizedIO

Star

IO using sized types and copatterns

experimental bindings agda directory-tree filepath input-output coinductive-types sized-types

Updated Oct 1, 2019
Agda

agda / agda-pkg

Star

apkg - package manager for Agda

package-manager agda lightweight-dependency-management

Updated Jul 1, 2020
Python

ice1000 / ConsHoTT

Star

Constructive Interpretations of HoTT

agda hott

Updated Jul 27, 2020
TeX

L-TChen / MtacAR

Star

Mtac in Agda

reflection metaprogramming coq tactics monad agda

Updated Aug 3, 2020
Agda

gallais / agda-presburger

Star

Deciding Presburger arithmetic in agda

agda formalization decision-procedure presburger-arithmetic

Updated Dec 23, 2019
Agda

alhassy / AgdaCheatSheet

Star

Basics of the dependently-typed functional language Agda ^_^

html pdf emacs cheatsheet agda

Updated Apr 29, 2020
Agda

wenkokke / msla2014

Star

wherein I implement several substructural logics in Agda

paper agda substructural-logics

Updated Oct 8, 2018
Agda

jpvillaisaza / cain

Star

Category theory applied to functional programming (undergraduate project)

haskell functional-programming category-theory agda

Updated Feb 17, 2019
TeX

mr-ohman / logrel-mltt

Star

A Logical Relation for Martin-Löf Type Theory in Agda

type-theory agda

Updated Jun 26, 2020
Agda

Improve this page

Add a description, image, and links to the agda topic page so that developers can more easily learn about it.

Curate this topic

Add this topic to your repo

To associate your repository with the agda topic, visit your repo's landing page and select "manage topics."

Learn more