|
| Author(s) |
Huet, Gerard (ed.) Plotkin, Gordon (ed.) |
|---|---|
| Title | Logical Environments |
| Publisher | CAMBRIDGE University Press |
| Year of publication | 1993 |
| Reviewed by | Doina TATAR |
This book is a selection of papers presented at the second annual Workshop held under the auspices of the ESPRIT Basic Research program "Logical Frameworks". This Workshop took place in Edinburgh, May, l991. (The first general workshop was organized in May 1990 in France). The title reflects a general awareness that, despite minor differences, the community now agrees on the general form of logical frameworks.
The papers constituting this volume have been arranged according to four themes. The first theme concerns the general problem of representing formal system: "Metalogical frameworks" by D.A. Basin and R.C. Constable, "Encoding of data types in Pure Construction Calculus: a semantic Justification " by S. Berardi, "Experience with FS0 as a framework Theory" by S. Matthews, A. Smaill and D. Basin, and "Logical Support for Modularization" by R. Diaconescu, J. Goguen and P. Stefaneas.
The second theme concerns basic algorithms of general use in proof assistants and is represented by the followings papers: "Algorithmic definition of lambda-typed lambda calculus" by N.G. Bruijin, "A Canonical Calculus of Residuals" by Y. Bertot and "Order-Sorted Polymorphism in Issabelle" by T. Nipkow.
The third paragraph is entitled "Logical Issues" and contains: "An Interpretation of Kleene's Slash in Type Theory " by J. Smith, "Inductive Data Types: Well-orderings Revizited" by H. Goguen and Z. Luo, "Witness Extraction in Classical Logic Through Normalization" by F. Barbanera and S. Berardi, "Finding the Answers in Classical Proofs" by C.R. Murthy and "Church-Rosser Property in Classical Free Deduction" by M. Parigot.
The final theme concerns experiments with proof assistants: "Completing the rationals and Metric Spaces in LEGO" by C. Jones and "A Machine Checked Proof that Ackermann's function is not Primitive Recursive" by N. Szasz.
The present volume give an overview of recent progress in the area for logic of computer science community.