Coq: The World's Best Macro Assembler? - 10-Year Most Influential Paper Talk

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.