• 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 command-line 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 higher-order 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...
  • RATH-Agda

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

  • Referenced in 4 articles [sw13305]
  • general-purpose 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 fixed-point theory. In this paper we describe ... Agda-based 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, general-purpose purely functional...
  • Scala

  • Referenced in 85 articles [sw07180]
  • Steps in Scala. An introduction to object-functional...
  • 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...
  • 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...