pith. machine review for the scientific record. sign in

arxiv: 2605.13456 · v1 · submitted 2026-05-13 · 💻 cs.PL

Recognition: unknown

Liquid Tree Automata

Ashish Mishra , Suresh Jagannathan
Authors on Pith no claims yet

Pith reviewed 2026-05-14 18:26 UTC · model grok-4.3

classification 💻 cs.PL
keywords component-based synthesisrefinement typestree automataprogram synthesissubtypingliquid typesstate merging
0
0 comments X

The pith

Liquid Tree Automata merge semantically similar states using subtyping from refinement types to speed up component-based synthesis.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces Liquid Tree Automata to address the sparse search spaces that arise when component-based synthesis uses precise logical specifications. Construction of the automata follows refinement typing rules, and subtyping constraints are applied to identify and collapse states that represent logically equivalent paths. The resulting reduction in redundant exploration allows the Hegel implementation to solve synthesis queries that defeat existing tools.

Core claim

Liquid Tree Automata are constructed according to refinement typing rules for library components and use subtyping constraints to eagerly merge states that label semantically equivalent exploration paths, thereby pruning the search without losing valid solutions.

What carries the argument

Liquid Tree Automata, a tree-automata variant whose state merging is driven directly by subtyping judgments on refinement types.

If this is right

  • The effective size of the search space shrinks as more paths are recognized as identical.
  • Synthesis remains sound because only provably equivalent states are merged.
  • Precise specifications become practical rather than prohibitive for component libraries.
  • The same merging discipline can be applied to any synthesis procedure that already reasons with refinement types.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The state-merging idea could be adapted to other automata constructions that operate over logical specifications.
  • Approximate or dynamic variants of the subtyping check might trade a small amount of precision for further scalability gains.
  • The technique suggests a general pattern for using type-based equivalences to compress search spaces in program synthesis.

Load-bearing premise

Subtyping constraints derived from refinement types accurately capture semantic equivalence of exploration paths without missing valid solutions or incorrectly merging distinct paths.

What would settle it

A synthesis query on which the LTA-based procedure either returns an incorrect program because two non-equivalent paths were merged or fails to find a known solution that a non-merging search would locate.

Figures

Figures reproduced from arXiv: 2605.13456 by Ashish Mishra, Suresh Jagannathan.

Figure 1
Figure 1. Figure 1: Motivating Synthesis Problem overall search space, making synthesis significantly more challenging. Intuitively, we can define CBS search as a reachability analysis over a graph that relates candidate methods based on their type or other similar defining attributes. For example, a node in this graph associated with a method that has a particular result type can be connected to any node corresponding to a m… view at source ↗
Figure 2
Figure 2. Figure 2: An Ex￾ample LTA A natural approach to handling such refined queries is to syn￾thesize programs using only the unrefined base types of the query and library components [10, 14, 21] , and to subsequently apply a verification check to discard candidates that violate refinement constraints. Although simple, this strategy is un￾likely to be effective at scale; not only is the solution space now very sparse, thu… view at source ↗
Figure 3
Figure 3. Figure 3: A simple LTA for binding (x : { ν : int | 10 ≥ ν ≥ 0 }) To address these limitations, we introduce a new data struc￾ture, Liquid Tree Automata (LTA), that allows us to capture such logical constraints. An LTA supports a richer alphabet than other FTA variants by incorporating logical qualifiers from decidable first-order theory fragments. While it also al￾lows constraints on its transitions similar to othe… view at source ↗
Figure 4
Figure 4. Figure 4: An LTA fragment embedding a refinement typing semantics for function application. Additionally, a typing semantics of￾ten establishes logical entailment con￾straints between formulas under a substitution. A good example is the inferred type for an app term and the function’s return type. LTAs model this using the constraints ○c , that equates base types, and ○d , that captures the logical entailment (fun.o… view at source ↗
Figure 5
Figure 5. Figure 5: LTA Constraints The target language of our synthesizer (λlta) is a stan￾dard A-normalized [13] call-by-value refinement-typed λ-calculus [31] with constructors, constants and vari￾ables, conditional expressions, and function abstrac￾tion and application. To simplify the presentation, we assume all variables have a single unique binding-site. λlta types include standard base types like int, bool etc., along… view at source ↗
Figure 6
Figure 6. Figure 6: LTA denotations. Formally, we define the language accepted by A using its denotation JAK (see [PITH_FULL_IMAGE:figures/full_fig_p007_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Selected rules for constructing transitions [PITH_FULL_IMAGE:figures/full_fig_p010_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Application of Well￾formedness and Transition rules to construct initial LTA A0 and A1 for the example library. Rules E-var(construction shown in [PITH_FULL_IMAGE:figures/full_fig_p012_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Selective rules for similarity inference and LTA Minimization. [PITH_FULL_IMAGE:figures/full_fig_p014_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Cycles in LTA for polymorphic types and abstract refinements. States in cycles are colored. The state qt captures all valid base-refinement types, where a poly￾morphic list constructor List can be instantiated with any possible type (the cyclic edge back to qt). The re￾finement formula in τ in turn can be instantiated with all valid refinement predicates captured by another state qϕ, with standard predica… view at source ↗
Figure 11
Figure 11. Figure 11: Synthesis Results for selected RQ1 Benchmarks where at least one of the [PITH_FULL_IMAGE:figures/full_fig_p018_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: A comparison for representation of space of terms using VSA, FTA, [PITH_FULL_IMAGE:figures/full_fig_p024_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Extended λLTA Expressions and Types with parametric polymorphism and abstract refinement variables [PITH_FULL_IMAGE:figures/full_fig_p025_13.png] view at source ↗
Figure 14
Figure 14. Figure 14: Extended Typing Semantics for λLTA Expressions [PITH_FULL_IMAGE:figures/full_fig_p026_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: Extended Typing Semantics for well-formedness and subtyping of [PITH_FULL_IMAGE:figures/full_fig_p027_15.png] view at source ↗
Figure 16
Figure 16. Figure 16: Rules for constructing transitions ∆, basis for WF and Transition. with rules E-α, E-κ and E-infer [PITH_FULL_IMAGE:figures/full_fig_p029_16.png] view at source ↗
Figure 17
Figure 17. Figure 17: Complete set of Similarity inference and LTA Minimization. [PITH_FULL_IMAGE:figures/full_fig_p031_17.png] view at source ↗
Figure 18
Figure 18. Figure 18: A LTA for the example library. The green arrow relates similar sets of [PITH_FULL_IMAGE:figures/full_fig_p032_18.png] view at source ↗
Figure 19
Figure 19. Figure 19: An Example LTA, portions shaded out for elucidation. Variable Scoping and Typing En￾vironment in LTA The details of variable scoping during LTA construc￾tion and pruning are important to un￾derstand how enumeration works with refinement types in a LTA. To sim￾plify scoping decisions and manage the typing environment, we made sev￾eral design choices. First, we require terms in our synthesis language λltato… view at source ↗
Figure 20
Figure 20. Figure 20: Inductively defined Relation R, capturing the relation between A and the Typing Environment Γ. A little abuse of notation for presentation, denotation for a type node (and edge) Jqτ K is a singleton set, and we use it to also denote the element in the set in Rules RQ-Var, RQ-Const and R∆-GEN [PITH_FULL_IMAGE:figures/full_fig_p034_20.png] view at source ↗
Figure 21
Figure 21. Figure 21: Results for experiments with Refined Hoogle+ and ECTA benchmarks. [PITH_FULL_IMAGE:figures/full_fig_p046_21.png] view at source ↗
Figure 22
Figure 22. Figure 22: Results for tailored specification-guided synthesis benchmarks, The #C [PITH_FULL_IMAGE:figures/full_fig_p047_22.png] view at source ↗
Figure 23
Figure 23. Figure 23: Synthesized Program for NLR_Remove [PITH_FULL_IMAGE:figures/full_fig_p048_23.png] view at source ↗
Figure 24
Figure 24. Figure 24: Comparison of Hegel and its variants Hegel, Hegel(-S), Hegel(-P), Hegel(- ALL), on average synthesis times and the number of candidate terms generated on RQ1 and RQ2. The labels on each bar show the number of benchmarks solved by these variants out of 42 in the case of RQ1 and 9 in the case of RQ2. The first two charts in [PITH_FULL_IMAGE:figures/full_fig_p049_24.png] view at source ↗
read the original abstract

Component-based synthesis (CBS) generates loop-free programs from library components to satisfy logical queries. While expressive specifications and precise queries simplify the solution space, they make finding feasible execution paths significantly more difficult for traditional CBS procedures. As constraints become more exact, the search must navigate an increasingly sparse space of valid paths. We address this challenge by reasoning about \emph{logical similarities} between exploration paths. We consider library methods equipped with refinement-type specifications, which enrich base types with logical qualifiers to precisely constrain the value space. To efficiently explore this space, we introduce Liquid Tree Automata (LTA), a novel tree automata variant whose construction is driven by refinement typing rules. LTAs leverage subtyping constraints to identify and eagerly merge semantically similar states during search. This merging avoids redundant exploration of equivalent paths, significantly improving synthesis efficiency. We implement this approach in a tool called Hegel. Our evaluation demonstrates that Hegel synthesizes solutions to complex queries that are beyond the reach of existing state-of-the-art tools.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 1 minor

Summary. The manuscript introduces Liquid Tree Automata (LTAs), a tree-automaton variant for component-based synthesis of loop-free programs from library components equipped with refinement-type specifications. LTAs are constructed using refinement typing rules and leverage subtyping constraints to identify and eagerly merge semantically similar states during search, with the goal of avoiding redundant exploration of equivalent paths and thereby improving synthesis efficiency. The approach is implemented in the Hegel tool, whose evaluation is claimed to synthesize solutions to complex queries beyond the reach of existing state-of-the-art tools.

Significance. If the soundness of the subtyping-driven merge operation holds, the work could meaningfully advance component-based synthesis by supporting more precise refinement-type specifications without incurring prohibitive search costs. The direct use of existing refinement typing rules for automata construction is a positive aspect that may facilitate integration with type-based synthesis frameworks.

major comments (1)
  1. [§3] §3: The LTA construction uses subtyping judgments on refinement types to decide state equivalence and perform eager merging during tree-automaton search. No lemma is supplied establishing that the subtyping relation is a congruence with respect to the synthesis semantics (i.e., that whenever two states are related by subtyping they remain semantically interchangeable in every context of component composition). Without such a result, it is unclear whether merging preserves the set of accepted programs; an over-approximation could silently drop valid solutions or introduce spurious ones, which directly undermines the central efficiency-without-loss claim.
minor comments (1)
  1. [Abstract] Abstract: The claim of 'significantly improving synthesis efficiency' is stated without any quantitative summary of runtime or success-rate improvements; a single sentence reporting key experimental deltas would strengthen the abstract.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading and for highlighting the need for an explicit congruence result. We agree that the soundness of the eager merge operation requires a formal guarantee that subtyping preserves semantic interchangeability under component composition. We will add the requested lemma in the revised manuscript.

read point-by-point responses

  1. Referee: [§3] §3: The LTA construction uses subtyping judgments on refinement types to decide state equivalence and perform eager merging during tree-automaton search. No lemma is supplied establishing that the subtyping relation is a congruence with respect to the synthesis semantics (i.e., that whenever two states are related by subtyping they remain semantically interchangeable in every context of component composition). Without such a result, it is unclear whether merging preserves the set of accepted programs; an over-approximation could silently drop valid solutions or introduce spurious ones, which directly undermines the central efficiency-without-loss claim.

    Authors: We agree that an explicit lemma is required. In the revised version we will insert a new lemma (placed after the definition of LTA construction in §3) proving that the subtyping relation is a congruence with respect to the synthesis semantics: if two states q1 and q2 satisfy q1 <: q2 then, for any context of component composition, the sets of programs accepted from q1 and from q2 coincide. The proof proceeds by induction on the structure of the component composition tree, using the fact that the refinement typing rules already enforce semantic inclusion and that subtyping is transitive and compatible with the tree-automaton transition relation. This establishes that the eager merge operation neither drops valid solutions nor introduces spurious ones, thereby preserving the completeness claim while still delivering the reported efficiency gains. revision: yes

Circularity Check

0 steps flagged

No significant circularity; LTA construction directly applies existing refinement typing rules

full rationale

The paper introduces Liquid Tree Automata as a novel variant whose construction is driven by standard refinement typing rules and subtyping constraints from the literature. No equations, fitted parameters, or self-referential definitions appear; state merging is presented as a direct application of existing subtyping judgments rather than a result that reduces to the paper's own inputs by construction. No load-bearing self-citations, uniqueness theorems imported from the authors, or ansatzes smuggled via prior work are invoked in the provided text. The central efficiency claim rests on the semantics of refinement types, which are treated as external and independent.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claim rests on the domain assumption that refinement typing rules can be used to construct automata that correctly detect semantic similarity via subtyping; no free parameters or invented physical entities are mentioned.

axioms (1)
  • domain assumption Refinement typing rules soundly identify logical similarities between program paths.
    The LTA construction is explicitly driven by refinement typing rules and subtyping constraints.
invented entities (1)
  • Liquid Tree Automata no independent evidence
    purpose: Tree automata variant that merges semantically similar states during synthesis search
    Newly introduced construct whose states are defined by refinement typing rules.

pith-pipeline@v0.9.0 · 5458 in / 1206 out tokens · 39554 ms · 2026-05-14T18:26:33.226018+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

38 extracted references

  1. [1]

    Recursive Program Syn- thesis

    Aws Albarghouthi, Sumit Gulwani, and Zachary Kincaid. Recursive Program Syn- thesis. In Natasha Sharygina and Helmut Veith, editors,Computer Aided Verifi- cation, pages 934–950, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Liquid Tree Automata 21

    2013

  2. [2]

    Olausson, Lionel Wong, Gabriel Grand, Joshua B

    Matthew Bowers, Theo X. Olausson, Lionel Wong, Gabriel Grand, Joshua B. Tenenbaum, Kevin Ellis, and Armando Solar-Lezama. Top-Down Synthesis for Library Learning. Proc. ACM Program. Lang., 7(POPL), jan 2023

    2023

  3. [3]

    Babble: Learning Better Abstractions with E-Graphs and Anti- Unification

    David Cao, Rose Kunkel, Chandrakana Nandi, Max Willsey, Zachary Tatlock, and Nadia Polikarpova. Babble: Learning Better Abstractions with E-Graphs and Anti- Unification. Proc. ACM Program. Lang., 7(POPL), jan 2023

    2023

  4. [4]

    VOCAL – A Verified OCaml Library

    Arthur Charguéraud, Jean-Christophe Filliâtre, Mário Pereira, and François Pot- tier. VOCAL – A Verified OCaml Library. ML Family Workshop, September 2017

    2017

  5. [5]

    Tree Automata Techniques and Applications

    Hubert Comon. Tree Automata Techniques and Applications. 1997

    1997

  6. [6]

    Extended symbolic finite automata and trans- ducers

    Loris D’antoni and Margus Veanes. Extended symbolic finite automata and trans- ducers. Form. Methods Syst. Des., 47(1):93–119, August 2015

    2015

  7. [7]

    AutomataforReduction Properties Solving

    MaxDauchet,Anne-CécileCaron,andJean-LucCoquidé. AutomataforReduction Properties Solving. Journal of Symbolic Computation, 20(2):215–233, 1995

    1995

  8. [8]

    Program Synthesis Using Conflict-Driven Learning

    Yu Feng, Ruben Martins, Osbert Bastani, and Isil Dillig. Program Synthesis Using Conflict-Driven Learning. InProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, page 420–435, New York, NY, USA, 2018. Association for Computing Machinery

    2018

  9. [9]

    Component-Based Synthesis of Table Consolidation and Transformation Tasks from Examples

    Yu Feng, Ruben Martins, Jacob Van Geffen, Isil Dillig, and Swarat Chaudhuri. Component-Based Synthesis of Table Consolidation and Transformation Tasks from Examples. In Proceedings of the 38th ACM SIGPLAN Conference on Pro- gramming Language Design and Implementation, PLDI 2017, page 422–436, New York, NY, USA, 2017. Association for Computing Machinery

    2017

  10. [10]

    Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, and Thomas W. Reps. Component-Based Synthesis for Complex APIs. InProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, page 599–612, New York, NY, USA, 2017. Association for Computing Machinery

    2017

  11. [11]

    Inductive Program Synthesis Guided by Observational Program Similarity.Proc

    Jack Feser, Işıl Dillig, and Armando Solar-Lezama. Inductive Program Synthesis Guided by Observational Program Similarity.Proc. ACM Program. Lang., 7(OOP- SLA2), oct 2023

    2023

  12. [12]

    Synthesizing Functional Reactive Programs

    Bernd Finkbeiner, Felix Klein, Ruzica Piskac, and Mark Santolucito. Synthesizing Functional Reactive Programs. InProceedings of the 12th ACM SIGPLAN Inter- national Symposium on Haskell, Haskell 2019, page 162–175, New York, NY, USA,

    2019

  13. [14]

    TheEssence of Compiling with Continuations

    CormacFlanagan,AmrSabry,BruceF.Duba,andMatthiasFelleisen. TheEssence of Compiling with Continuations. In Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation, PLDI ’93, page 237–247, New York, NY, USA, 1993. Association for Computing Machinery

    1993

  14. [15]

    Program Synthesis by Type-Guided Abstraction Refine- ment

    Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, and Nadia Polikarpova. Program Synthesis by Type-Guided Abstraction Refine- ment. Proc. ACM Program. Lang., 4(POPL), December 2019

    2019

  15. [16]

    Foster, and David Van Horn

    Sankha Narayan Guria, Jeffrey S. Foster, and David Van Horn. RbSyn: Type- and Effect-Guided Program Synthesis. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021, page 344–358, New York, NY, USA, 2021. Association for Computing Machinery

    2021

  16. [17]

    On the Automated Verification of Web Applications with Embedded SQL

    Shachar Itzhaky, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith, and Florian Zuleger. On the Automated Verification of Web Applications with Embedded SQL. In Michael Benedikt and Giorgio Orsi, editors,20th Inter- national Conference on Database Theory, ICDT 2017, March 21-24, 2017, Venice, 22 A. Mishra and S. Jagannathan Italy, volume 68...

    2017

  17. [18]

    James, Zheng Guo, Ziteng Wang, Shivani Doshi, Hila Peleg, Ranjit Jhala, and Nadia Polikarpova

    Michael B. James, Zheng Guo, Ziteng Wang, Shivani Doshi, Hila Peleg, Ranjit Jhala, and Nadia Polikarpova. Digging for Fold: Synthesis-Aided API Discovery for Haskell.Proc. ACM Program. Lang., 4(OOPSLA), nov 2020

    2020

  18. [19]

    Seshia, and Ashish Tiwari

    Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, and Ashish Tiwari. Oracle-Guided Component-Based Program Synthesis. In Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 1, ICSE ’10, page 215–224, New York, NY, USA, 2010. Association for Computing Machinery

    2010

  19. [20]

    Refinement Types: A Tutorial

    Ranjit Jhala and Niki Vazou. Refinement Types: A Tutorial. Found. Trends Program. Lang., 6(3-4):159–317, 2021

    2021

  20. [21]

    A relational framework for higher-order shape analysis

    Gowtham Kaki and Suresh Jagannathan. A relational framework for higher-order shape analysis. InProceedings of the 19th ACM SIGPLAN International Confer- ence on Functional Programming, ICFP ’14, pages 311–324, New York, NY, USA,

  21. [22]

    Association for Computing Machinery

  22. [23]

    Searching Entangled Program Spaces.Proc

    James Koppel, Zheng Guo, Edsko de Vries, Armando Solar-Lezama, and Nadia Polikarpova. Searching Entangled Program Spaces.Proc. ACM Program. Lang., 6(ICFP), aug 2022

    2022

  23. [24]

    Lau, Pedro Domingos, and Daniel S

    Tessa A. Lau, Pedro Domingos, and Daniel S. Weld. Version Space Algebra and Its Application to Programming by Demonstration. InProceedings of the Seven- teenth International Conference on Machine Learning, ICML ’00, page 527–534, San Francisco, CA, USA, 2000. Morgan Kaufmann Publishers Inc

    2000

  24. [25]

    Bottom-up Synthesis of Recursive Functional Programs Using Angelic Exe- cution

    Anders Miltner, Adrian Trejo Nuñez, Ana Brendel, Swarat Chaudhuri, and Işıl Dilig. Bottom-up Synthesis of Recursive Functional Programs Using Angelic Exe- cution. Proc. ACM Program. Lang., 6(POPL), jan 2022

    2022

  25. [26]

    Relational Syn- thesis of Recursive Programs via Constraint Annotated Tree Automata

    Anders Miltner, Ziteng Wang, Swarat Chaudhuri, and Isil Dillig. Relational Syn- thesis of Recursive Programs via Constraint Annotated Tree Automata. InCom- puter Aided Verification: 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24–27, 2024, Proceedings, Part III, page 41–63, Berlin, Heidelberg,

    2024

  26. [27]

    Specification-Guided Component-Based Synthesis from Effectful Libraries.Proc

    Ashish Mishra and Suresh Jagannathan. Specification-Guided Component-Based Synthesis from Effectful Libraries.Proc. ACM Program. Lang., 6(OOPSLA2), oct 2022

    2022

  27. [28]

    Springer Berlin Heidelberg, Berlin, Heidelberg, 1999

    Flemming Nielson, Hanne Riis Nielson, and Chris Hankin.Abstract Interpretation, pages 211–282. Springer Berlin Heidelberg, Berlin, Heidelberg, 1999

    1999

  28. [29]

    Program Synthesis from Polymorphic Refinement Types

    Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. Program Synthesis from Polymorphic Refinement Types. InProceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’16, page 522–538, New York, NY, USA, 2016. Association for Computing Machinery

    2016

  29. [30]

    FrAngel: Component-Based Syn- thesis with Control Structures.Proc

    Kensen Shi, Jacob Steinhardt, and Percy Liang. FrAngel: Component-Based Syn- thesis with Control Structures.Proc. ACM Program. Lang., 3(POPL), jan 2019

    2019

  30. [31]

    Program Synthesis with Equivalence Reduc- tion

    Calvin Smith and Aws Albarghouthi. Program Synthesis with Equivalence Reduc- tion. In Constantin Enea and Ruzica Piskac, editors,Verification, Model Checking, and Abstract Interpretation, pages 24–47, Cham, 2019. Springer International Pub- lishing

    2019

  31. [32]

    Verifying Higher-Order Programs with the Dijkstra Monad

    Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen, and Benjamin Livshits. Verifying Higher-Order Programs with the Dijkstra Monad. InProceed- ings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, page 387–398, New York, NY, USA, 2013. Associ- ation for Computing Machinery. Liquid Tree Automata 23

    2013

  32. [33]

    Bounded refinement types

    Niki Vazou, Alexander Bakst, and Ranjit Jhala. Bounded refinement types. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, pages 48–61, New York, NY, USA, 2015. Association for Computing Machinery

    2015

  33. [34]

    Rondon, and Ranjit Jhala

    Niki Vazou, Patrick M. Rondon, and Ranjit Jhala. Abstract Refinement Types. In Matthias Felleisen and Philippa Gardner, editors,Programming Languages and Systems, pages 209–228, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg

    2013

  34. [35]

    Visu- alization by Example.Proc

    Chenglong Wang, Yu Feng, Rastislav Bodik, Alvin Cheung, and Isil Dillig. Visu- alization by Example.Proc. ACM Program. Lang., 4(POPL), dec 2019

    2019

  35. [36]

    Program Synthesis using Abstraction Refinement

    Xinyu Wang, Isil Dillig, and Rishabh Singh. Program Synthesis using Abstraction Refinement. Proc. ACM Program. Lang., 2(POPL), dec 2017

    2017

  36. [37]

    Synthesis of Data Completion Scripts Using Finite Tree Automata.Proc

    Xinyu Wang, Işıl Dillig, and Rishabh Singh. Synthesis of Data Completion Scripts Using Finite Tree Automata.Proc. ACM Program. Lang., 1(OOPSLA), oct 2017

    2017

  37. [38]

    Egg: Fast and Extensible Equality Saturation.Proc

    Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tat- lock, and Pavel Panchekha. Egg: Fast and Extensible Equality Saturation.Proc. ACM Program. Lang., 5(POPL), jan 2021

    2021

  38. [39]

    query":

    Yihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, and Max Willsey. Better Together: Unifying Datalog and Equality Saturation.Proc. ACM Program. Lang., 7(PLDI), jun 2023. 10 Appendix/Supplemental Material for the Main Paper 24 A. Mishra and S. Jagannathan Fig.12: A comparison for representation of space o...

    2023