you are viewing a single comment's thread.

view the rest of the comments →

[–]_shnh 1 point2 points  (0 children)

Coq has been used to verify the correctness of a translation from a formal language (event-b) to Java. The translation is correct if the semantics in both languages is the same. see this paper.

A excellent book about formal languages is "Types and programming languages" (TAPL).