pith. machine review for the scientific record. sign in

arxiv: 2605.08369 · v1 · submitted 2026-05-08 · 💻 cs.PL

Recognition: 2 theorem links

· Lean Theorem

First-Class Refinement Types for Scala

Matt Bovel , Viktor Kun\v{c}ak , Martin Odersky
Authors on Pith no claims yet

Pith reviewed 2026-05-12 01:04 UTC · model grok-4.3

classification 💻 cs.PL
keywords refinement typesScala 3type soundnessdependent typessubtypingtype inferencepattern matchingunion and intersection types
0
0 comments X

The pith

Refinement types in Scala 3 function as ordinary types that participate directly in subtyping, inference, and pattern matching.

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

The paper designs refinement types for Scala 3 so that logical predicates become regular types rather than separate annotations. These types interact with the rest of the language through subtyping rules, type inference, and pattern matching. The authors prove type soundness for a core calculus that combines refinement types with dependent function types, bounded polymorphism, recursive types, and union and intersection types. Soundness is established under a partial-correctness semantics defined by a fuel-bounded interpreter and semantic typing. A prototype compiler extension shows the design working in practice with a solver that decides when one predicate entails another.

Core claim

Refinement types are ordinary types in Scala 3 that participate in subtyping, inference, and pattern matching alongside existing language features, with type soundness proven for a core calculus combining dependent function types, bounded polymorphism, positive equi-recursive types, union and intersection types, and refinement types under a partial-correctness semantics using a fuel-bounded definitional interpreter and semantic typing.

What carries the argument

The core calculus that treats refinement types as first-class alongside dependent functions, recursive types, and unions and intersections, with entailment decided by a lightweight solver.

If this is right

  • Programmers can write and use logical predicates on types without maintaining a separate specification language or mental model.
  • Type inference, subtyping, and pattern matching automatically respect the logical predicates attached to refinements.
  • The combination with dependent functions, polymorphism, and recursive types remains sound under the partial-correctness semantics.
  • A prototype implementation demonstrates that the approach can be added to the Scala 3 compiler.

Where Pith is reading between the lines

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

  • This integration could reduce the effort needed to verify simple invariants such as array bounds or data structure properties during ordinary compilation.
  • The first-class status opens the door to using refinements inside type-level computations or higher-order functions without special syntax.
  • Similar first-class treatment might be attempted in other languages that already support dependent types or unions.

Load-bearing premise

The solver correctly decides predicate entailment for the predicates that arise in real Scala programs, and the fuel-bounded partial-correctness semantics matches the observable behavior of the full language.

What would settle it

A concrete Scala program accepted by the prototype type checker but that violates one of its declared refinement predicates at runtime would falsify the soundness claim.

Figures

Figures reproduced from arXiv: 2605.08369 by Martin Odersky, Matt Bovel, Viktor Kun\v{c}ak.

Figure 1
Figure 1. Figure 1: Instantiation of a bounded type parameter with a refinement type. [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Overload resolution with refinement types. [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Length-indexed vectors using refinement types. [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: A collect function in Scala (left) and its encoding in the core calculus (right). The tail-recursive loop becomes a loop combinator whose body returns inl(state′ ) to continue or inr(result) to break. Lists are equi-recursive: inl(unit) represents the empty list and inr( (hd, tl)) a cons cell. if ("a2e7-e89b".matches(idRegex)) "a2e7-e89b".asInstanceOf[ID] else throw new IllegalArgumentException() As with o… view at source ↗
Figure 5
Figure 5. Figure 5: Abstract syntax of the core calculus. Types and terms are mutually inductive; bindings use de Bruijn [PITH_FULL_IMAGE:figures/full_fig_p008_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Successful evaluation rules (𝜌 ⊢ 𝑎 ⇓ 𝑣), derived from the definitional interpreter ( [PITH_FULL_IMAGE:figures/full_fig_p010_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Fuel-bounded definitional interpreter, following Amin and Rompf [ [PITH_FULL_IMAGE:figures/full_fig_p011_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Semantic framework. The value interpretation [PITH_FULL_IMAGE:figures/full_fig_p013_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Typing rules. All rules are proven sound with respect to the semantic typing judgment. [PITH_FULL_IMAGE:figures/full_fig_p015_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Subtyping rules. All rules are proven sound with respect to the semantic subtyping judgment. [PITH_FULL_IMAGE:figures/full_fig_p016_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Strict positivity. spos(𝑋, 𝐴) holds when 𝑋 appears only in strictly positive positions in 𝐴: never to the left of a function arrow, and never in the bounds of a universal type. Union types require 𝑋 to be entirely absent (needed for the distributing lemma). for the shift that increments every free index in 𝐴 by one, 𝐴[𝑖↦→𝑗] for the substitution of index 𝑗 for index 𝑖, and 𝑣, 𝜌 for the environment 𝜌 extend… view at source ↗
Figure 12
Figure 12. Figure 12: Compilation time benchmarks (ms/op, single-shot). Each platform shows unchecked (baseline) and [PITH_FULL_IMAGE:figures/full_fig_p021_12.png] view at source ↗
read the original abstract

Refinement types -- types qualified with logical predicates -- have proven effective for lightweight verification in languages like Liquid Haskell, F*, and Dafny. However, in these systems refinements are either written in a separate specification language or treated as second-class annotations, disconnected from the host language's type system. This disconnect creates usability barriers: programmers must maintain two mental models, and refinements cannot interact with features like type inference, subtyping, or overloading. We present the design of first-class refinement types for Scala 3, where refinements are ordinary types that participate in subtyping, inference, and pattern matching alongside existing language features. We prove type soundness of a core calculus mechanized in Rocq, combining dependent function types, bounded polymorphism, positive equi-recursive types, union and intersection types, and refinement types under a partial-correctness semantics using a fuel-bounded definitional interpreter and semantic typing. Finally, we implement our design as a prototype extension of the Scala 3 compiler with a lightweight e-graph-based solver for predicate entailment.

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 / 2 minor

Summary. The paper presents a design for first-class refinement types in Scala 3, treating refinements as ordinary types that integrate with subtyping, type inference, and pattern matching. It defines a core calculus combining dependent function types, bounded polymorphism, positive equi-recursive types, union and intersection types, and refinement types. Type soundness is established via a mechanized proof in Rocq under a partial-correctness semantics, using a fuel-bounded definitional interpreter and semantic typing. A prototype implementation extends the Scala 3 compiler, employing a lightweight e-graph-based solver for predicate entailment.

Significance. If the core result holds, this advances refinement type systems by eliminating the separation between specification and host language features, enabling more seamless use in a mainstream language. The mechanized Rocq proof for a rich core calculus (including recursive types, intersections, and dependent features) under semantic typing is a notable strength, providing independent verification against an external semantics. The prototype offers evidence of practicality, though the unverified solver limits the strength of implementation claims.

major comments (1)
  1. [Implementation and prototype solver] The mechanized soundness proof (core calculus section) treats predicate entailment as an assumed decision procedure. The prototype implementation relies on an unverified e-graph solver without a separate correctness argument or validation against the predicate fragment generated by the full feature set (dependent predicates, recursive refinements, intersections). This creates a gap between the proven core and the implemented checker, as an unsound solver could accept invalid entailments.
minor comments (2)
  1. [Semantics] Clarify in the semantics section how the fuel bound in the definitional interpreter relates to observable termination behavior in the full Scala language and its extensions.
  2. [Abstract and Introduction] The abstract and introduction could more explicitly state that soundness is claimed only for the core calculus, not the prototype implementation.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful and constructive review. The observation about the gap between the assumed decision procedure in the mechanized proof and the unverified solver in the prototype is valid, and we will revise the manuscript to make this relationship explicit.

read point-by-point responses

  1. Referee: [Implementation and prototype solver] The mechanized soundness proof (core calculus section) treats predicate entailment as an assumed decision procedure. The prototype implementation relies on an unverified e-graph solver without a separate correctness argument or validation against the predicate fragment generated by the full feature set (dependent predicates, recursive refinements, intersections). This creates a gap between the proven core and the implemented checker, as an unsound solver could accept invalid entailments.

    Authors: We agree that the Rocq proof treats predicate entailment as an assumed sound decision procedure, which is a standard modularization in mechanized type soundness proofs to isolate the core type system rules. The prototype's e-graph solver is a practical, lightweight implementation for handling entailment queries that arise in Scala 3 programs, but it is indeed unverified and we provide no separate formal argument or exhaustive validation for the full predicate fragment (including dependent predicates, recursive refinements, and intersections). In the revised version we will add a short subsection in the implementation section (currently Section 6) that (1) explicitly states the assumption made by the proof, (2) describes the solver's design and its intended coverage, and (3) notes the absence of a machine-checked correctness argument for the solver itself. We will also record this as an item for future work. This revision clarifies the boundary between the proven core and the prototype without changing the soundness theorem or the solver implementation. revision: partial

Circularity Check

0 steps flagged

No significant circularity; soundness proof is mechanized externally in Rocq

full rationale

The paper's core claim is a type soundness proof for a core calculus (dependent functions, bounded polymorphism, equi-recursive types, unions/intersections, refinements) mechanized in Rocq using a fuel-bounded definitional interpreter and semantic typing under partial-correctness semantics. This is an independent formalization against an external semantics and does not reduce any result to fitted parameters, self-definitions, or self-citation chains. The prototype's lightweight e-graph solver for predicate entailment is presented as an implementation detail separate from the mechanized proof, which treats entailment as an assumed decision procedure. No equations or derivations in the provided claims equate outputs to inputs by construction, and the result is self-contained against the external Rocq benchmark.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work extends standard type-theoretic constructs without introducing new free parameters or postulated entities; the only non-standard element is the choice of fuel-bounded partial semantics for the proof.

axioms (2)
  • standard math The core calculus combines dependent function types, bounded polymorphism, positive equi-recursive types, union and intersection types, and refinement types under partial-correctness semantics.
    These are established constructs in advanced type theory; the paper invokes them as background for the new refinement integration.
  • domain assumption A fuel-bounded definitional interpreter and semantic typing suffice to establish type soundness.
    The proof relies on this semantic model rather than a full operational semantics of Scala.

pith-pipeline@v0.9.0 · 5475 in / 1361 out tokens · 53734 ms · 2026-05-12T01:04:57.950087+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

42 extracted references · 42 canonical work pages · 1 internal anchor

  1. [1]

    Nada Amin and Tiark Rompf. 2017. Type soundness proofs with definitional interpreters.SIGPLAN Not.52, 1 (Jan. 2017), 666–679. doi:10.1145/3093333.3009866

    work page doi:10.1145/3093333.3009866 2017

  2. [2]

    2024.Syntax and Runtime Checks for Qualified Types in Scala 3

    Quentin Bernet. 2024.Syntax and Runtime Checks for Qualified Types in Scala 3. Master’s thesis. École Polytechnique Fédérale de Lausanne (EPFL), Lausanne, Switzerland

    work page 2024

  3. [3]

    Borkowski, Niki Vazou, and Ranjit Jhala

    Michael H. Borkowski, Niki Vazou, and Ranjit Jhala. 2024. Mechanizing Refinement Types.Proc. ACM Program. Lang. 8, POPL, Article 70 (Jan. 2024), 30 pages. doi:10.1145/3632912

    work page doi:10.1145/3632912 2024

  4. [4]

    Mitchell, and Andre Scedrov

    Luca Cardelli, Simone Martini, John C. Mitchell, and Andre Scedrov. 1991. An extension of system F with subtyping. In Theoretical Aspects of Computer Software, Takayasu Ito and Albert R. Meyer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 750–770

    work page 1991

  5. [5]

    Robert Cartwright. 1976. User-Defined Data Types as an Aid to Verifying LISP Programs. InProceedings of the 3rd ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL). ACM, 228–256. doi:10.1145/512927. 512951

    work page doi:10.1145/512927 1976

  6. [6]

    École Polytechnique Fédérale de Lausanne. 2024. The Scala 3 Language Specification, Version 3.4. https://www.scala- lang.org/files/archive/spec/3.4/ §13: Syntax Summary

    work page 2024

  7. [7]

    Chris Fallin. 2023. Cranelift’s Acyclic Egraph implementation. https://docs.rs/cranelift-egraph/latest/cranelift_egraph/. Rust crate documentation

    work page 2023

  8. [8]

    Cormac Flanagan. 2006. Hybrid type checking.SIGPLAN Not.41, 1 (Jan. 2006), 245–256. doi:10.1145/1111320.1111059

    work page doi:10.1145/1111320.1111059 2006

  9. [9]

    Tim Freeman and Frank Pfenning. 1991. Refinement types for ML.SIGPLAN Not.26, 6 (May 1991), 268–277. doi:10.1145/113446.113468

    work page doi:10.1145/113446.113468 1991

  10. [10]

    Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, and Derek Dreyer. 2024. RefinedRust: A Type System for High-Assurance Verification of Rust Programs.Proc. ACM Program. Lang.8, PLDI, Article 192 (June 2024), 25 pages. doi:10.1145/3656422

    work page doi:10.1145/3656422 2024

  11. [11]

    Catarina Gamboa, Abigail Reese, Alcides Fonseca, and Jonathan Aldrich. 2025. Usability Barriers for Liquid Types. Proc. ACM Program. Lang.9, PLDI, Article 224 (June 2025), 26 pages. doi:10.1145/3729327

    work page doi:10.1145/3729327 2025

  12. [12]

    Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, and Robbert Krebbers

    Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, and Robbert Krebbers. 2020. Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris.Proc. ACM Program. Lang.4, ICFP (2020), 114:1–114:29. doi:10.1145/3408996

    work page doi:10.1145/3408996 2020

  13. [13]

    Jad Hamza, Nicolas Voirol, and Viktor Kunčak. 2019. System FR: formalized foundations for the stainless verifier.Proc. ACM Program. Lang.3, OOPSLA, Article 166 (Oct. 2019), 30 pages. doi:10.1145/3360592 First-Class Refinement Types for Scala 25

    work page doi:10.1145/3360592 2019

  14. [14]

    Li Haoyi. 2016. Fansi: Scala library for manipulating Fancy Ansi colored strings. https://github.com/com-lihaoyi/fansi. Accessed: 2026-03-18

    work page 2016

  15. [15]

    Iltotore. 2021. Iron: A compile-time and runtime refinement library for Scala 3. https://github.com/Iltotore/iron. Accessed: 2026-02-11

    work page 2021

  16. [16]

    Ranjit Jhala. 2019. Why Refinement Types? https://ucsd-progsys.github.io/liquidhaskell/blogposts/2019-10-20-why- types.lhs/. Accessed: 2026-03-09

    work page 2019

  17. [17]

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

    work page doi:10.1561/2500000032 2021

  18. [18]

    Matthias Keil and Peter Thiemann. 2015. Blame assignment for higher-order contracts with intersection and union. SIGPLAN Not.50, 9 (Aug. 2015), 375–386. doi:10.1145/2858949.2784737

    work page doi:10.1145/2858949.2784737 2015

  19. [19]

    Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. 2023. Verus: Verifying Rust Programs using Linear Ghost Types.Proc. ACM Program. Lang.7, OOPSLA1, Article 85 (April 2023), 30 pages. doi:10.1145/3586037

    work page doi:10.1145/3586037 2023

  20. [20]

    Rustan M

    K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. InLogic for Programming, Artificial Intelligence, and Reasoning, Edmund M. Clarke and Andrei Voronkov (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 348–370

    work page 2010

  21. [21]

    Greg Nelson and Derek C. Oppen. 1980. Fast Decision Procedures Based on Congruence Closure.J. ACM27, 2 (April 1980), 356–364. doi:10.1145/322186.322198

    work page doi:10.1145/322186.322198 1980

  22. [22]

    Martin Odersky, Yaoyu Zhao, Yichen Xu, Oliver Bračevac, and Cao Nguyen Pham. 2026. Tracking Capabilities for Safer Agents. arXiv:2603.00991 [cs.AI] https://arxiv.org/abs/2603.00991

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  23. [23]

    Myreen, Ramana Kumar, and Yong Kiam Tan

    Scott Owens, Magnus O. Myreen, Ramana Kumar, and Yong Kiam Tan. 2016. Functional Big-Step Semantics. In Proceedings of the 25th European Symposium on Programming Languages and Systems - Volume 9632. Springer-Verlag, Berlin, Heidelberg, 589–615. doi:10.1007/978-3-662-49498-1_23

    work page doi:10.1007/978-3-662-49498-1_23 2016

  24. [24]

    Li, and Andrew W

    Zoe Paraskevopoulou, John M. Li, and Andrew W. Appel. 2021. Compositional optimizations for CertiCoq.Proc. ACM Program. Lang.5, ICFP, Article 86 (Aug. 2021), 30 pages. doi:10.1145/3473591

    work page doi:10.1145/3473591 2021

  25. [25]

    Rondon, Ming Kawaguci, and Ranjit Jhala

    Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. 2008. Liquid types.SIGPLAN Not.43, 6 (June 2008), 159–169. doi:10.1145/1379022.1375602

    work page doi:10.1145/1379022.1375602 2008

  26. [26]

    Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, and Deepak Garg. 2021. RefinedC: automating the foundational verification of C code with refined ownership types. InProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation(Virtual, Canada)(PLDI 2021). Association for C...

    work page doi:10.1145/3453483.3454036 2021

  27. [27]

    Georg Stefan Schmid and Viktor Kuncak. 2016. SMT-based checking of predicate-qualified types for Scala. InProceedings of the 2016 7th ACM SIGPLAN Symposium on Scala(Amsterdam, Netherlands)(SCALA 2016). Association for Computing Machinery, New York, NY, USA, 31–40. doi:10.1145/2998392.2998398

    work page doi:10.1145/2998392.2998398 2016

  28. [28]

    2024.Runtime Checks for Qualified Types in Scala 3

    Valentin Schneeberger. 2024.Runtime Checks for Qualified Types in Scala 3. Bachelor’s thesis. École Polytechnique Fédérale de Lausanne (EPFL), Lausanne, Switzerland

    work page 2024

  29. [29]

    Rudi Schneider, Thomas Koehler, and Michel Steuwer. 2025. Slotted E-Graphs. InProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). Association for Computing Machinery

    work page 2025

  30. [30]

    Ke Sun, Di Wang, Sheng Chen, Meng Wang, and Dan Hao. 2024. Formalizing, Mechanizing, and Verifying Class-Based Refinement Types. In38th European Conference on Object-Oriented Programming (ECOOP 2024) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 313), Jonathan Aldrich and Guido Salvaneschi (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für ...

    work page doi:10.4230/lipics.ecoop.2024.39 2024

  31. [31]

    Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago Zanella- Béguelin. 2016. Dependent types and multi-monadic effects in F*.SIGPLAN Not.51, 1 (Jan. 2016), 256–270. doi:10. 1145/2914770.2837655

    work page arXiv 2016

  32. [32]

    2025.The Rocq Prover

    The Rocq Development Team. 2025.The Rocq Prover. https://rocq-prover.org/

    work page 2025

  33. [33]

    Frank S. Thomas. 2015. refined: Refined is a Scala library for refinement types. https://github.com/fthomas/refined. Accessed: 2026-02-11

    work page 2015

  34. [34]

    Amin Timany, Robbert Krebbers, Derek Dreyer, and Lars Birkedal. 2024. A Logical Approach to Type Soundness.J. ACM71, 6, Article 40 (Nov. 2024), 75 pages. doi:10.1145/3676954

    work page doi:10.1145/3676954 2024

  35. [35]

    Rondon, and Ranjit Jhala

    Niki Vazou, Patrick M. Rondon, and Ranjit Jhala. 2013. Abstract refinement types. InProceedings of the 22nd European Conference on Programming Languages and Systems(Rome, Italy)(ESOP’13). Springer-Verlag, Berlin, Heidelberg, 209–228. doi:10.1007/978-3-642-37036-6_13

    work page doi:10.1007/978-3-642-37036-6_13 2013

  36. [36]

    Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones

    Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. 2014. Refinement types for Haskell.SIGPLAN Not.49, 9 (Aug. 2014), 269–282. doi:10.1145/2692915.2628161 26 Matt Bovel, Viktor Kunčak, and Martin Odersky

    work page doi:10.1145/2692915.2628161 2014

  37. [37]

    Scott, Ryan R

    Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala

    work page

  38. [38]

    ACM Program

    Refinement reflection: complete verification with SMT.Proc. ACM Program. Lang.2, POPL, Article 53 (Dec. 2017), 31 pages. doi:10.1145/3158141

    work page doi:10.1145/3158141 2017

  39. [39]

    Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. 2021. egg: Fast and extensible equality saturation.Proc. ACM Program. Lang.5, POPL, Article 23 (Jan. 2021), 29 pages. doi:10.1145/3434304

    work page doi:10.1145/3434304 2021

  40. [40]

    Yichen Xu, Oliver Bračevac, Cao Nguyen Pham, and Martin Odersky. 2025. What’s in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures.Proc. ACM Program. Lang.9, OOPSLA2, Article 334 (Oct. 2025), 28 pages. doi:10.1145/3763112

    work page doi:10.1145/3763112 2025

  41. [41]

    Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche. 2017. HACL*: A Verified Modern Cryptographic Library. InProceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security(Dallas, Texas, USA)(CCS ’17). Association for Computing Machinery, New York, NY, USA, 1789–1806. doi:10.1145/3133956.3134043

    work page doi:10.1145/3133956.3134043 2017

  42. [42]

    Philip Zucker. 2024. Acyclic Egraphs and Smart Constructors. https://www.philipzucker.com/smart_constructor_ aegraph/. Blog post. First-Class Refinement Types for Scala 27 A More examples // Example 3:Matrix operations with checked dimensions case classMatrix(width:Pos, height:Pos): private valsize=width * height private valdata=CheckedArray(size.runtimeC...

    work page 2024