IV Higher Order Workshop, Banff 1990

1. Front Matter

   Pages i-x

   PDF

2. Partially Deterministic Functions

   • F. Warren Burton, W. Ken Jackson

   Pages 1-10

3. Nondeterministic Functional Programming with Sets

   • John Hughes, John O’Donnell

   Pages 11-31

4. Process Algebra as a Tool for Real Time Analysis

   • Faron Moller

   Pages 32-53

5. The study of butterflies

   • Geraint Jones, Mary Sheeran

   Pages 54-65

6. Sorts of butterflies

   • Mary Sheeran

   Pages 66-76

7. A fast flutter by the Fourier transform

   • Geraint Jones

   Pages 77-84

8. Parallel Computations and Delay-Insensitive Circuits

   • Jo C. Ebergen

   Pages 85-104

9. The Nature of Delay-Insensitive Computing

   • Martin Rem

   Pages 105-122

10. A Higher Order Logic Mechanization of the CSP Failure-Divergence Semantics

    • Albert J. Camilleri

    Pages 123-150

11. Partial Functions, Ordered Categories, Limits and Cartesian Closure

    • C. Barry Jay

    Pages 151-161

12. Evaluation Logic

    • Andrew M. Pitts

    Pages 162-189

13. Conditional Control is not quite Categorical Control

    • J. Robin, B. Cockett

    Pages 190-217

14. Simple Type Theory in EVES

    • Mark Saaltink, Dan Craigen

    Pages 218-244

15. Formal Synthesis

    • Michael P. Fourman, Roberto A. Hexsel

    Pages 245-264

16. Proving (facts about) Ruby

    • Lars Rossen

    Pages 265-283

17. Back Matter

    Pages 285-285

    PDF

It is many years since Landin, Burge and others showed us how to apply higher order techniques and thus laid some foundations for modern functional programming. The advantage of higher order descriptions - that they can be very succinct and clear - has been percolating through ever since. Current research topics range from the design, implementation and use of higher order proof assistants and theorem provers, through program specification and verification, and programming language design, to its applications in hardware description and verification. The papers in this book represent the presentations made at a workshop held at Banff, Canada, September 10-14 1990 and organised by the Computer Science Department of the University of Calgary. The workshop gathered together researchers interested in applying higher order techniques to a range of problems. The workshop format had a few (but fairly long) presentations per day. This left ample time for healthy discussion and argument, many of which continued on into the small hours. With so much to choose from, the program had to be selective. This year's workshop was divided into five parts: 1. Expressing and reasoning about concurrency: Warren Burton and Ken Jackson, John Hughes, and Faron Moller. 2. Reasoning about synchronous circuits: Geraint Jones and Mary Sheeran (with a bonus on the fast Fourier transform from Geraint). 3. Reasoning about asynchronous circuits: Albert Camilleri, Jo Ebergen, and Martin Rem. 4. Categorical concepts for programming languages: Robin Cockett, Barry Jay, and Andy Pitts.

• Higher order techniques
• Ruby
• Softwareentwicklung
• communication
• concurrency
• development
• formal methods
• functional programming
• language
• logic
• process algebra
• programming
• programming language
• semantics
• software

• Department of Computer Science, University of Calgary, Calgary, Canada

  Graham Birtwistle

Policies and ethics