The automated proof of a trace transformation for a bitonic sort

DOI10.1016/0304-3975(86)90033-2MaRDI QIDQ1822503zbMATH OpenOpenAlexFDO

Authors Chua-Huang Huang, Christian Lengauer

Publication date 1986

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(86)90033-2

zbMATH Keywords

concurrencystepwise refinementbitonic sorting

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Searching and sorting (68P10) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• On the role of automated theorem proving in the compile-time derivation of concurrency
• On optimal parallelization of sorting networks
• A note on bitonic sorting
• Automatic Parallelization and Optimization of Programs by Proof Rewriting
• Types for Proofs and Programs

Cites work

• scientific article; zbMATH DE number 4164171 (Why is no real title available?)
• scientific article; zbMATH DE number 3902008 (Why is no real title available?)
• scientific article; zbMATH DE number 3473265 (Why is no real title available?)
• A methodology for programming with concurrency: An informal presentation
• A methodology for programming with concurrency: The formalism
• Automatic program verification. I: A logical basis and its implementation
• Compiler specification and verification
• Mechanical proofs about computer programs
• On the role of automated theorem proving in the compile-time derivation of concurrency
• Programming as a Discipline of Mathematical Nature

Cited in

(7)

• A note on bitonic sorting
• scientific article; zbMATH DE number 3902008 (Why is no real title available?)
• Odd-even sort in powerlists
• A theorem prover for a computational logic
• Parallelization of divide-and-conquer in the Bird-Meertens formalism
• On optimal parallelization of sorting networks
• Types for Proofs and Programs

Describes a project that uses

Uses Software

• NQTHM

This page was built for publication: The automated proof of a trace transformation for a bitonic sort

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1822503)