HNGlance

Top Best New Show

Tom compiler: Transformations of programs for C{,++,#}, Java, Python, Ocaml

http://tom.loria.fr/

by khandekars • 17 years ago

17 2 17 years ago

TO

Related Stories

Loading related stories...

Comments

2

ed• 17 years ago

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

http://www.loria.fr/~moreau/Papiers/MoreauRV-CC2003.pdf

khandekars• 17 years ago

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.

Links:

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

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

http://en.wikipedia.org/wiki/Coq#Four_color_theorem_and_ssre...

Source preview

tom.loria.fr

HNGlance

© 2024-2026 HN Glance. Story content belongs to its original sources.

Privacy
Terms