Showing cs.LOShow all
2 papers · 1 filter
cs.LO2026
Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar
Sage Binder, Hanna Lachnitt, Katherine Kosaian
In Isabelle/HOL, declarative proofs written in the Isar language are widely appreciated for their readability and robustness. However, some users may prefer writing procedural "app…
cs.LO2024
Formalizing Pick's Theorem in Isabelle/HOL
Sage Binder, Katherine Kosaian
We formalize Pick's theorem for finding the area of a simple polygon whose vertices are integral lattice points. We are inspired by John Harrison's formalization of Pick's theorem…