agda
Theorem prover
A system for specifying and proving mathematical theorems using a dependently typed language
Agda is a dependently typed programming language / interactive theorem prover.
3k stars
65 watching
362 forks
Language: Haskell
last commit: over 1 year ago
Linked from 3 awesome lists
agdadependent-typesprogramming-languageproof-assistanttype-theory
xgrommx/awesome-functional-programming
learn-anything/programming-languages
awesomo4000/awesome-provableRelated projects:
| Repository | Description | Stars |
|---|---|---|
| agda/agda2hs | Tools for translating Agda code to readable Haskell | 178 |
 typelead/eta-hackage | Patches to make Hackage compatible with Eta language | 64 |
 andreasabel/miniagda | A research prototype of a dependently typed language with sized types and variances | 104 |
 0xd34df00d/refinedt | A project that formalizes refinement types and dependent types in the Agda language | 58 |
 migamake/json-autotype | Generates Haskell type declarations from JSON input to improve developer productivity when working with big JSON APIs. | 148 |
 nomeata/inspection-testing | A tool that allows developers to embed assertions about intermediate code in their Haskell programs and have them checked by the compiler. | 172 |
 thma/whyhaskellmatters | Explaining why Haskell's unique features make it an important language for software development | 470 |
 theam/haskell-do | A Haskell-based code editor designed for interactive development and programming in the language. | 352 |
 chris-taylor/aima-haskell | An implementation of popular AI algorithms in the Haskell programming language | 331 |
 imdea-software/htt | A verification system for reasoning about sequential heap-manipulating programs using separation logic and dependent types | 70 |
 magmide/magmide | Creating a programming language and ecosystem to make formal verification and provably correct software development practical and mainstream for working software engineers. | 810 |
 codeintegrity-ai/mutahunter | Automated unit test generation and mutation testing tool using Large Language Models. | 252 |
 justusadam/language-haskell | Provides syntax highlighting and indentation support for Haskell language in Visual Studio Code | 97 |
 rudymatela/fitspec | Automates refinement of test properties for Haskell functions by testing mutant variations and providing suggestions for improvement. | 74 |
 haskell-things/implicitcad | A Haskell-based CAD program that supports CSG, bevels, and shells, as well as 2D & 3D geometry and GCode generation. | 1,415 |