DARTS.7.2.3.pdf
- Filesize: 0.61 MB
- 11 pages
Document
mist: Refinements of Futures Past (Artifact)
Authors
-
Part of:
Issue:
Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021)
Volume: DARTS, Volume 7 (ECOOP 2021)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2021-07-06
Artifact Description
Document Identifiers
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
Artifact
DARTS-7-2-3-artifact-aa4c6b98c4c7b17c67c9369ae9e3aff7.tgz
(Filesize: 7.53 GB)
MD5 Sum:
aa4c6b98c4c7b17c67c9369ae9e3aff7
(Get MD5 Sum)
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.
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)
0PDF Downloads