But ACL2 is a far better match for someone on this list.
On Mon, Oct 4, 2010 at 1:49 PM, Hendrik Boom <hend...@topoi.pooq.com> wrote: > On Mon, Oct 04, 2010 at 12:12:02PM -0400, Matthias Felleisen wrote: >> >> Patrick, in principle you're not mistaken to ask for a 'loop checker'. >> Many people work on this topic -- despite the Halting Problem -- to this >> day, mostly in language contexts that are connected to theorem proving >> (or logic programming, which is close). >> >> If you're really interested, start with the ACL2 theorem prover. > > Or coq. Its whole logic combines programming and logic, and is very > much involved with termination. > > -- hendrik. > _________________________________________________ > For list-related administrative tasks: > http://lists.racket-lang.org/listinfo/users > _________________________________________________ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/users
