Lighting talks and closing discussion
summary
spectTech starts from a dependently typed DSL that encodes WebAssembly plus annotations and already yields automated artifacts (LaTeX, an interpreter and translated definitions into proof assistants); an MSc student automatically translated definitions from the prior "wamer" development and mechanized preservation by copying and adapting proofs, while progress remains undone and a new MSc will tackle it; work targets synchronized mechanizations across Coq Isabelle Lean, maximising automation, minimizing hand proofs, and publishing the result.
AI-written summary · about
related talks
16mBringing the WebAssembly Standard up to Speed with SpecTec
51mLightning Talks
29mVerification of WebAssembly Features
30mMechanising WebAssembly Well?
47m[Keynote] Keynote and SpecTec demo
26mSpecTec, a Single Source of Truth
19mProgressful Interpreters for Efficient WebAssembly Mechanisation
01h 06mAs low-level as possible, but no lower