VLDB 2026 Research / reviewers in the wild / expert
Sage Binder
dblp:376/2139
· DBLP profile ↗
3ranked-venue papers
3as first author
3since 2021 · last 2026
0009-0004-4776-2018ORCID · corroborated
Domains — the database's venue-derived domains; a paper can count in several
Theory of computation · 3 · 3 first-author · 3 since 2021Artificial intelligence and machine learning · 1 · 1 first-author · 1 since 2021Software engineering, systems software and programming languages · 1 · 1 first-author · 1 since 2021
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured IsarabstractIn Isabelle/HOL, declarative proofs written in the Isar language are widely appreciated for their readability and robustness. However, some users may prefer writing procedural "apply-style" proofs since they enable rapid exploration of the search space. To get the best of both worlds, we introduce Apply2Isar, a tool for Isabelle/HOL that automatically converts apply-style proofs to declarative Isar. This allows users to write complex, possibly fragile apply-style proofs, and then automatically convert them to more readable and robust declarative Isar proofs. To demonstrate the efficacy of Apply2Isar in practice, we evaluate it on a large benchmark set consisting of apply-style proofs from the Isabelle Archive of Formal Proofs. Sage Binder, Hanna Lachnitt, Katherine Kosaian |
ITP | 1 |
| 2025 | Formalizing the Hidden Number Problem in Isabelle/HOL
Sage Binder, Eric Ren, Katherine Kosaian |
ITP | 1 |
| 2024 | Formalizing Pick's Theorem in Isabelle/HOL
Sage Binder, Katherine Kosaian |
CICM | 1 |