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

Added related work on refinement types.

parent 1a82d3f4
......@@ -400,4 +400,102 @@ abstract = "The notion of parallel reduction is extracted from the Tait-Martin-L
year = {1984},
volume = {103},
edition = {Revised},
\ No newline at end of file
author = {Knowles, Kenneth and Flanagan, Cormac},
title = {Compositional Reasoning and Decidable Checking for Dependent Contract Types},
year = {2009},
isbn = {9781605583303},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {},
doi = {10.1145/1481848.1481853},
abstract = {Simple type systems perform compositional reasoning in that the type of a term depends
only on the types of its subterms, and not on their semantics. Contracts offer more
expressive abstractions, but static contract checking systems typically violate those
abstractions and base their reasoning directly upon the semantics of terms. Pragmatically,
this noncompositionality makes the decidability of static checking unpredictable.We
first show how compositional reasoning may be restored using standard type-theoretic
techniques, namely existential types and subtyping. Despite its compositional nature,
our type system is exact, in that the type of a term can completely capture its semantics,
hence demonstrating that precision and compositionality are compatible. We then address
predictability of static checking for contract types by giving a type-checking algorithm
for an important class of programs with contract predicates drawn from a decidable
theory. Our algorithm relies crucially on the fact that the type of a term depends
only the types of its subterms (which fall into the decidable theory) and not their
semantics (which will not, in general).},
booktitle = {Proceedings of the 3rd Workshop on Programming Languages Meets Program Verification},
pages = {27–38},
numpages = {12},
keywords = {compositional reasoning, abstraction, dependent types, refinement types},
location = {Savannah, GA, USA},
series = {PLPV '09}
author="Ou, Xinming
and Tan, Gang
and Mandelbaum, Yitzhak
and Walker, David",
editor="Levy, Jean-Jacques
and Mayr, Ernst W.
and Mitchell, John C.",
title="Dynamic Typing with Dependent Types",
booktitle="Exploring New Frontiers of Theoretical Informatics",
publisher="Springer US",
address="Boston, MA",
abstract="Dependent type systems are promising tools programmers can use to increase the reliability and security of their programs. Unfortunately, dependently-typed programming languages require programmers to annotate their programs with many typing specifications to help guide the type checker. This paper shows how to make the process of programming with dependent types more palatable by defining a language in which programmers have fine-grained control over the trade-off between the number of dependent typing annotations they must place on programs and the degree of compile-time safety. More specifically, certain program fragments are marked dependent, in which case the programmer annotates them in detail and a dependent type checker verifies them at compile time. Other fragments are marked simple, in which case they may be annotation-free and dependent constraints are verified at run time.",
author = {Patrick Maxim Rondon and
Ming Kawaguchi and
Ranjit Jhala},
editor = {Rajiv Gupta and
Saman P. Amarasinghe},
title = {Liquid types},
booktitle = {Proceedings of the {ACM} {SIGPLAN} 2008 Conference on Programming
Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008},
pages = {159--169},
publisher = {{ACM}},
year = {2008},
url = {},
doi = {10.1145/1375581.1375602},
timestamp = {Fri, 25 Jun 2021 14:48:54 +0200},
biburl = {},
bibsource = {dblp computer science bibliography,}
author = {Sabry, Amr and Felleisen, Matthias},
title = {Reasoning about Programs in Continuation-Passing Style.},
year = {1992},
isbn = {0897914813},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {},
doi = {10.1145/141471.141563},
abstract = {Plotkin's λ-value calculus is sound but incomplete for reasoning about βeegr;-transformations
on programs in continuation-passing style (CPS). To find a complete extension, we
define a new, compactifying CPS transformation and an “inverse”mapping, un-CPS, both
of which are interesting in their own right. Using the new CPS transformation, we
can determine the precise language of CPS terms closed under β7eegr;-transformations.
Using the un-CPS transformation, we can derive a set of axioms such that every equation
between source programs is provable if and only if βη can prove the corresponding
equation between CPS programs. The extended calculus is equivalent to an untyped
variant of Moggi's computational λ-calculus.},
booktitle = {Proceedings of the 1992 ACM Conference on LISP and Functional Programming},
pages = {288–298},
numpages = {11},
location = {San Francisco, California, USA},
series = {LFP '92}
......@@ -243,6 +243,29 @@ appear in a logical formula (where previous work only allowed formulae
on ``base types''). This is done in the context of a dynamic
language and their approach is extended with polymorphism, dynamic
dispatch and record types.
\rev{A problem that is faced by refinement type systems is the one of
propagating in the branches of a test the information learned on
a \emph{sub-expression} of a tested expression. A solution
e.g. choosen by \cite{OTMW04} and \cite{KF09} is to devise a
meta-function that recursively explores both a type and an expression
and propagates the type information on the sub-expressions. This
process (called \emph{selfification} in the cited works) roughly
corresponds to our $\constrf$ function (see Section~\ref{sec:typenv}).
Another approach is the one followed by \cite{RKJ08} is based purely
on a program transformation, namely putting the the term
in \emph{administrative normal form} (\cite{\F92}). Using a program
transformation, every destructor application (function application,
projection, \ldots) is given a name through a let-binding. The problem
of tracking precise type information for every sub-expression is
therefore reduced to the one of keeping precise typing information for
a variable. While this solution seems appealing, it is not as
straightforward in our case. Indeed, to retain the same degree of
precision, we would need to identify alpha equivalent sub-expressions
and share the same binding, something that a plain A-normalisation
does not provide.
\rev{TODO Intersection + refinement}
\rev{TODO refinement + gradual ?}
\citet{Kent16} bridge the gap between prior work on occurrence typing
and SMT based (sub) typing. It introduces the $\lambda_{RTR}$ core calculus, an
......@@ -611,7 +611,10 @@ the new contributions.
{[}5{]} studies the integration of liquid with gradual types while
preserving the gradual guarantees.
We have further developped the our section of the related work on
refinment types, using the given references has a starting point.
\item \textbf{Meta-theory Clarifications:}
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