Applications and libraries/Theorem provers
Jump to navigation
Jump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
Theorem provers
- 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 generates Haskell code * from a type declaration, using a decision procedure from intuitionistic propositional calculus.