agda

Star

Here are 162 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 May 9, 2021
Haskell

agda / agda-stdlib

Star

The Agda standard library

library proof agda

Updated May 7, 2021
Agda

HoTT / HoTT-Agda

Star

Development of homotopy type theory in Agda

agda homotopy hott univalence

Updated Feb 19, 2019
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 Apr 22, 2021
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 Mar 19, 2021
Scala

gallais / agdarsec

Star

Total Parser Combinators in Agda

parser-combinators agda

Updated Jan 11, 2021
Agda

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 May 8, 2021
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 Apr 29, 2021
TeX

algebraic-graphs / agda

Star

The theory of algebraic graphs formalised in Agda

algebra graph agda

Updated Jul 15, 2018
Agda

banacorn / agda-mode-vscode

Star

agda-mode on VS Code

vscode vscode-extension agda reasonml agda-mode

Updated Apr 9, 2021
ReScript

banacorn / agda-mode

Star

agda-mode on Atom

atom agda agda-mode

Updated Feb 26, 2021
Reason

HoTT-Intro / Agda

Star

Agda formalisation of the Introduction to Homotopy Type Theory

mathematics agda textbook univalence homotopy-type-theory univalent-foundations mathematics-library univalent-mathematics hott-uf univalence-axiom

Updated May 7, 2021
Agda

wenkokke / schmitty

Star

Agda bindings to SMT-LIB2 compatible solvers.

agda smt-solver

Updated Mar 5, 2021
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 Apr 16, 2021
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 Sep 16, 2020
Agda

jespercockx / ataca

Star

A TACtic library for Agda

dependent-types metaprogramming tactics agda proof-search

Updated Mar 14, 2019
Agda

wenkokke / AutoInAgda

Star

Proof automation – for Agda, in Agda.

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

Updated Sep 7, 2020
Agda

scott-fleischman / greek-grammar

Star

Modeling Ancient Greek Grammar

haskell morphology grammar greek phonology ancient-greek agda

Updated May 11, 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

ice1000 / ConsHoTT

Sponsor Star

Constructive Interpretations of HoTT

agda hott

Updated Aug 26, 2020
TeX

gallais / agda-sizedIO

Star

IO using sized types and copatterns

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

Updated Apr 14, 2021
Agda

agda / agda-pkg

Star

apkg - package manager for Agda

package-manager agda lightweight-dependency-management

Updated Mar 25, 2021
Python

L-TChen / MtacAR

Star

Mtac in Agda

reflection metaprogramming coq tactics monad agda

Updated May 4, 2021
Agda

alhassy / AgdaCheatSheet

Star

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

html pdf emacs cheatsheet agda

Updated Sep 16, 2020
Agda

gallais / agda-presburger

Star

Deciding Presburger arithmetic in agda

agda formalization decision-procedure presburger-arithmetic

Updated Dec 23, 2019
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