Topic: agda Goto Github

👇 Here are 252 public repositories matching this topic...

agda / agda
agda,Agda is a dependently typed programming language / interactive theorem prover.
Organization: agda
Home Page: https://wiki.portal.chalmers.se/agda/pmwiki.php
dependent-types programming-language proof-assistant agda type-theory

agda / agda-language-server
agda,Language Server for Agda
Organization: agda
agda agda-mode language-server-protocol

agda / agda-pkg
agda,apkg - package manager for Agda
Organization: agda
Home Page: https://agda.github.io/agda-pkg/
agda package-manager lightweight-dependency-management

agda / agda-stdlib
agda,The Agda standard library
Organization: agda
Home Page: https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
agda library proof

agda / cubical
agda,An experimental library for Cubical Agda
Organization: agda
Home Page: https://agda.github.io/cubical/Cubical.README.html
agda cubical-type-theory library

algebraic-graphs / agda
agda,The theory of algebraic graphs formalised in Agda
Organization: algebraic-graphs
algebra graph agda

alhassy / agdacheatsheet
agda,Basics of the dependently-typed functional language Agda ^_^
User: alhassy
agda cheatsheet pdf html emacs

alhassy / gentle-intro-to-reflection
agda,A slow-paced introduction to reflection in Agda. ---Tactics!
User: alhassy
agda tactics tutorial proof-pattern macro exercise

alhassy / next-700-module-systems
agda,PhD research ;; What's the difference between a typeclass/trait and a record/class/struct? Nothing really, or so I argue.
User: alhassy
agda phd emacs lisp ocaml coq modules typeclasses records canonical-structures

awesomo4000 / awesome-provable
agda,A curated set of links to formal methods involving provable code.
User: awesomo4000
formal-verification certified-programming sel4 coq isabelle isabelle-hol idris agda

banacorn / agda-mode
agda,agda-mode on Atom
User: banacorn
Home Page: https://atom.io/packages/agda-mode
agda agda-mode atom

banacorn / agda-mode-vscode
agda,agda-mode on VS Code
User: banacorn
Home Page: https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode
agda agda-mode vscode vscode-extension reasonml

copumpkin / categories
agda,Categories parametrized by morphism equality, in Agda
User: copumpkin
category-theory agda

effectfully / inference-in-agda
agda,A tutorial on how Agda infers things
User: effectfully
Home Page: https://raw.githack.com/effectfully/inference-in-agda/master/InferenceInAgda.html
agda

egbertrijke / hott-intro
agda,An introductory course to Homotopy Type Theory
User: egbertrijke
agda hott univalence book coq formalization mathematics

fredefox / cat
agda,A formalization of category theory in cubical Agda
User: fredefox
agda category-theory homotopy-type-theory

frex-project / agda-fragment
agda,Algebraic proof discovery in Agda
Organization: frex-project
formal-verification agda universal-algebra

gallais / agda-presburger
agda,Deciding Presburger arithmetic in agda
User: gallais
agda presburger-arithmetic formalization decision-procedure

gallais / agda-sizedio
agda,IO using sized types and copatterns
User: gallais
Home Page: https://gallais.github.io/agda-sizedIO/README.html
agda input-output coinductive-types sized-types bindings experimental directory-tree filepath

gallais / agdarsec
agda,Total Parser Combinators in Agda
User: gallais
Home Page: https://gallais.github.io/agdarsec/
parser-combinators agda

gallais / generic-syntax
agda,A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs
User: gallais
Home Page: https://gallais.github.io/generic-syntax/Generic.html
agda semantic proof generic-programming

hott-intro / agda
agda,Agda formalisation of the Introduction to Homotopy Type Theory
Organization: hott-intro
hott-uf agda textbook univalent-foundations univalence univalent-mathematics univalence-axiom homotopy-type-theory mathematics mathematics-library

hott / hott-agda
agda,Development of homotopy type theory in Agda
Organization: hott
agda homotopy hott univalence

ice1000 / agda-mode
agda,Accessing Agda's interaction mode via command line & external tactic for Agda.
User: ice1000
agda command-line-tool

ice1k / conshott
agda,Constructive Interpretations of HoTT
Organization: ice1k
hott agda

ilya-klyuchnikov / ttlite
agda,A SuperCompiler for Martin-Löf's Type Theory
User: ilya-klyuchnikov
supercompilation programming-language dependent-types type-theory agda idris coq

intersectmbo / formal-ledger-specifications
agda,Formal specifications of the cardano ledger
Organization: intersectmbo
agda cardano-node formal-methods

isovector / certainty-by-construction
agda,Source material for Certainty by Construction
User: isovector
Home Page: https://leanpub.com/certainty-by-construction/
agda book functional-programming math

isovector / cornelis
agda,agda-mode for neovim
User: isovector
nvim-hs neovim agda vim-textobj-user vim-which-key

jespercockx / agda-core
agda,A work-in-progress core language for Agda, in Agda
User: jespercockx
agda agda-backend core-language dependent-types type-checker

jespercockx / ataca
agda,A TACtic library for Agda
User: jespercockx
dependent-types agda metaprogramming tactics proof-search

jonsterling / agda-calf
agda,A cost-aware logical framework, embedded in Agda.
User: jonsterling
Home Page: https://jonsterling.github.io/agda-calf/
logical-framework agda cost complexity modal-type-theory

jpvillaisaza / cain
agda,Category theory applied to functional programming (undergraduate project)
User: jpvillaisaza
Home Page: https://jpvillaisaza.co/cain/cain.pdf
category-theory functional-programming haskell agda

l-tchen / mtacar
agda,Mtac in Agda
User: l-tchen
agda reflection monad metaprogramming tactics coq

langston-barrett / write-yourself-a-scheme-in-agda
agda,Like "Write Yourself a Scheme in 48 Hours", but in Agda
User: langston-barrett
agda tutorial scheme

lclem / agda-kernel
agda,An experimental Agda kernel for Jupyter
User: lclem
agda jupyter jupyter-notebook

martinescardo / hott-uf-agda-lecture-notes
agda,Lecture notes on univalent foundations of mathematics with Agda
User: martinescardo
hott-uf univalent-foundations univalent-mathematics agda homotopy-type-theory mltt martin-lof-type-theory lecture-notes dependent-types univalence-axiom

martinescardo / typetopology
agda,Logical manifestations of topological concepts, and other things, via the univalent point of view.
User: martinescardo
univalent-foundations agda homotopy-type-theory type-theory constructive-mathematics compact-type totally-separated-type injective-type ordinal searchable-set

mr-ohman / logrel-mltt
agda,A Logical Relation for Martin-Löf Type Theory in Agda
User: mr-ohman
agda type-theory

oisdk / agda-ring-solver
agda,A fast, easy-to-use ring solver for agda with step-by-step solutions
User: oisdk
Home Page: https://oisdk.github.io/agda-ring-solver/README.html
agda agda-library interactive-theorem-proving

plt-amy / 1lab
agda,A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory
User: plt-amy
Home Page: https://1lab.dev
homotopy-type-theory agda

scott-fleischman / agda-from-nothing
agda,A workshop on learning Agda with minimal prerequisites.
User: scott-fleischman
agda learning-agda dependent-types

scott-fleischman / greek-grammar
agda,Modeling Ancient Greek Grammar
User: scott-fleischman
Home Page: https://scott-fleischman.github.io/greek-grammar
haskell agda greek morphology grammar phonology ancient-greek

tree-sitter / tree-sitter-agda
agda,Agda grammar for tree-sitter
Organization: tree-sitter
tree-sitter context-free-grammar syntax-highlighting agda

ualib / agda-algebras
agda,The Agda Universal Algebra Library (html docs available at the url below)
Organization: ualib
Home Page: https://ualib.github.io/agda-algebras/
agda-library universal-algebra logic foundations type-theory agda model-theory dependent-types

vehicle-lang / vehicle
agda,A toolkit for enforcing logical specifications on neural networks
Organization: vehicle-lang
Home Page: https://vehicle-lang.readthedocs.io/
agda haskell neural-network specification verification

wenkokke / autoinagda
agda,Proof automation – for Agda, in Agda.
User: wenkokke
Home Page: https://wenkokke.github.io/pubs/mpc2015.pdf
paper proof-automation proof-assistant no-longer-maintained agda

wenkokke / msla2014
agda,wherein I implement several substructural logics in Agda
User: wenkokke
paper agda substructural-logics

wenkokke / schmitty
agda,Agda bindings to SMT-LIB2 compatible solvers.
User: wenkokke
agda smt-solver

xgrommx / agda-ecosystem
agda,
User: xgrommx
agda ecosystem agda-ecosystem