[Prev][Next][Index][Thread]
Re: Subject reduction fails in Java
Dear Benjamin, Sophia, Donald, ...
Benjamin Pierce wrote:
> One may wonder how this failure of subject reduction squares with
> recent proofs of type soundness for fragments of Java by Drossopolou
> and Eisenbach [2] and Nipkow and XXXXXXXXXXXXXX [3]. On the one hand,
> since these fragments omit the conditional expression form, this
> failure does not affect the validity of their results, per se. On the
> other hand, both of these papers use a reduction-based operational
> semantics, and therefore, it seems, their proof methods cannot easily
> be extended to deal with the full Java language including conditional
> expressions.
We did not handle conditional expressions by now because we considered
them as trivial. As we do _not_ use a reduction-based operational
semantics, but an evaluation semantics, they are indeed absolutely
harmless in our setting, see below.
Sophia Drossopoulou wrote:
> Therefore, as well as thinking about improving the language
> definition, it is interesting to try to formalize the situation as is
> and prove soundness.
>
> I see the following alternatives:
>
> 1) Use large step semantics -- I believe that the von Oheimb/Nipkow
> proof could be extended to describe conditional expressions without
> any problems.
I've just done this -- as expected, within our formalization it is a
15-minutes exercise. This approach is characterized simply by the
straightforward typing rule given by Sophia:
> b : bool e1:E1 e2:E2
> (E1 < E2 and E2=T) or (E2 < E1 and E1=T)
> --------------------------------------------
> (b?e1:e2) : T
After adding this typing rule together with the obvious evaluation rule
to our formalization in Isabelle, and after adding a call of a standard
automatic proof tactic, the type soundness proof re-ran perfectly,
confirming that type soundness is not violated.
This easy - yet reliable - maintainability is one of the main benefits
of computer-assisted proofs.
Donald Syme wrote:
> That is, ultimately we would like to be able to formulate
> arguments for the type correctness of "real" implementations of
> languages, or at least close approximations to them. These do not
> carry around much type information, and so further annotating
> our runtime apparatus with types is, from my perspective, "cheating".
At least using an evaluation semantics, it's not necessary to
distinguish the original language and the run-time language (and any
complications involved in this) to handle problematic cases such as the
typing of conditionals and array assignments. Even more, one doesn't
have to worry about such potential pitfalls.
Regards,
David
PS: Our Java formalization (not a fully up-to-date version right now)
may be found in http://www.in.tum.de/~isabelle/bali/
THAT's _\\/, For a more realistic picture, my address and other stuff
NOT me: (@ @) see http://www.in.tum.de/~oheimb/ <><
...---oOO-(_)-OOo-------------------------------------------------------