The talk concentrated on 3 sets of papers all dealing with semantics for modern Object-Oriented (OO) languages, concentrating on Java.
The first group of papers from Drossopoulou, Eisenbanch and Khurshid concentrate on proving Java's type system sound. The question was raised "Why do we need to prove, a type system, sound? What's the point?". After a discussion the conclusion was:
Environments are provided with the following definition:
Env ::= stdEnv | Env; Decl
where stdEnv includes what comes with the standard Java Library. Environments are used to store information about class definitions, field definitions, type, arguments and their types, method types etc. In order to make type information readily available a language two languages are defined.
Where Javas is the Kernel language and Javas is annotated (through a rewrite step →) extra type information e.g., class where the field is defined, class where a method is defined. A variable can hold an instance of a class or a subtype of that class.
Question: What is the meaning of "type", because you refer to
it both at compile and runtime?
Answer: Type is compile time, at runtime this becomes a tag
The rules provided are the typical ones, but there is an addition
for widening between types one of the rules states that I
can substitute an object of type τ with one of type τ' is
the latter is a subtype of the former (τ ⊆ τ'):
|Γ |- τ ⊆ τ'|
|Γ |- τ ≤wdn τ'|
In a well-formed environment of Javase subclassing defines a partial order for classes (⊆) and interfaces (≤). The widening rule is partial order. The widening rule extends to deal with method overrides, this is based according to the return type of the method i.e.
Javase has a richer set of type rules (e.g., memory addresses), first fit (the first class for the hierarchy tree that fits), object creation, assignment etc. Operational semantics for Javase is defined as a ternary relationship, mapping configurations and programs to configurations. A configuration is a tuple of Javase terms and states or just state.
Config ::= 〈 Javase term, state 〉 ∪ state
Where state is a mapping from identifiers to primitive values or references.
Subject reduction and soundness theorems state that a well-typed program in this subset of Java evaluates to a ground term of the type that can be widened to the type of the original program, or it raises an exception and the state remains consistent with the environment.
The second group of paper consists of a paper by Igarashi, Pierce and Wadler, describing a core subset of Java (Featherweight Java) to which they provide semantics and an extension to handle generics in Java. Unlike the previous group of papers the goal is to define a small core of the language with which most of the language features can be studied. The model defines mutually recursive class definitions, subtypes, casting etc. The goal, well-typed programs do note get stuck.
Question: What to you mean not stuck?
Answer: A program returns a value or an exception.
There are 3 ways to get stuck
(Object) (new Pair(..))
(Pair) (new Pair(new Pair(1,2),3)).first()
(Person) (new List(..))and List is not a subclass of Person
if Γ |- e ∈ c and e → e' then Γ |- e' ∈ c' for some c' <: c
The progress theorem states that if a well-typed program has a field access or a method invocation then this field or method is well-defined. This leads to the soundness theorem which states that an expression e of the type c in an environment Γ evaluates to e' with e' being in normal form then ' is either a value or it contains an expression with a stupid cast inside it.
The last group of paper by Flatt, Krishnamurthi and Felleisen (Classic Java) define again a core for the Java language. In one of their papers the core language is used to add mixins to Java. The system is very much similar to Featherweight Java with the addition of assignment. The paper defines elaboration rules that translate expression into annotated expressions that include needed type information. Semantics are given as a contextual rewrite system on pairs of expressions and stores.
Matthias summarized the work by the three groups as: