Re: [TYPES] I'm searching for a survey on type system feature combinations

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

On 17/06/15 20:18, Derek Dreyer wrote:
>
> In more recent years, we (and various collaborators) have extended
> these kinds of semantic models to handle features like concurrency and
> substructural typing as well, and we have developed higher-order
> separation logics for abstracting the relevant reasoning principles
> that these models support.  We have not (yet) looked at
> intersection/union types or subtyping.

This is veering off the original topic quite a bit, but Pierre
Pradic, Nick Benton and I looked at integrating intersection
types and and substructural/dependent types in our POPL 2015
paper "Integrating Linear and Dependent Types".

It turns out that intersection function work rather like
a type-theoretic analogue of "logical variables" from Hoare
logic. Paul-Andre Mellies and Noam Zeilberger give a
categorical account of this fact in their POPL 2015 paper
"Functors are Type Refinement Systems".

Best,
Neel

PS -- Slightly farther afield, Alexandre Miquel gave a denotational
model of the implicit calculus of constructions in terms of
coherence spaces and stable functions,  which can be thought of
as a way of presenting state machines and simulation relations
(see Uday Reddy's "Global State Considered Unnecessary"). As a
result it seems plausible to me that there are some deep
connections between intersection types and protocol-based
reasoning about state.