Document Open Access Logo

mist: Refinements of Futures Past (Artifact)

Authors Anish Tondwalkar, Matt Kolosick, Ranjit Jhala

PDF

Artifact Description

Thumbnail PDF
PDF
DARTS.7.2.3.pdf
  • Filesize: 0.61 MB
  • 11 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Program constructs
  • Theory of computation → Program specifications
  • Theory of computation → Program verification
Keywords
  • Refinement Types
  • Implicit Parameters
  • Verification
  • Dependent Pairs

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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 Get BibTex

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) https://doi.org/10.4230/DARTS.7.2.3

Author Details

Anish Tondwalkar
  • University of California, San Diego, CA, USA
Matt Kolosick
  • University of California, San Diego, CA, USA
Ranjit Jhala
  • University of California, San Diego, CA, USA

Funding

This work was supported by NSF grant CCF-1911213.

Artifact

  MD5 Sum: aa4c6b98c4c7b17c67c9369ae9e3aff7 (Get MD5 Sum)

Related Article

  • 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), LIPIcs, Vol. 194, pp. 18:1-18:29, 2021. https://doi.org/10.4230/LIPIcs.ECOOP.2021.18
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact