Extending CASL with Higher-order Functions -- Design Proposal

Anne E. Haxthausen1
Bernd Krieg-Brückner
Till Mossakowski2

7 January 1998

This document is available by FTP in various formats. It was converted to HTML using Hyperlatex 2.2.


We present a proposal for the design of the higher-order extension of CASL. For each design step, we have tried to find the best of several possible alternatives, give a motivation for the preferred alternative and argue why the other alternatives are not taken.

This note discusses function spaces, product types, partial functions, predicates, subsorting, signature morphisms and \-abstraction. A forthcoming note will be devoted to polymorphism, type constructors and dependent types. A companion note, replacing L-2, will explain the formal details of the proposal made in this note.

  • 1 What can be declared in a basic item?
  • 2 Reduction to first-order logic
  • 3 What is a function space?
  • 4 Product types and arities of functions
  • 5 Partial function spaces and partial types
  • 6 Predicate types
  • 7 Subsorting
  • 8 \-abstraction
  • 9 Description operator
  • 10 Signature morphisms
  • References
  • Footnotes

  • CoFI Note: L-8 ---- 7 January 1998.
    Comments to till@informatik.uni-bremen.de