Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves

DOI10.1007/s10817-007-9096-8zbMath1140.68491OpenAlexW2118598235MaRDI QIDQ928671

Bernard Paul Serpette, Laurence Rideau, Xavier Leroy

Publication date: 11 June 2008

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/inria-00289709/file/parallel-move.pdf

zbMATH Keywords

CompilationCoq proof assistantCompiler correctnessParallel assignmentParallel move

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

A formally verified compiler back-end, The verified CakeML compiler backend

Uses Software

• Coq
• OCaml

Cites Work

• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A note on implementing parallel assignment instructions
• Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
• Parallel assignment revisited
• Verification of non-functional programs using interpretations in type theory
• Formal certification of a compiler back-end or
• Types for Proofs and Programs