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

Rewrite related work.

parent 7f0d3a38
......@@ -232,3 +232,65 @@ Finally, I took advantage of this opportunity to describe some undocumented adva
address = {New York, NY, USA},
keywords = {Racket, Refinement types, occurrence typing},
}
@article{Bierman10,
author = {Bierman, Gavin M. and Gordon, Andrew D. and Hriundefinedcu, Cundefinedtundefinedlin and Langworthy, David},
title = {Semantic Subtyping with an SMT Solver},
year = {2010},
issue_date = {September 2010},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {45},
number = {9},
issn = {0362-1340},
url = {https://doi.org/10.1145/1932681.1863560},
doi = {10.1145/1932681.1863560},
journal = {SIGPLAN Not.},
month = sep,
pages = {105–116},
numpages = {12},
keywords = {type systems, semantic subtyping, data processing, satisfiability modulo theories}
}
@inproceedings{Chugh12,
author = {Chugh, Ravi and Rondon, Patrick M. and Jhala, Ranjit},
title = {Nested Refinements: A Logic for Duck Typing},
year = {2012},
isbn = {9781450310833},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/2103656.2103686},
doi = {10.1145/2103656.2103686},
booktitle = {Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
pages = {231–244},
numpages = {14},
keywords = {dynamic languages, refinement types},
location = {Philadelphia, PA, USA},
series = {POPL ’12}
}
@inproceedings{Bonn16,
author = {Ambrose Bonnaire{-}Sergeant and
Rowan Davies and
Sam Tobin{-}Hochstadt},
editor = {Peter Thiemann},
title = {Practical Optional Types for Clojure},
booktitle = {Programming Languages and Systems - 25th European Symposium on Programming,
{ESOP} 2016, Held as Part of the European Joint Conferences on Theory
and Practice of Software, {ETAPS} 2016, Eindhoven, The Netherlands,
April 2-8, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9632},
pages = {68--94},
publisher = {Springer},
year = {2016},
url = {https://doi.org/10.1007/978-3-662-49498-1\_4},
doi = {10.1007/978-3-662-49498-1\_4},
timestamp = {Tue, 14 May 2019 10:00:41 +0200},
biburl = {https://dblp.org/rec/conf/esop/Bonnaire-Sergeant16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
\ No newline at end of file
......@@ -9,7 +9,38 @@ defined predicates.
State what we capture already, for instance lists since we have product and recursive types.
}
\kim{Need to clean-up and insert at the right place.
}
The work of \cite{Bierman10}, presents Dminor, a data oriented
language featuring a {\tt SELECT}-like constructs over
collections. Its typesystems combines semantic subtyping and
refinement types. Syntactic types are mapped to first order formula
and subtyping is expressed as logicial implication. An SMT-solver is
then used to (try to) prove the logicial implication. The refinement
types they present go well beyond what can be expressed with the set-theoretic
types we use (as they allow almost any pure expression to occur in
types). However, the system foregoes any notion of completeness
(since satisfiability of first order logic is undecidable) and the
subtyping algorithm is largely dependent on the subtle behaviour of
the SMT solver (which may timeout our give an incorrect model that
cannot be used as a counter-example to explain the type-error).
As with our work, the typing rule for the {\tt if~$e$ then $e_1$ else
$e_2$} construct
of Dminor refines the type of each branch by remembering that $e$
(resp. $\lnot e$) is true in $e_1$ (resp. $e_2$) but this information
is not propagated to the outer context.
A similar approach is taken in \cite{Chugh12}, and extended to so
called nested refinement types. In these types, an arrow type may
appear in a logical formula (where previous work only allowed formulae
between ``base types''). This is done in the context of a dynamic
language and their approach is extended with polymorphism, dynamic
dispatch and record types. As in \cite{Bierman10}, the refined typed
of a conditional does not flow to the outer context and the same
provision to using an SMT solver apply.
\kim{\cite{Bonn16} is typed racket with closure\ldots}.
Occurrence typing was introduced by \citet{THF08} and further advanced
in \cite{THF10} in the context of the Typed Racket language. This
......
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