×

Selected papers on AUTOMATH, dedicated to N. G. de Bruijn. (English) Zbl 0822.03009

Studies in Logic and the Foundations of Mathematics. 133. Amsterdam: Elsevier. xix, 1024 p. (1994).
[The articles of this volume will not be indexed individually.]
AUTOMATH is a language developed in 1967-1968 at the Eindhoven University of Technology, The Netherlands, as a suitable language to express large parts of mathematics in such a way that the correctness of the mathematical contents is guaranteed by its grammar rules. The papers selected to be presented in the book are grouped according to six major topics: motivation and exposition, language definition and special related subjects, theory, illustrative test examples, verification and other related works; inside each of these parts the papers are ordered mainly chronologically. Besides historical considerations and the description of the general framework of AUTOMATH, some relationships between typed lambda calculus and a series of fundamental concepts in higher programming languages are pointed out in the first part of the book. Next, some detailed formalized descriptions of several versions of AUTOMATH and their corresponding lambda calculus foundations are given in part B. The full theoretical support of AUTOMATH is developed in the papers grouped in part C of the book. A series of illustrative examples of translations of already existing mathematical texts into a language of AUTOMATH type are presented in part D. The structures and possible implementations of AUTOMATH verifying programs are presented by the next three papers grouped in part E of the book. Finally, some related topics and suggestions for further developments are discussed in the papers of part F.
The topics and themes developed by the authors of the papers represent an attempt to explain AUTOMATH and to investigate its fundamentals and capacities to capture and express mathematical reasoning.

MSC:

03B35 Mechanization of proofs and logical operations
03B40 Combinatory logic and lambda calculus
00B60 Collections of reprinted articles

Biographic References:

Bruijn, N. G. de

Software:

Automath
PDFBibTeX XMLCite