New Book Announcement:
Solving Higher-Order Equations
From Logic to Programming
Christian Prehofer, TU Muenchen,
Birkhauser Progress in Theoretical Computer Science Series
This monograph develops techniques for equational reasoning and
declarative programming based on higher-order logic. The author
presents a novel framework for the full integration of declarative
programming models and shows its application. On the technical side,
he integrates the main results of both worlds. The book presents
completeness results as common in logic programing and also
generalizes evaluation strategies found in current functional
programming languages to this setting.
The book includes a thorough introduction to higher-order equational
logic, higher-order rewriting, and unification. This is followed by a
stepwise development from general equational reasoning toward
effective methods for declarative programming in higher-order logic
and lambda-calculus. Another important, complementing, result shows
that higher order unification, the basic inference engine in logic
programming, is decidable for programming applications. The book
concludes with applications showing the utility of higher-order logic
for symbolic computation with complex structures in mathematics and
programming. The examples include symbolic differentiation, program
transformation and declarative programming.
The book is aimed at researchers and advanced students in computer
science and mathematics with interests in declarative programming,
symbolic computation, term rewriting, equational reasoning, and
theorem proving. It can provide a firm basis for a variety of graduate
courses in logic and theoretical computer science.
More information at:
http://www.birkhauser.com/cgi-win/ISBN/0-8176-4032-0
Received on Sa Mai 09 1998 - 15:54:00 CEST