KnowledgeBase » 
SEMINAR
» ID = 467
Presenting Semantics for a Fragment of the Java Programming Language in Nuprl Proof Development System
by Pavel Naumov
1997-1998
In this my third talk at Nuprl Seminar on Java Formal Semantics I will give an introduction to my work that does not require knowledge of Nuprl. The two main results of this work are: a formal semantics for a Java language developed in Nuprl; and a new mathematical Theory of Reference Objects on which this semantics is based.
In my talk I will describe the fragment of the Java for which I gave formal semantics, discuss the kind of semantics I was looking for, explain intuition behind the Theory of Reference Objects, present some of its inference rules, and sketch a consistency proof for this theory. I also will mention application of the formal semantics to verification of small Java programs and the method for publishing Nuprl formal proofs on the Web that I have developed.