Sep 28, 2015
Davide Ancona: Type soundness proofs with big-step operational semantics of object-oriented languages
Proofs of soundness of type systems are typically based on small-step operational semantics, because of the inability of big-step operational semantics to distinguish stuck from non-terminating computations.
In this talk I will present two techniques to prove type soundness with big-step semantics.
The former is based on the notion of coinductive big-step semantics, obtained by interpreting the semantics rules coinductively, and by considering non-well-founded values. The corresponding proof of soundness is rather involved, since it requires showing that the set of proof trees defining the semantic judgment forms a complete metric space when equipped with a specific distance function.
A simpler approach consists in approximating at arbitrary depth the possibly infinite derivations of the coinductive semantics with infinite sequences of finite derivations; in this way, type soundness can be proved by standard mathematical induction.
Finally, I will briefly discuss interesting research directions to overcome some of the limitations of the presented techniques.