Hacker News new | past | comments | ask | show | jobs | submit login
Tom compiler: Transformations of programs for C{,++,#}, Java, Python, Ocaml (loria.fr)
17 points by khandekars on June 6, 2009 | hide | past | web | favorite | 2 comments

For a nice high-level introduction to the Tom compiler, I'd suggest reading section 4.2 of the following paper:


Thanks, it's good.

In examples/README, it mentions of exmaples/zenon -- certification of Tom's output using zenon and Coq. Apparently, the "zvtov" tool required for that is part of FoCaLize. Given that Coq was used to create a surveyable proof of 4-color problem, it sounds impressive.


FoCaLize -- http://focalize.inria.fr/

Coq -- http://coq.inria.fr/


Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact