Commit da876c60 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Add related work on intersection + refinement types.

parent fce00ac6
......@@ -557,3 +557,33 @@ series = {LFP '92}
title={Liquid Intersection Types},
journal={Electronic Proceedings in Theoretical Computer Science},
publisher={Open Publishing Association},
author={Pereira, Mário and Alves, Sandra and Florido, Mário},
author = {Backes, Michael and Hri\c{t}cu, C\u{a}t\u{a}lin and Maffei, Matteo},
title = {Union, intersection and refinement types and reasoning about type
disjointness for secure protocol implementations},
journal = {J. Comput. Secur.},
volume = {22},
number = {2},
pages = {301--353},
year = {2014},
url = {},
doi = {10.3233/JCS-130493},
timestamp = {Mon, 11 May 2020 22:59:05 +0200},
biburl = {},
bibsource = {dblp computer science bibliography,}
\ No newline at end of file
......@@ -282,9 +282,42 @@ precision, one would need to identify $\alpha$-equivalent sub-expressions
so that they share the same binding, something that a plain A-normalization
does not provide (and which, actually, must not provide, since in that
case the transformation may not preserve the reduction semantics).
Amongst the work on refinement types, some have studied the extensions
of a refinement type-system with intersection types. For
instance, \cite{BHM14} studies a type system with refinement types,
polymorphism and full union and intersection (but no negation). While
the goal of their type-system is to verify secure protocol
implementations, the core language RCF$^{\forall}_{\land\lor}$ they
present, as well as the associated type-system is a lambda calculus
with pattern-matching, let bindings, and a refining test for equality
(as well as protocol oritented constructs such as channel creation,
message passing and expression forking). While on the surface their
types ressemble ours, they follow another direction. First, their
language is fully annotated (meaning that e.g. polymorphic terms must
be intantiated explicitely and intersection type must also be given
through an annotation). Second, since the subtyping relation they
provide is syntactic, it cannot in general take into account the
distributivity of logical connectives w.r.t type constructors. This
limitation is hovever not a problem since the main goal of their
subtyping relation is to propagate a \emph{kinding} information that
they use to characterize the level of knowledge an attacker may have
about a particular value.
Another work adding intersection types to refinement types
is \cite{PAF15} in the context of liquid types. This work introduces
intersection (but not union nor negations) to liquid types, with a
particular focus on intersection of arrow types. This work uses a
syntactic subtyping relation to push down intersection of types into
the logical formulas of types. Once the formulas have been propagated,
they are offloaded to an SMT solver to decide the base case of the
subtyping relation. Of particular interest is their type-inference
algorithm. Contrary to ours, their inference is based on algorithm
$\mathcal{W}$, using the polymorphic type deduced as a template for an
intersection. They can therefore infer intersection arrow types that
are several distinct instances of the same polymorphic type.
\rev{TODO Intersection + refinement}
\rev{TODO refinement + gradual ?}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment