Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves
type: Item
instance of: scholarly article
title: Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves
zbMATH Open document ID: 1140.68491
author: Laurence Rideau
author: Bernard Paul Serpette
author: Xavier Leroy
published in: Journal of Automated Reasoning
publication date: 2008-06-11T00:00:00Z
full work available at URL: parallel-move.pdf
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68N20
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 5287723
zbMATH Keywords: Parallel move
zbMATH Keywords: Parallel assignment
zbMATH Keywords: Compilation
zbMATH Keywords: Compiler correctness
zbMATH Keywords: Coq proof assistant
describes a project that uses: Coq
describes a project that uses: OCaml
MaRDI profile type: Publication
OpenAlex ID: W2118598235
cites work: Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: Types for Proofs and Programs
cites work: Verification of non-functional programs using interpretations in type theory
cites work: Formal certification of a compiler back-end or
cites work: Q4435471
cites work: A note on implementing parallel assignment instructions
cites work: Parallel assignment revisited
DOI: 10.1007/S10817-007-9096-8
Recommended article: A Coq library for verification of concurrent programs
Recommended article: A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction
Recommended article: Formal verification of cP systems using Coq
Recommended article: Verification of dynamic bisimulation theorems in Coq
Recommended article: Q3347266
Recommended article: Verification of the correctness of compiler optimization using co-induction
Recommended article: A Coq Library for Internal Verification of Running-Times
Recommended article: Q2754056
Recommended article: Q4484330
description: scientific article; zbMATH DE number 5287723