THE LIVING ARCHIVE

From punched cards to autonomous collaborators: the ideas, people, languages and systems that taught machines to follow—and increasingly interpret—human intent.

PAST / PRESENT / NEXT

Collection

Tag: xavier-leroy

CompCert and the Verified Compiler: Proving the Translator Correct

CompCert used Coq to prove semantic preservation across a realistic optimizing C compiler, closing the assurance gap between verified source programs and generated assembly.

↗