Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Giuseppe Castagna
occurrence-typing
Commits
da876c60
Commit
da876c60
authored
Sep 27, 2021
by
Kim Nguyễn
Browse files
Add related work on intersection + refinement types.
parent
fce00ac6
Changes
2
Hide whitespace changes
Inline
Side-by-side
main.bib
View file @
da876c60
...
...
@@ -557,3 +557,33 @@ series = {LFP '92}
}
@article
{
PAF15
,
title
=
{Liquid Intersection Types}
,
volume
=
{177}
,
ISSN
=
{2075-2180}
,
url
=
{http://dx.doi.org/10.4204/EPTCS.177.3}
,
DOI
=
{10.4204/eptcs.177.3}
,
journal
=
{Electronic Proceedings in Theoretical Computer Science}
,
publisher
=
{Open Publishing Association}
,
author
=
{Pereira, Mário and Alves, Sandra and Florido, Mário}
,
year
=
{2015}
,
month
=
{Mar}
,
pages
=
{24–42}
}
@article
{
BHM14
,
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
=
{https://doi.org/10.3233/JCS-130493}
,
doi
=
{10.3233/JCS-130493}
,
timestamp
=
{Mon, 11 May 2020 22:59:05 +0200}
,
biburl
=
{https://dblp.org/rec/journals/jcs/BackesHM14.bib}
,
bibsource
=
{dblp computer science bibliography, https://dblp.org}
}
\ No newline at end of file
related.tex
View file @
da876c60
...
...
@@ -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
\rev
{
TODO Intersection + refinement
}
\rev
{
TODO refinement + gradual ?
}
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment