Mathematics of Program Construction

Towards automatic parallelization of logic programs.- Functional Algorithm Design.- Mathematics of software engineering.- Program construction in intuitionistic Type Theory.- Computer-aided computing.- Derivation of parallel algorithms from functional specifications to CSP processes.- Architecture independent massive parallelization of divide-and-conquer algorithms.- Exploring summation and product operators in the refinement calculus.- An action system specification of the caltech asynchronous microprocessor.- Formal derivation of CSP programs from temporal specifications.- A compositional proof system for asynchronously communicating processes.- A graphical calculus.- A simple, efficient, and flexible implementation of flexible arrays.- Induction and recursion on datatypes.- Program construction by parts.- An initial-algebra approach to directed acyclic graphs.- Algebraic proof assistants in HOL.- Angelic termination in Dijkstra's calculus.- Extracting programs with exceptions in an impredicative type system.- Synthesizing proofs from programs in the Calculus of Inductive Constructions.- A general scheme for breadth-first graph traversal.- Specware: Formal support for composing software.- A refinement relation supporting the transition from unbounded to bounded communication buffers.- ImpUNITY: UNITY with procedures and local variables.