On the role of automated theorem proving in the compile-time derivation of concurrency (Q1819947)

A recent trend in program development is to derive correct implementations from program specifications by the application of a formal calculus, a ''programming methodology''. The application of formal rules lends itself to automation. We investigate the automation of one part of a methodology for programming with concurrency. In this methodology, concurrency is derived by transforming the sequential execution of a program into an equivalent concurrent execution on the basis of formal transformation rules. Such rules can be interpreted as theorems of semantic equivalences. The mechanical certification of these theorems would significantly enhance the reliability of the methodology. The following is an initial exploration of this problem applied to a certain class of programs: sorting networks. We present an implementation of a part of the underlying semantic theory in Boyer and Moore's mechanized logic, and report on the mechanical proof of a transformation that derives concurrency for an insertion sort.