3 Search Results for "Tondwalkar, Anish"

Document
Extended Abstract
DOI: 10.4230/OASIcs.Programming.2025.4
Debugging a Smalltalk VM Assisted by Large Automated Reasoning (Extended Abstract)

Authors: Boris Shingarov and Jan Vraný

Published in: OASIcs, Volume 134, Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025)

Abstract
We show how a full-scale automated-reasoning engine implemented in Smalltalk can be applied to assist in the programmer’s cognitive task of traversing abstraction levels. This approach follows naturally from our definition of debugging as any activity aimed towards understanding a program. We introduce the notion of "dimensions of abstraction", give two examples ("stratum" and "mode"), and show how it is applied in debugging a native compiler backend.
Cite as

Boris Shingarov and Jan Vraný. Debugging a Smalltalk VM Assisted by Large Automated Reasoning (Extended Abstract). In Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025). Open Access Series in Informatics (OASIcs), Volume 134, pp. 4:1-4:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{shingarov_et_al:OASIcs.Programming.2025.4,
  author =	{Shingarov, Boris and Vran\'{y}, Jan},
  title =	{{Debugging a Smalltalk VM Assisted by Large Automated Reasoning}},
  booktitle =	{Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming (Programming 2025)},
  pages =	{4:1--4:6},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-382-9},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{134},
  editor =	{Edwards, Jonathan and Perera, Roly and Petricek, Tomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Programming.2025.4},
  URN =		{urn:nbn:de:0030-drops-242881},
  doi =		{10.4230/OASIcs.Programming.2025.4},
  annote =	{Keywords: Smalltalk, Virtual Machine, Automated Reasoning, Debugging, ISA Specification}
}
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 Type
  • 3 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 2 2021

  • Refine by Author
  • 2 Jhala, Ranjit
  • 2 Tondwalkar, Anish
  • 1 Kolosick, Matt
  • 1 Kolosick, Matthew
  • 1 Shingarov, Boris
  • Show More...

  • Refine by Series/Journal
  • 1 LIPIcs
  • 1 OASIcs
  • 1 DARTS

  • 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 → Runtime environments
  • 1 Software and its engineering → Semantics
  • Show More...

  • Refine by Keyword
  • 2 Dependent Pairs
  • 2 Implicit Parameters
  • 2 Refinement Types
  • 2 Verification
  • 1 Automated Reasoning
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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