Type-Based Termination

Autor Abel, Andreas
Buchtitel Type-Based Termination
Untertitel A Polymorphic Lambda-Calculus with Sized Higher-Order Types
VerlagHarland media
ISBN-10 3-938363-04-5
ISBN-13 978-3-938363-04-1
Seitenzahl 218
Verkaufspreis 39.80 €
Buchformat 21x14,8 (DIN A5)
Cover Softcover
Veröffentlichung 02/2007

Buch / Bücher

Andreas Abel addresses the problem of ensuring that computer programs terminates, meaning that their execution halts after some time and delivers a result. He considers functional programs in which repeating computations are programmed with recursion. By the use of a type system, recursion is restricted to guarantee termination; only terminating programs, yet not all, are accepted by the compiler. Several classical algorithms from computer science textbooks are implemented in this language with the type-based termination check in order to demonstrate its expressivity and practicality. The type-based termination check is mathematically proven correct by constructing a semantics where each type is interpreted by a set of terminating programs.

The book is aimed at researchers and professionals with a strong interest in programming language theory.

Copyright 1996-2022
Dr. Peter E. Harland
Ernst-Thälmann-Str. 16
07747 Jena