GitHub topics: agda

Repositories

fsestini/nbe-mltt-wes

Normalization by Evaluation for a version of Martin-Löf Type Theory with weak explicit substitutions.

Language: Agda - Size: 26.4 KB - Last synced at: 9 months ago - Pushed at: over 2 years ago - Stars: 6 - Forks: 0

choukh/agda-veblen

veblen function in agda

Language: Agda - Size: 182 KB - Last synced at: 6 months ago - Pushed at: about 1 year ago - Stars: 5 - Forks: 0

iwilare/formal-methods

Operational semantics, Type-based information flow security, Hoare logic, Verification conditions, and Separation logic in Agda for the IMP language

Language: Agda - Size: 32.2 KB - Last synced at: about 1 year ago - Pushed at: about 3 years ago - Stars: 14 - Forks: 1

PragmaTwice/TNT

some simple&naive formal proof of trivial Number Theory, using Agda/Coq, just to practice skills

Language: Agda - Size: 8.79 KB - Last synced at: 5 months ago - Pushed at: over 6 years ago - Stars: 8 - Forks: 1

AJChapman/agda-frp

Functional Reactive Programming in Agda, adapting [Conal Elliott's Push-Pull Functional Reactive Programming](http://conal.net/papers/push-pull-frp/push-pull-frp.pdf).

Language: Agda - Size: 59.6 KB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 0 - Forks: 0

kkd26/cam

Categorical Abstract Machine: Theory, Formalisation, Extensions

Language: Agda - Size: 102 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

Bicategories of automata, completeness of F-automata in monoidal categories, adjoints between (semi)bicategories; https://arxiv.org/pdf/2303.03867, https://arxiv.org/pdf/2303.03865, https://arxiv.org/abs/2305.00272

Language: Agda - Size: 578 KB - Last synced at: about 1 year ago - Pushed at: over 1 year ago - Stars: 15 - Forks: 1

yazaldefilimone/lambda-checker.agda

Language: Agda - Size: 1000 Bytes - Last synced at: 7 days ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

JonasHoefer/scoped-effects-agda

An implementation of scoped algebraic effects and handlers in Agda.

Language: TeX - Size: 13.7 MB - Last synced at: about 1 year ago - Pushed at: over 4 years ago - Stars: 11 - Forks: 0

yitzchak/dicy 📦

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

Language: TypeScript - Size: 2.23 MB - Last synced at: about 9 hours ago - Pushed at: over 6 years ago - Stars: 21 - Forks: 2

piotr-lewandowski/hoare-triples

Agda proof of soundness of Hoare Logic for a simple toy language

Language: Agda - Size: 10.7 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

choukh/MetaLogic

first-order logic and set theory

Language: Agda - Size: 616 KB - Last synced at: 3 months ago - Pushed at: over 1 year ago - Stars: 2 - Forks: 0

yitzchak/atom-dicy 📦

Compile LaTeX, knitr, literate Agda, literate Haskell and Pweave documents using DiCy from within Atom

Language: TypeScript - Size: 94.7 KB - Last synced at: over 1 year ago - Pushed at: over 6 years ago - Stars: 2 - Forks: 0

Mari-W/System-Fo

formal proof of type preservation of the dictionary passing transform for system f

Language: Agda - Size: 13.1 MB - Last synced at: over 1 year ago - Pushed at: over 2 years ago - Stars: 2 - Forks: 0

oisdk/agda-ring-solver 📦

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

Language: Agda - Size: 6.07 MB - Last synced at: over 1 year ago - Pushed at: over 3 years ago - Stars: 38 - Forks: 4

yazaldefilimone/lambda-normalizer

seeking to understand patterns behind a normalizer for typed lambda calculus with type affinities.

Language: TypeScript - Size: 82 KB - Last synced at: 7 days ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

jmlowenthal/staged-streams.agda

An implementation of the staged Strymonas streams library in Agda for C

Language: Haskell - Size: 309 KB - Last synced at: over 1 year ago - Pushed at: about 5 years ago - Stars: 8 - Forks: 1

JonathanBrouwer/research-project

Language: Agda - Size: 4.06 MB - Last synced at: over 1 year ago - Pushed at: about 4 years ago - Stars: 2 - Forks: 0

ajrouvoet/implicits.agda

Mechanized formalization of Implicit resolution in Agda

Language: Agda - Size: 510 KB - Last synced at: over 1 year ago - Pushed at: about 8 years ago - Stars: 6 - Forks: 0

andreasabel/agda-automata

Formalisation of automata in Agda

Language: Agda - Size: 218 KB - Last synced at: 3 months ago - Pushed at: over 1 year ago - Stars: 8 - Forks: 0

yurrriq/word-processing-in-groups

:book: Word Processing in Groups

Language: TeX - Size: 39.1 KB - Last synced at: 6 months ago - Pushed at: almost 8 years ago - Stars: 1 - Forks: 0

gonzigaran/agda-clones

Formalizing the clone theory in type theory and Agda

Language: HTML - Size: 1.43 MB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 0 - Forks: 0

yazaldefilimone/type-theory

Language: Agda - Size: 48.8 KB - Last synced at: 7 days ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

septembraljourney/agda-files-survey-HoTT

Agda files used for a survey paper on Homotopy Type Theory

Size: 1.54 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

appliedfm/growth-data

Measuring the growth of open source formal methods

Language: Python - Size: 36.6 MB - Last synced at: 17 days ago - Pushed at: 17 days ago - Stars: 4 - Forks: 0

FilippoFantinato/type-theory

Type Theory course ; Master's Degree in Computer Science @ UniPD

Language: Agda - Size: 53.7 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

juniors90/CALP-beamer

Notes about "An introduction to Finite Group Representation Theory using Agda"

Language: TeX - Size: 2.33 MB - Last synced at: 20 days ago - Pushed at: almost 3 years ago - Stars: 1 - Forks: 0

frex-project/agda-fragment

Algebraic proof discovery in Agda

Language: Agda - Size: 2.39 MB - Last synced at: over 1 year ago - Pushed at: almost 4 years ago - Stars: 31 - Forks: 2

gallais/agda-sizedIO

IO using sized types and copatterns

Language: Agda - Size: 4.56 MB - Last synced at: 5 months ago - Pushed at: over 4 years ago - Stars: 33 - Forks: 1

doofin/hott-examples

Homotopy type theory for theorem proving with univalence

Language: Agda - Size: 1.47 MB - Last synced at: 6 days ago - Pushed at: almost 4 years ago - Stars: 8 - Forks: 0

lclem/agda-kernel

An experimental Agda kernel for Jupyter

Language: Jupyter Notebook - Size: 19.9 MB - Last synced at: 4 days ago - Pushed at: over 3 years ago - Stars: 24 - Forks: 2

jmlowenthal/agda-c

Verified C programming in Agda

Language: Agda - Size: 273 KB - Last synced at: over 1 year ago - Pushed at: over 4 years ago - Stars: 16 - Forks: 1

vikraman/generalised-species

Espèces généralisées de structures sur les groupoïdes

Language: Agda - Size: 150 KB - Last synced at: 7 months ago - Pushed at: about 3 years ago - Stars: 5 - Forks: 1

wrrnhttn/agda-cubical-multidimensional

Multidimensional data in Cubical Agda.

Language: Agda - Size: 81.1 KB - Last synced at: over 1 year ago - Pushed at: over 5 years ago - Stars: 0 - Forks: 0

copumpkin/categories

Categories parametrized by morphism equality, in Agda

Language: Agda - Size: 772 KB - Last synced at: over 1 year ago - Pushed at: about 6 years ago - Stars: 148 - Forks: 27

mr-ohman/logrel-mltt

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

Language: Agda - Size: 4.2 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 40 - Forks: 10

divipp/frp_agda 📦

Functional Reactive Programming with Agda

Size: 51.8 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 26 - Forks: 1

ernius/formalmetatheory-nominal

Alpha-Structural Induction and Recursion for the Lambda Calculus in Constructive Type Theory

Language: Agda - Size: 7.08 MB - Last synced at: over 1 year ago - Pushed at: over 7 years ago - Stars: 6 - Forks: 2

ice1k/ConsHoTT

Constructive Interpretations of HoTT

Language: TeX - Size: 148 KB - Last synced at: over 1 year ago - Pushed at: about 5 years ago - Stars: 36 - Forks: 1

ice1k/Theorems

:globe_with_meridians: Theorems that rule this multiverse

Language: Agda - Size: 76.2 KB - Last synced at: about 2 months ago - Pushed at: almost 7 years ago - Stars: 11 - Forks: 2

Jlobblet/advent-of-code-2022

Solutions to Advent of Code 2022 in Lots of Languages

Language: Agda - Size: 83 KB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 1 - Forks: 1

ettorealdrovandi/agda-mas5932

Homotopy Type Theory and categorical algebra experiments in the style of UniMath

Language: Agda - Size: 148 KB - Last synced at: almost 2 years ago - Pushed at: about 3 years ago - Stars: 2 - Forks: 0

scott-fleischman/agda-from-nothing-2017

Agda from Nothing: Order in the Types

Language: Agda - Size: 553 KB - Last synced at: 5 months ago - Pushed at: over 8 years ago - Stars: 13 - Forks: 0

altriasjy31/agda_agda_ag_ag_da

play, just play, programming in agda for which is the best probably

Size: 2.93 KB - Last synced at: almost 2 years ago - Pushed at: almost 7 years ago - Stars: 0 - Forks: 0

fzipp/agda-life

Conway's Game of Life in Agda.

Language: Agda - Size: 2.93 KB - Last synced at: 6 months ago - Pushed at: almost 4 years ago - Stars: 0 - Forks: 1

AtticusKuhn/parallel-algorithms

Proving the correctness and performance of certain parallel algorithms

Language: TeX - Size: 111 KB - Last synced at: 2 months ago - Pushed at: about 2 years ago - Stars: 4 - Forks: 0

L-TChen/MtacAR

Mtac in Agda

Language: Agda - Size: 98.6 KB - Last synced at: 5 months ago - Pushed at: over 4 years ago - Stars: 28 - Forks: 0

jonaprieto/athena 📦

Translates Metis ATP proofs to the Agda code

Language: TeX - Size: 15.1 MB - Last synced at: over 1 year ago - Pushed at: over 5 years ago - Stars: 6 - Forks: 2

agda-web/agda-codemirror-alpha 📦

Source code of Agda mode on CodeMirror Next.

Language: JavaScript - Size: 7.46 MB - Last synced at: about 2 years ago - Pushed at: almost 5 years ago - Stars: 0 - Forks: 0

freeman42x/formalize-all-the-things

Proofs about General Intelligence, Narow Intelligence, Ethics, etc.

Language: Agda - Size: 23.4 KB - Last synced at: about 2 years ago - Pushed at: about 2 years ago - Stars: 4 - Forks: 0

ernius/mergesort

Merge sort correctness proof

Language: Agda - Size: 800 KB - Last synced at: over 1 year ago - Pushed at: over 10 years ago - Stars: 10 - Forks: 0

HoTT-Intro/Agda

Agda formalisation of the Introduction to Homotopy Type Theory

Language: Agda - Size: 6.82 MB - Last synced at: almost 2 years ago - Pushed at: almost 4 years ago - Stars: 110 - Forks: 4

dfirsov/agda-programming-with-finite-sets

Dependently Typed Programming with Finite Sets

Language: Agda - Size: 35.2 KB - Last synced at: about 2 years ago - Pushed at: about 3 years ago - Stars: 0 - Forks: 0

seanpm2001/AI2001_Category-Source_Code-SC-Agda

🧠️🖥️2️⃣️0️⃣️0️⃣️1️⃣️💾️📜️ The sourceCode:Agda category for AI2001, containing Agda programming language datasets

Language: R - Size: 2.47 MB - Last synced at: 6 days ago - Pushed at: over 2 years ago - Stars: 3 - Forks: 1

BitFunctor/bitfunctor

Decentralized blockchain-based storage of the automatically-verifiably correct (certified) code as well as generalized blockchain platform

Language: Haskell - Size: 246 KB - Last synced at: about 2 years ago - Pushed at: almost 8 years ago - Stars: 3 - Forks: 0

andreasabel/agda-earley-parsing Fork of hexointed/DATX05

A verified Agda implementation of the Earley parser for context-free languages

Size: 3.08 MB - Last synced at: about 2 years ago - Pushed at: almost 5 years ago - Stars: 0 - Forks: 0

splintersuidman/combinatory-logic

Explorations in combinatory logic with Agda

Language: Agda - Size: 2.03 MB - Last synced at: about 2 years ago - Pushed at: about 4 years ago - Stars: 2 - Forks: 0

sergey-goncharov/hybrid-agda

Duration monad and hybrid semantics in cubical Agda

Language: Agda - Size: 59.6 KB - Last synced at: about 2 years ago - Pushed at: over 5 years ago - Stars: 1 - Forks: 0

superhaNds/cwfs

Formalization of Categories with Families

Language: Agda - Size: 1.45 MB - Last synced at: about 2 years ago - Pushed at: almost 4 years ago - Stars: 13 - Forks: 0

metaborg/mj.agda

https://metaborg.github.io/mj.agda/

Language: Agda - Size: 1.91 MB - Last synced at: over 1 year ago - Pushed at: almost 5 years ago - Stars: 12 - Forks: 1

iwilare/categorical-qtl

Categorical semantics of counterpart-based quantified (linear) temporal logics in Agda using https://github.com/agda/agda-categories

Language: Agda - Size: 409 KB - Last synced at: about 1 year ago - Pushed at: almost 3 years ago - Stars: 6 - Forks: 0

banacorn/agda-mode 📦

agda-mode on Atom

Language: Reason - Size: 32.8 MB - Last synced at: over 1 year ago - Pushed at: over 4 years ago - Stars: 59 - Forks: 14

mihanus/curry-agda

Agda proofs for properties of Curry operations

Language: Agda - Size: 11.7 KB - Last synced at: about 2 years ago - Pushed at: almost 9 years ago - Stars: 1 - Forks: 0

marcinjangrzybowski/cubeViz2

Language: Haskell - Size: 6.66 MB - Last synced at: about 2 years ago - Pushed at: about 2 years ago - Stars: 18 - Forks: 2

fredefox/cat

A formalization of category theory in cubical Agda

Language: Agda - Size: 3.96 MB - Last synced at: about 2 years ago - Pushed at: over 5 years ago - Stars: 53 - Forks: 4

fjpub/itfj

An Inherently-Typed Formalization for Featherweight Java

Language: Agda - Size: 15.6 KB - Last synced at: about 2 years ago - Pushed at: over 6 years ago - Stars: 2 - Forks: 0

joom/modal

Compilation of modal logic based functional language ML5 to JavaScript.

Language: Agda - Size: 106 KB - Last synced at: about 1 month ago - Pushed at: over 8 years ago - Stars: 9 - Forks: 1

MetaBorgCube/brp-agda-refactoring-mjozwik

Correct-by-construction refactoring of functional code Provided by Programming Languages for the Research Project 2022/2023 Q4 course.

Language: Agda - Size: 39.1 KB - Last synced at: over 1 year ago - Pushed at: about 2 years ago - Stars: 1 - Forks: 0

MetaBorgCube/brp-agda-refactoring-jbastenhof

Correct-by-construction refactoring of functional code Provided by Programming Languages for the Research Project 2022/2023 Q4 course.

Language: Agda - Size: 60.5 KB - Last synced at: 9 months ago - Pushed at: about 2 years ago - Stars: 0 - Forks: 1

andreasabel/pfm-lambda Fork of axelf4/pfm-lambda

Parametric Fitch-style modal lambda calculus

Language: Agda - Size: 981 KB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 2 - Forks: 0

andreasabel/continuous-normalization

Evaluation of typed terms in Agda using the Delay monad.

Language: Agda - Size: 243 KB - Last synced at: 4 months ago - Pushed at: over 2 years ago - Stars: 5 - Forks: 1

fsestini/hs2agda-plugin

GHC Core plugin for lightweight formal verification of Haskell programs via Agda.

Language: Haskell - Size: 26.4 KB - Last synced at: 9 months ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0

Eggy115/Agda

Agda

Language: Agda - Size: 33.2 KB - Last synced at: 6 months ago - Pushed at: over 2 years ago - Stars: 2 - Forks: 1

fsestini/nbe-weak-stlc

Agda formalization of normalization by evaluation for the confluent simply-typed weak lambda-calculus.

Language: Agda - Size: 29.3 KB - Last synced at: 9 months ago - Pushed at: over 2 years ago - Stars: 8 - Forks: 0

uedatakumi/nat

Natural Numbers

Language: Agda - Size: 3.91 KB - Last synced at: 11 days ago - Pushed at: over 2 years ago - Stars: 1 - Forks: 0

codewars/codemirror-agda

Agda mode and input helper for CodeMirror used on Codewars

Language: TypeScript - Size: 63.5 KB - Last synced at: 24 days ago - Pushed at: 11 months ago - Stars: 6 - Forks: 3

kotoromo/IntroAgda

Material para una exposición dada el Miércoles 2 de Marzo del 2023 sobre una introducción a Agda como asistente de pruebas y a la Teoría Homotópica de Tipos.

Language: HTML - Size: 1.14 MB - Last synced at: over 2 years ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0

desi-ivanov/agda-regexp-automata

Formalization of Regular Languages in Agda: regular expressions, finite-state automata, proof of equivalence, proof of the pumping lemma.

Language: Agda - Size: 840 KB - Last synced at: over 2 years ago - Pushed at: about 5 years ago - Stars: 7 - Forks: 0

ualib/ualib.github.io

The Agda Universal Algebra Library (UALib) is a library of types and programs (theorems and proofs) that formalizes the foundations of universal algebra in dependent type theory using the Agda proof assistant language.

Language: TeX - Size: 52.7 MB - Last synced at: over 2 years ago - Pushed at: over 3 years ago - Stars: 19 - Forks: 2