3 Search Results for "Tondwalkar, Anish"

Document
DOI: 10.4230/LIPIcs.ECOOP.2024.39
Formalizing, Mechanizing, and Verifying Class-Based Refinement Types

Authors: Ke Sun, Di Wang, Sheng Chen, Meng Wang, and Dan Hao

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Refinement types have been extensively used in class-based languages to specify and verify fine-grained logical specifications. Despite the advances in practical aspects such as applicability and usability, two fundamental issues persist. First, the soundness of existing class-based refinement type systems is inadequately explored, casting doubts on their reliability. Second, the expressiveness of existing systems is limited, restricting the depiction of semantic properties related to object-oriented constructs. This work tackles these issues through a systematic framework. We formalize a declarative class-based refinement type calculus (named RFJ), that is expressive and concise. We rigorously develop the soundness meta-theory of this calculus, followed by its mechanization in Coq. Finally, to ensure the calculus’s verifiability, we propose an algorithmic verification approach based on a fragment of first-order logic (named LFJ), and implement this approach as a type checker.
Cite as

Ke Sun, Di Wang, Sheng Chen, Meng Wang, and Dan Hao. Formalizing, Mechanizing, and Verifying Class-Based Refinement Types. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 39:1-39:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{sun_et_al:LIPIcs.ECOOP.2024.39,
  author =	{Sun, Ke and Wang, Di and Chen, Sheng and Wang, Meng and Hao, Dan},
  title =	{{Formalizing, Mechanizing, and Verifying Class-Based Refinement Types}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{39:1--39:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.39},
  URN =		{urn:nbn:de:0030-drops-208881},
  doi =		{10.4230/LIPIcs.ECOOP.2024.39},
  annote =	{Keywords: Refinement Types, Program Verification, Object-oriented Programming}
}
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}
}
Document
Artifact
DOI: 10.4230/DARTS.7.2.3
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}
}
  • Refine by Author
  • 2 Jhala, Ranjit
  • 2 Tondwalkar, Anish
  • 1 Chen, Sheng
  • 1 Hao, Dan
  • 1 Kolosick, Matt
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Program constructs
  • 2 Theory of computation → Program specifications
  • 2 Theory of computation → Program verification
  • 1 Software and its engineering → Formal software verification
  • 1 Theory of computation → Type structures

  • Refine by Keyword
  • 3 Refinement Types
  • 2 Dependent Pairs
  • 2 Implicit Parameters
  • 2 Verification
  • 1 Object-oriented Programming
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 2 2021
  • 1 2024

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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact