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/
Tondwalkar, Anish ;
Kolosick, Matthew ;
Jhala, Ranjit
Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types
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}
}
