
Agda
 Referenced in 182 articles
[sw09689]
 Agda is a dependently typed functional programming language: It has inductive families, which are similar ... assist in the development of your code). Agda is also a proof assistant ... interactive system for writing and checking proofs. Agda is based on intuitionistic type theory ... package includes both a commandline program (agda) and an Emacs mode. If you want...

UniMath
 Referenced in 15 articles
[sw15140]
 such as the ones used in Coq, Agda or Lean is based on the discovery...

AoPA
 Referenced in 8 articles
[sw09832]
 Algebra of programming in Agda: dependent types for relational program derivation. Relational program derivation ... library, AoPA (Algebra of Programming in Agda), to encode relational derivations in the dependently typed ... programming language Agda. A program is coupled with an algebraic derivation whose correctness is guaranteed...

AgsyHOL
 Referenced in 4 articles
[sw13302]
 AgsyHOL source code and Agda formalization. agsyHol is a theorem prover for higherorder logic ... proof language has been established in Agda, a dependently typed programming language. The theorem prover ... output solutions in Agda format, enabling checking the validity independently and against the formalised soundness ... costly for agsyHOL. Constructed Agda proofs for problems do currently not include this transformation step...

RATHAgda
 Referenced in 3 articles
[sw13303]
 RATHAgda: RelationAlgebraic Theories in Agda. The basic category and allegory theory library ... RATHAgda project, containing (only sporadically truly) literate theories ranging from semigroupoids, which are “categories...

Aglet
 Referenced in 4 articles
[sw13305]
 generalpurpose dependently typed programming language, Agda. Our library, Aglet, accounts for the major features...

RoutingLib
 Referenced in 2 articles
[sw28638]
 Agda formalization of Üresin & Dubois’ asynchronous fixedpoint theory. In this paper we describe ... Agdabased formalization of results from Üresin & Dubois’ “Parallel Asynchronous Algorithms for Discrete Data”. That ... distributed computation, making formal verification worthwhile.{ }Our Agda library provides users with a collection...

Hazelnut
 Referenced in 2 articles
[sw22659]
 metatheory, which we have mechanized using the Agda proof assistant, serves as a guide when...

Coq
 Referenced in 1784 articles
[sw00161]
 Coq is a formal proof management system. It...

Haskell
 Referenced in 844 articles
[sw03521]
 Haskell is a standardized, generalpurpose purely functional...

Scala
 Referenced in 85 articles
[sw07180]
 Steps in Scala. An introduction to objectfunctional...

ALF
 Referenced in 67 articles
[sw08603]
 The Implementation of ALF  a Proof Editor based...

TRX
 Referenced in 9 articles
[sw08800]
 TRX: a formally verified parser interpreter. Parsing is...

LEGO
 Referenced in 107 articles
[sw09685]
 LEGO is an interactive proof development system (proof...

Epigram
 Referenced in 22 articles
[sw09687]
 Epigram: Practical programming with dependent types. Find the...

Coquet
 Referenced in 5 articles
[sw09919]
 Coquet: a Coq library for verifying hardware. We...

PoplMark
 Referenced in 60 articles
[sw10109]
 The POPLmark Challenge is a concrete set of...

AURA
 Referenced in 10 articles
[sw11482]
 AURA, a programming language for authorization and audit...

Ynot
 Referenced in 35 articles
[sw12334]
 Ynot, dependent types for imperative programs. We describe...

Fortress
 Referenced in 16 articles
[sw13026]
 Fortress is a new programming language being designed...