User:Realazthat/Projects wishlist/LLVM/Formal methods: Difference between revisions
Content added Content deleted
(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: | Line 81: | ||
* [http://wiki.portal.chalmers.se/agda/pmwiki.php Agda] |
* [http://wiki.portal.chalmers.se/agda/pmwiki.php Agda] |
||
*: Requires termination proofs, effectively making it decidable (I think) |
*: 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 |
** Also a theorem proover (can be a language and its proof according to the [[wp:Curry–Howard_correspondence#Related_proofs-as-programs_correspondences| Curry–Howard correspondence]] |