DROPS

Document

Artifact

mist: Refinements of Futures Past (Artifact)

Authors: Anish Tondwalkar, Matt Kolosick, and Ranjit Jhala

Published in: DARTS, Volume 7, Issue 2, Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021)

Abstract

mist is a tiny language for teaching and experimenting with refinement types, in the style of https://github.com/ucsd-progsys/liquidhaskell. We use it as a platform for experimenting with and as a demonstration of implicit refinement types as presented in the ECOOP21 paper Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types. We start with the parser and AST we use to teach our undergradute compilers class, and layer upon it a refinement type checker directly translated from the typing rules presented in that paper, which produces constraints that are solved with the liquid-fixpoint horn clause solver. We present source code and binaries for mist in a container image that includes installations of the competing tools we compare to.

Cite as

Anish Tondwalkar, Matt Kolosick, and Ranjit Jhala. mist: Refinements of Futures Past (Artifact). In Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021). Dagstuhl Artifacts Series (DARTS), Volume 7, Issue 2, pp. 3:1-3:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Article{tondwalkar_et_al:DARTS.7.2.3,
  author =	{Tondwalkar, Anish and Kolosick, Matt and Jhala, Ranjit},
  title =	{{mist: Refinements of Futures Past (Artifact)}},
  pages =	{3:1--3:11},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2021},
  volume =	{7},
  number =	{2},
  editor =	{Tondwalkar, Anish and Kolosick, Matt and Jhala, Ranjit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.7.2.3},
  URN =		{urn:nbn:de:0030-drops-140275},
  doi =		{10.4230/DARTS.7.2.3},
  annote =	{Keywords: Refinement Types, Implicit Parameters, Verification, Dependent Pairs}
}

Document

DOI: 10.4230/LIPIcs.ECOOP.2021.18

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

Authors: Anish Tondwalkar, Matthew Kolosick, and Ranjit Jhala

Published in: LIPIcs, Volume 194, 35th European Conference on Object-Oriented Programming (ECOOP 2021)

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.

Cite as

Anish Tondwalkar, Matthew Kolosick, and Ranjit Jhala. Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 18:1-18:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.ECOOP.2021.18},
  URN =		{urn:nbn:de:0030-drops-140615},
  doi =		{10.4230/LIPIcs.ECOOP.2021.18},
  annote =	{Keywords: Refinement Types, Implicit Parameters, Verification, Dependent Pairs}
}

Search Results

Documents authored by Tondwalkar, Anish

mist: Refinements of Futures Past (Artifact)

Abstract

Cite as

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

Abstract

Cite as

Thanks for your feedback!

Could not send message