Prev Up
Go backward to 5.3 The Specification of the Reals in Higher-Order CASL
Go up to 5 More About the Specification BasicReal

5.4 A Short Remark on Related Work

There is surprisingly little work on the algebraic specification of the abstract reals. Some good work on real analysis in higher-order logic has been done by Harrison [Har98], including fully formal proofs of a substantial part of real analysis. This could be the basis for the specification of the reals in higher-order CASL. The presentation of Harrison probably can be simplified by using the powerful constructs of CASL and by working with an axiomatic description. Note that Harrison follows the Isabelle/HOL tradition of describing datatypes constructively as a conservative extension of HOL in order to ensure consistency. In CASL, we follow a more abstract axiomatic approach and prove consistency through (architectural) refinement.

CoFI Note: M-7 -- Version: 0.2 -- 13 April 1999.
Comments to

Prev Up