Synopses & Reviews
This volume contains the papers presented at a workshop held at Banff, Canada, 10-14 September 1990, which gathered together researchers interested in applying higher order techniques to: reasoning about concurrency, specifying and reasoning about synchronous circuits (specifically butterfly circuits), reasoning about delay insensitive circuits, categorical concepts for programming languages, and support for automated reasoning. In the 1960's and 70's, Landin, Burge and others showed us how to apply higher order techniques and laid practical foundations for modern functional programming. The advantage of higher order techniques is clear: they provide succinct and clear specifications that are easy to reason with. Over the past few years, higher order techniques have been applied successfully to a wide range of applications in software, hardware, and communications. While the papers present recent research results, they have been written so as to be accessible to non hard- liners. This volume will be of interest to readers who wish to gain a broad view of the subject, as well as to specialists in specific subtopics.
Table of Contents
From the contents: Partially deterministic functions.- Expressing and reasoning about non-deterministic functional programming.- Process algebra as a tool for real time analysis.- A fast flutter by the Fourier transform.- Parallel computations and delay-insensitive circuits.- A higher order logic mechanization of the CSP failures-divergences model.- Evaluation logic.- Simple type theory in EVES.- Formal synthesis.- Proving (facts about) Ruby.