[PRL] [1510.05216] From F to DOT: Type Soundness Proofs with Definitional Interpreters

[Matthias Felleisen]

On Oct 20, 2015, at 9:18 AM, Amal Ahmed <amal at ccs.neu.edu> wrote:

> 
> 
> 
> Sent from my iPhone
> On Oct 20, 2015, at 8:20 AM, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
> 
>> 
>> With respect, a more-or-less similar argument has been put forth by Xavier for years. The type soundness proof for FP based on denotational interpretations or Tofte’s operational semantics (which can easily be viewed as an interpreter) have stood the test of time.
> 
> Agreed (except I wasn't aware that Xavier has pushed this argument).

Xavier shared this with me in a couple of conversations so I may have misunderstood. But he was very excited to have to tell me that he needed an alternative proof method :-) 


> 
>> It’s just that scaling those to anything non-functional is hard (not impossible, just incredibly error prone).
> 
> If I understand you right, my dissertation contains exactly such a result: a type soundness proof for System F plus ML-like mutable references that relies on denotational 
> interpretations of types based on the operational semantics of the language. So, yes, it's hard, but it's been a solved problem for a decade. 


The prior work section in WF spells out how others tackled type soundness with imperative languages. It is so error prone that people were pretty frustrated for 20 years because only super-experts could prove this kind of thing. I am pretty sure sub-typing soundness predates you too by a decade though not necessarily your particular formulation (just think FeatherFooBar, which wasn't real progress only progress for OO). 

I am sure WF could be adjusted to cope but hukairs. 







> 
> -Amal
> 
>> Since Scala is post-functional, they dont need soundness for effects :-) 
>> 
>> 
>> 
>> 
>> 
>>> On Oct 20, 2015, at 7:16 AM, Mitchell Wand <wand at ccs.neu.edu> wrote:
>>> 
>>> Your morning link: Not read, but sounds neat....
>>> 
>>> From F to DOT: Type Soundness Proofs with Definitional Interpreters
>>> 
>>> Tiark Rompf, Nada Amin
>>> (Submitted on 18 Oct 2015)
>>> Scala's type system unifies aspects of ML-style module systems, object-oriented, and functional programming paradigms. The DOT (Dependent Object Types) family of calculi has been proposed as a new theoretic foundation for Scala and similar expressive languages. Unfortunately, type soundness has only been established for a very restricted subset of DOT (muDOT), and it has been shown that adding important Scala features such as type refinement or extending subtyping to a lattice breaks at least one key metatheoretic property such as narrowing or subtyping transitivity, which are usually required for a type soundness proof. 
>>> The first main contribution of this paper is to demonstrate how, perhaps surprisingly, even though these properties are lost in their full generality, a richer DOT calculus that includes both type refinement and a subtyping lattice with intersection types can still be proved sound. The key insight is that narrowing and subtyping transitivity only need to hold for runtime objects, but not for code that is never executed. Alas, the dominant method of proving type soundness, Wright and Felleisen's syntactic approach, is based on term rewriting, which does not make an adequate distinction between runtime and type assignment time. 
>>> The second main contribution of this paper is to demonstrate how type soundness proofs for advanced, polymorphic, type systems can be carried out with an operational semantics based on high-level, definitional interpreters, implemented in Coq. We present the first mechanized soundness proof for System F<: based on a definitional interpreter. We discuss the challenges that arise in this setting, in particular due to abstract types, and we illustrate in detail how DOT-like calculi emerge from straightforward generalizations of the operational aspects of F<:.
>>> http://arxiv.org/abs/1510.05216
>>> _______________________________________________
>>> PRL mailing list
>>> PRL at lists.ccs.neu.edu
>>> https://lists.ccs.neu.edu/bin/listinfo/prl
>> 
>> _______________________________________________
>> PRL mailing list
>> PRL at lists.ccs.neu.edu
>> https://lists.ccs.neu.edu/bin/listinfo/prl