Ebook: Logic of Computation

The Marktoberdorf Summer School 1995 'Logic of Computation' was the 16th in a series of Advanced Study Institutes under the sponsorship of the NATO Scientific Affairs Division held in Marktoberdorf. Its scientific goal was to survey recent progress on the impact of logical methods in software development. The courses dealt with many different aspects of this interplay, where major progress has been made. Of particular importance were the following. • The proofs-as-programs paradigm, which makes it possible to extract verified programs directly from proofs. Here a higher order logic or type theoretic setup of the underlying language has developed into a standard. • Extensions of logic programming, e.g. by allowing more general formulas and/or higher order languages. • Proof theoretic methods, which provide tools to deal with questions of feasibility of computations and also to develop a general mathematical understanding of complexity questions. • Rewrite systems and unification, again in a higher order context. Closely related is the now well-established Grabner basis theory, which recently has found interesting applications. • Category theoretic and more generally algebraic methods and techniques to analyze the semantics of programming languages. All these issues were covered by a team of leading researchers. Their courses were grouped under the following headings.

---

The latest work by the world's leading authorities on the use of formal methods in computer science is presented in this volume, based on the 1995 International Summer School in Marktoberdorf, Germany. Logic is of special importance in computer science, since it provides the basis for giving correct semantics of programs, for specification and verification of software, and for program synthesis. The lectures presented here provide the basic knowledge a researcher in this area should have and give excellent starting points for exploring the literature. Topics covered include semantics and category theory, machine based theorem proving, logic programming, bounded arithmetic, proof theory, algebraic specifications and rewriting, algebraic algorithms, and type theory.

---

The latest work by the world's leading authorities on the use of formal methods in computer science is presented in this volume, based on the 1995 International Summer School in Marktoberdorf, Germany. Logic is of special importance in computer science, since it provides the basis for giving correct semantics of programs, for specification and verification of software, and for program synthesis. The lectures presented here provide the basic knowledge a researcher in this area should have and give excellent starting points for exploring the literature. Topics covered include semantics and category theory, machine based theorem proving, logic programming, bounded arithmetic, proof theory, algebraic specifications and rewriting, algebraic algorithms, and type theory.
Content:
Front Matter....Pages I-VII
Lectures on Semantics: The Initial Algebra and Final Coalgebra Perspectives....Pages 1-33
Introduction to Groebner Bases....Pages 35-66
Bounded Arithmetic and Propositional Proof Complexity....Pages 67-121
The Structure of Nuprl’s Type Theory....Pages 123-155
Axiomatisations, Proofs, and Formal Specifications of Algorithms: Commented Case Studies in the Coq Proof Assistant....Pages 157-199
Some Proof Theory of First Order Logic Programming....Pages 201-228
Timed Rewriting Logic for the Specification of Time-Sensitive Systems....Pages 229-264
Logic Programming and Meta-Logic....Pages 265-308
Proofs, Lambda Terms and Control Operators....Pages 309-347
Basic Proof Theory with Applications to Computation....Pages 349-394
Back Matter....Pages 395-401

---

The latest work by the world's leading authorities on the use of formal methods in computer science is presented in this volume, based on the 1995 International Summer School in Marktoberdorf, Germany. Logic is of special importance in computer science, since it provides the basis for giving correct semantics of programs, for specification and verification of software, and for program synthesis. The lectures presented here provide the basic knowledge a researcher in this area should have and give excellent starting points for exploring the literature. Topics covered include semantics and category theory, machine based theorem proving, logic programming, bounded arithmetic, proof theory, algebraic specifications and rewriting, algebraic algorithms, and type theory.
Content:
Front Matter....Pages I-VII
Lectures on Semantics: The Initial Algebra and Final Coalgebra Perspectives....Pages 1-33
Introduction to Groebner Bases....Pages 35-66
Bounded Arithmetic and Propositional Proof Complexity....Pages 67-121
The Structure of Nuprl’s Type Theory....Pages 123-155
Axiomatisations, Proofs, and Formal Specifications of Algorithms: Commented Case Studies in the Coq Proof Assistant....Pages 157-199
Some Proof Theory of First Order Logic Programming....Pages 201-228
Timed Rewriting Logic for the Specification of Time-Sensitive Systems....Pages 229-264
Logic Programming and Meta-Logic....Pages 265-308
Proofs, Lambda Terms and Control Operators....Pages 309-347
Basic Proof Theory with Applications to Computation....Pages 349-394
Back Matter....Pages 395-401
....