Extending CASL with Higher-order Functions

Anne Haxthausen1
Bernd Krieg-Brückner2
Till Mossakowski3

10 April 1997

This document is available for browsing on WWW, and in various formats for printing by FTP.

Abstract

This note studies how the CASL language can be extended with higher-order functions.

Contents

  • 1 Introduction
  • Terminology:
  • 2 Proposals for changes to the syntax
  • 2.1 Introduction of types instead of sorts
  • 2.2 More general application terms
  • 3 Semantics
  • 3.1 Requirements to the semantics
  • 3.2 Extensions of the subsort relation
  • 3.3 Well-typed terms and formulas
  • 3.4 Expansions to an underlying logic
  • 3.5 Equivalent expansions
  • Appendices:
  • 4 One possibility for the underlying logic
  • 4.1 A higher-order subsorted logic
  • 4.2 A generalised subsorted logic
  • Footnotes
    • This document was converted from LaTeX2e sources to HTML using Hyperlatex 2.2.
    CoFI Note: L-2 --Version 1.0-- 10 April 1997.
    Comments to ah@it.dtu.dk