Re: [isabelle] Program verification and Isabelle?

You may be interested in the Sunrise project.  Although not targeting Java
or C#, only a small imperative language similar to a subset of Pascal, it is
a genuine system for proving partial or total correctness of individual
programs written in the Sunrise language, using the Higher Order Logic
theorem prover.

Rather than by translation, which could be considered a "shallow embedding,"
it is based on a "deep embedding" of Sunrise within HOL.  Deep embeddings
are much more difficult to create, but once built, have significant
advantages over shallow embeddings.

Please see


On 9/29/06, Klaus Ostermann <ostermann at> wrote:

I have seen many examples of proving properties of programming languages
as type soundness) in Isabelle.

I wonder whether it is also possible to prove properties of individual
written in some language, say Java or C#. It would of course be tiresome
manually "translate" the program into Isabelle, but in principle it should
possible to "compile" a Java program into an Isabelle specification, e.g.,
partially evaluating a Java semantics written in Isabelle with an input

Has something like this been tried (maybe with another theorem prover)? If
could you give me a reference? If no, are there specific reasons why it
has not
been tried?


"In Your majesty ride prosperously because of truth, humility, and
And Your right hand shall teach You awesome things." (Psalm 45:4)

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.