Coq: The World's Best Macro Assembler? - 10-Year Most Influential Paper Talk
Offered By: ACM SIGPLAN via YouTube
Course Description
Overview
Explore a 54-minute conference talk from ACM SIGPLAN's PPDP23 event, focusing on the 10-Year Most Influential Paper "Coq: the world's best macro assembler?" Delve into a Coq formalization of a subset of the x86 architecture, emphasizing brevity through the use of dependent types, type classes, and notation. Discover how the authors give the x86 semantics a makeover to counter its reputation for complexity. Learn about the concrete modeling of bits, bytes, and memory using functions computable within Coq, and how these representations are mapped to mathematical objects in the SSReflect library. Examine the use of notation to support conventional assembly code syntax inside Coq, including lexically-scoped labels. Understand how ordinary Coq definitions serve as a powerful "macro" feature for various programming constructs. Explore the assembler's capability to produce hex byte sequences and its correctness theorem relating machine code to separation-logic formulas for program verification.
Syllabus
[PPDP23] 10-Year Most Influential Paper Talk: Coq: the world's best macro assembler?
Taught by
ACM SIGPLAN
Related Courses
SPARK 2014AdaCore via Independent Automated Reasoning: Symbolic Model Checking
EIT Digital via Coursera Software Testing and Verification
University System of Maryland via edX Haskell for Imperative Programmers
YouTube Model Checking and Temporal Logic - E. Allen Emerson's Turing Award Lecture
Association for Computing Machinery (ACM) via YouTube