6 citations · 7 across the 4 of their papers we have counts for
4 papers · 1 filter
Foundational Refinement Proofs for EVM Bytecode, at the Price of Tokens
Lefteris Lazaropoulos, Zoe Paraskevopoulou
Relating executable code to a high-level model of its behavior has been a central concern of programming-language research for decades. Formally verified compilers, translation val…
Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)
Zoe Paraskevopoulou
We report on using an agentic coding assistant (Claude Code, powered by Claude Opus 4.6) to mechanize a substantial Rocq correctness proof from scratch, with human guidance but wit…
RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly
Zoe Paraskevopoulou, Michael Fitzgibbons, Michelle Thalakottur +3
Safe, shared-memory interoperability between languages with different type systems and memory-safety guarantees is an intricate problem as crossing language boundaries may result i…
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
Guido Martínez, Danel Ahman, Victor Dumitrescu +10
We introduce Meta-F*, a tactics and metaprogramming framework for the F* program verifier. The main novelty of Meta-F* is allowing the use of tactics and metaprogramming to dischar…