Anonymous user
User:Realazthat/Projects wishlist/LLVM/Formal methods: Difference between revisions
User:Realazthat/Projects wishlist/LLVM/Formal methods (view source)
Revision as of 14:43, 13 October 2010
, 13 years ago→Other interesting languages
(Created page with '==Formal methods project== Write an LLVM pass that will prove certain properties of functions. ==Features== Things that the pass might prove, for each function: * That all '''as…') |
|||
Line 81:
* [http://wiki.portal.chalmers.se/agda/pmwiki.php Agda]
*: Requires termination proofs, effectively making it decidable (I think)
** Also a theorem proover (can be a language and its proof according to the [[wp:Curry–Howard_correspondence#Related_proofs-as-programs_correspondences
| |||