8 citations · 8 across the 3 of their papers we have counts for
Showing cs.PLShow all
2 papers · 1 filter
cs.PL2024★ 8 cited
Mechanised Hypersafety Proofs about Structured Data: Extended Version
Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens +2
Arrays are a fundamental abstraction to represent collections of data. It is often possible to exploit structural properties of the data stored in an array (e.g., repetition or spa…
cs.PL2024
Small Scale Reflection for the Working Lean User
Vladimir Gladshtein, George Pîrlea, Ilya Sergey
We present the design and implementation of the Small Scale Reflection proof methodology and tactic language (a.k.a. SSR) for the Lean 4 proof assistant. Like its Coq predecessor S…