Proof and Computation

Logical concepts and methods are of growing importance in many areas of computer science. The proofs-as-programs paradigm and the wide acceptance of Prolog show this clearly. The logical notion of a formal proof in various constructive systems can be viewed as a very explicit way to describe a computation procedure. Also conversely, the development of logical systems has been influenced by accumulating knowledge on rewriting and unification techniques. This volume contains a series of lectures by leading researchers giving a presentation of new ideas on the impact of the concept of a formal proof on computation theory. The subjects covered are: specification and abstract data types, proving techniques, constructive methods, linear logic, and concurrency and logic.

List of contents

Program Development by Proof Transformation.- Concurrent Processes and Petri Nets.- Using Reflection to Explain and Enhance Type Theory.- On Geometry of Interaction.- Behavioural Specifications.- A Deductive Approach to Logic Programming.- Rewrite Proofs and Computations.- Action Structures and the Pi Calculus.- Linear Logic and Computation: A Survey.- Computable Functions on Stream Algebras.- The Proof Theoretic Complexity of Recursive Programs.

Product details

• Assisted by: Helmu Schwichtenberg (Editor), Helmut Schwichtenberg (Editor)
• Publisher: Springer, Berlin
• Languages: English
• Product format: Paperback / Softback
• Released: 05.12.2012
• EAN: 9783642793639
• ISBN: 978-3-642-79363-9
• No. of pages: 470
• Dimensions: 155 mm x 26 mm x 235 mm
• Weight: 733 g
• Illustrations: VII, 470 p.
• Series: NATO ASI Series F: Computer and Systems Sciences; Nato ASI Subseries F: Nato ASI Series (closed) / Nato ASI Subseries F: (closed); NATO ASI Series; NATO ASI Series F: Computer and Systems Sciences; Nato ASI Subseries F:
• Subject: Natural sciences, medicine, IT, technology > IT, data processing > IT