Personal tools

Applications and libraries/Theorem provers

From HaskellWiki

< Applications and libraries(Difference between revisions)
Jump to: navigation, search
m (The description of Epigram mentions the concept of dependent type, so I have made a link to Dependent type)
(Add Cayenne)
Line 1: Line 1:
 
== Theorem provers ==
 
== Theorem provers ==
  +
  +
Tools for formal reasoning, written in Haskell.
   
 
;[http://www.cs.chalmers.se/~catarina/agda/ Agda]
 
;[http://www.cs.chalmers.se/~catarina/agda/ Agda]
Line 14: Line 16:
   
 
;[http://wiki.di.uminho.pt/wiki/bin/view/PURe/Camila Camila]
 
;[http://wiki.di.uminho.pt/wiki/bin/view/PURe/Camila Camila]
:Camila is a system for software development using formal methods. Other materials on formal methods can be found also on [[Analysis and design]] page.
+
:Camila is a system for software development using formal methods. Other materials on formal methods can be found also on the [[Analysis and design|analysis and design]] page.
   
 
;[http://www.e-pig.org/ Epigram]
 
;[http://www.e-pig.org/ Epigram]
 
:Epigram is a prototype [[Dependent type|dependently typed]] functional programming language, equipped with an interactive editing and typechecking environment. High-level Epigram source code elaborates into a dependent type theory based on Zhaohui Luo's UTT. Programming with evidence lies at the heart of Epigram's design.
 
:Epigram is a prototype [[Dependent type|dependently typed]] functional programming language, equipped with an interactive editing and typechecking environment. High-level Epigram source code elaborates into a dependent type theory based on Zhaohui Luo's UTT. Programming with evidence lies at the heart of Epigram's design.
  +
  +
;[http://www.cs.chalmers.se/~augustss/cayenne/index.html Cayenne]
  +
:Cayenne is a functional language with a powerful [[Dependent type|dependent type system]]. The basic types are functions, products, and sums. Functions and products use dependent types to gain additional power. As with Epigram, a dependently typed language may be used to encode strong proofs in the type system.
   
 
;[http://www.haskell.org/yarrow/ Yarrow]
 
;[http://www.haskell.org/yarrow/ Yarrow]

Revision as of 02:18, 1 April 2006

Theorem provers

Tools for formal reasoning, written in Haskell.

Agda
Agda is a system for incrementally developing proofs and programs. Agda is also a functional language with Dependent types. This language is very similar to cayenne and agda is intended to be a (almost) full implementation of it in the future.
Djinn
Djinn generates Haskell code from a type declaration, using a decision procedure from intuitionistic propositional calculus.
Paradox
Paradox processes first-order logic problems and tries to find finite-domain models for them.
Dumatel
Dumatel is a prover based on many-sorted term rewriting (TRW) and equational reasoning
Camila
Camila is a system for software development using formal methods. Other materials on formal methods can be found also on the analysis and design page.
Epigram
Epigram is a prototype dependently typed functional programming language, equipped with an interactive editing and typechecking environment. High-level Epigram source code elaborates into a dependent type theory based on Zhaohui Luo's UTT. Programming with evidence lies at the heart of Epigram's design.
Cayenne
Cayenne is a functional language with a powerful dependent type system. The basic types are functions, products, and sums. Functions and products use dependent types to gain additional power. As with Epigram, a dependently typed language may be used to encode strong proofs in the type system.
Yarrow
Yarrow is a proof-assistant for Pure Type Systems (PTSs) with several extensions. In Yarrow you can experiment with various pure type systems, representing different logics and programming languages.
Proof General Kit
The Proof General Kit designs and implements a component-based framework for interactive theorem proving. The central middleware of the toolkit is implemented in Haskell. The project is the sucessor of the highly successful Emacs-based Proof General interface.
Expander2
Expander2 is a flexible multi-purpose workbench for rewriting, verification, constraint solving, flow graph analysis and related procedures that build up proofs or computation sequences. Moreover, tailor-made interpreters display terms as 2D structures ranging from trees and rooted graphs to tables, fractals and other turtle-system-generated pictures.