The automated proof of a trace transformation for a bitonic sort

DOI10.1016/0304-3975(86)90033-2zbMATH Open0618.68053OpenAlexW2091172700MaRDI QIDQ1822503FDOQ1822503

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

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

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)

Cites Work

• Title not available (Why is that?)
• Programming as a Discipline of Mathematical Nature
• Title not available (Why is that?)
• Automatic program verification. I: A logical basis and its implementation
• Mechanical proofs about computer programs
• A methodology for programming with concurrency: An informal presentation
• Title not available (Why is that?)
• Compiler specification and verification
• A methodology for programming with concurrency: The formalism
• On the role of automated theorem proving in the compile-time derivation of concurrency

Cited In (7)

• A note on bitonic sorting
• Title not available (Why is that?)
• A theorem prover for a computational logic
• Odd-even sort in powerlists
• Parallelization of divide-and-conquer in the Bird-Meertens formalism
• Types for Proofs and Programs
• On optimal parallelization of sorting networks

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)