| Publication type: |
Article in Proceedings |
| Author: |
Markus Roggenbach, Lutz Schröder, Till Mossakowski |
| Editor: |
Christine Choppy, Didier Bert |
| Title: |
Specifying real numbers in CASL |
| Book / Collection title: |
Recent Developments in Algebraic Development Techniques, 14th International Workshop, WADT'99 |
| Volume: |
1827 |
| Page(s): |
146 – 161 |
| Series: |
Lecture Notes in Computer Science |
| Year published: |
2000 |
| Publisher: |
Springer, Berlin |
| Abstract: |
We present a weak theory of the real numbers in the first order specification language CASL. The aim is to provide a datatype for practical purposes, including the central notions and results of basic analysis. Our theory captures for instance e and pi, as well as the trigonometric and other standard functions. Concepts such as continuity, differentiation and integration are shown to be definable and tractable in this setting; Newton's Method is presented as an example of a numerical application. Finally, we provide a proper connection between the specified datatype and specifications of the real numbers in higher order logic and various set theories.
|
| ISBN: |
3-540-67898-0 |
| Internet: |
http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=1827&spage=146 |
| PostScript Version: |
http://www.informatik.uni-bremen.de/~lschrode/reals.ps.gz |
| Keywords: |
real numbers CASL |
| Status: |
Reviewed |
| Last updated: |
01. 02. 2006 |
