Selected Papers on AutomathR.P. Nederpelt, J.H. Geuvers, R.C. de Vrijer The present volume contains a considered choice of the existing literature on Automath. Many of the papers included in the book have been published in journals or conference proceedings, but a number have only circulated as research reports or have remained unpublished. The aim of the editors is to present a representative selection of existing articles and reports and of material contained in dissertations, giving a compact and more or less complete overview of the work that has been done in the Automath research field, from the beginning to the present day. Six different areas have been distinguished, which correspond to Parts A to F of the book. These areas range from general ideas and motivation, to detailed syntactical investigations. |
Contents
55 | |
Language deflnition and special subjects | 249 |
Theory | 369 |
Text examples | 685 |
Verification | 781 |
Related topics | 839 |
Bibliography | 973 |
975 | |
Indexes | 995 |
Index of Names | 997 |
1003 | |
1005 | |
Common terms and phrases
2-expressions 3-reduction A E B abbreviation abstraction abstractors application AUT-II AUT-QE Automath languages axioms Benthem Jutting beta reduction bool bound variables Bruijn called cartesian product Church-Rosser Church-Rosser theorem closure constants construction context Daalen 73 defined definitional equality denoted domain example extended formal free variables function induction interpretation introduced lambda calculus lambda tree Landau Lemma logic mathematics metalanguage natural deduction natural numbers Nederpelt norm normal form notation objects occur p-normable partial function predicate predicate logic proof prop proposition prove quantifier real number reduction refer rule Section segment semantics sequence simultaneous substitution single-step statement string strong normalization substantive substitution symbol syntactic theorem theory typ(A type inclusion typed lambda calculus write X-calculus
References to this book
Programming Languages: Implementations, Logics, and Programs: 8th ... S.Doaitse Swierstra Limited preview - 1996 |