License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2021.18
URN: urn:nbn:de:0030-drops-140615
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14061/
Go to the corresponding LIPIcs Volume Portal


Tondwalkar, Anish ; Kolosick, Matthew ; Jhala, Ranjit

Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types

pdf-format:
LIPIcs-ECOOP-2021-18.pdf (1 MB)


Abstract

Refinement types decorate types with assertions that enable automatic verification. Like assertions, refinements are limited to binders that are in scope, and hence, cannot express higher-order specifications. Ghost variables circumvent this limitation but are prohibitively tedious to use as the programmer must divine and explicate their values at all call-sites. We introduce Implicit Refinement Types which turn ghost variables into implicit pair and function types, in a way that lets the refinement typechecker automatically synthesize their values at compile time. Implicit Refinement Types further take advantage of refinement type information, allowing them to be used as a lightweight verification tool, rather than merely as a technique to automate programming tasks. We evaluate the utility of Implicit Refinement Types by showing how they enable the modular specification and automatic verification of various higher-order examples including stateful protocols, access control, and resource usage.

BibTeX - Entry

@InProceedings{tondwalkar_et_al:LIPIcs.ECOOP.2021.18,
  author =	{Tondwalkar, Anish and Kolosick, Matthew and Jhala, Ranjit},
  title =	{{Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types}},
  booktitle =	{35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages =	{18:1--18:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-190-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{194},
  editor =	{M{\o}ller, Anders and Sridharan, Manu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14061},
  URN =		{urn:nbn:de:0030-drops-140615},
  doi =		{10.4230/LIPIcs.ECOOP.2021.18},
  annote =	{Keywords: Refinement Types, Implicit Parameters, Verification, Dependent Pairs}
}

Keywords: Refinement Types, Implicit Parameters, Verification, Dependent Pairs
Collection: 35th European Conference on Object-Oriented Programming (ECOOP 2021)
Issue Date: 2021
Date of publication: 06.07.2021
Supplementary Material: Software (ECOOP 2021 Artifact Evaluation approved artifact): https://doi.org/10.4230/DARTS.7.2.3 archived at: https://archive.softwareheritage.org/swh:1:snp:aeaf3dbb58f5be84b565e73b5ade1503ee8cb6d6


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI