swMATH9689MaRDI QIDQ21668FDOQ21668
Author name not available (Why is that?)
Official website: https://wiki.portal.chalmers.se/agda/pmwiki.php
Source code repository: https://github.com/agda/agda
Cited In (only showing first 100 items - show all)
- Herbrand constructivization for automated intuitionistic theorem proving
- A web-based toolkit for mathematical word processing applications with semantics
- A synthesis of the procedural and declarative styles of interactive theorem proving
- Ivor, a Proof Engine
- Theorema
- Beluga
- MetaPRL
- CIRC
- Matita
- Ivor
- HOL Light
- HOL-Omega
- Nuprl
- Automath
- Twelf
- Lurch
- AURA
- ALF
- AutPGrp
- Lilac
- Polyp
- Alfalfa
- Coq/SSReflect
- MetaOCaml
- Camlflow
- Abella
- TRX
- iTasks
- Cayenne
- Epigram
- CalcCheck
- Flask
- AoPA
- Irdis
- Mella
- Minlog
- Coquet
- Galculator
- Milawa
- PhoX
- Gmeta
- PoplMark
- Paco
- Nominal Isabelle
- FoCaLiZe
- Ynot
- Mtac
- Traffic 4
- Aglet
- RATH-Agda
- RepLib
- BNFConverter
- dedukti
- DrIFT
- wxHaskell
- lens
- VeriML
- Yampa
- HoTT
- MathScheme
- Lean
- seL4
- UniMath
- CoALP
- Nepal
- HOL Zero
- Security-typed programming within dependently typed programming
- FreshML
- HOL Light QE
- Leo-III
- CoqMTU
- CoqMT
- Idris
- Lincx
- LLFp
- AmiCo
- Literate CoffeeScript
- Markdown
- MathQuill
- HOL2P
- CLF
- Delphin
- MiniAgda
- TAG
- gradualizerDynamicSemantics
- webLurch
- Hume
- Teyjus
- Calcite
- CoCaml
- TypeScript
- Hazelnut
- Lamdu
- mbeddr
- TouchDevelop
- An Agda formalization of Üresin \& Dubois' asynchronous fixed-point theory
- Hammer for Coq: automation for dependent type theory
- A new implementation of Automath
- The Lean theorem prover (system description)
- Friends with benefits. Implementing corecursion in foundational proof assistants
This page was built for software: Agda
