zbMATH — the first resource for mathematics

Reasoning in simple type theory. Festschrift in honor of Peter B. Andrews on his 70th birthday. (English) Zbl 1196.03002
Studies in Logic (London) 17. Mathematical Logic and Foundations. London: College Publications (ISBN 978-1-904987-70-3/pbk). 467 p. (2008).

Show indexed articles as search result.

The articles of this volume will be reviewed individually.
Indexed articles:
Andrews, Peter B., Some historical reflections, 3-34 [Zbl 1226.03002]
Church, Alonzo, A formulation of the simple theory of types, 35-47 [Zbl 1226.03015]
Henkin, Leon, Completeness in the theory of types, 49-59 [Zbl 1226.03018]
Andrews, Peter B., Resolution in type theory, 63-81 [Zbl 1226.03011]
Andrews, Peter B., General models, descriptions, and choice in type theory, 83-92 [Zbl 1227.03013]
Andrews, Peter B., General models and extensionality, 93-95 [Zbl 1226.03012]
Benzmüller, Christoph; Brown, Chad E.; Kohlhase, Michael, Cut elimination with \(\xi\)-functionality, 97-113 [Zbl 1226.03060]
Hermant, Olivier; Lipton, James, Cut elimination in the intuitionistic theory of types with axioms and rewriting cuts, constructively, 115-148 [Zbl 1226.03061]
Brown, Chad E., \(M\)-set models, 149-172 [Zbl 1226.03014]
Andrews, Peter B., Resolution and the consistency of analysis, 175-186 [Zbl 1226.03013]
Andrews, Peter B., On connections and higher-order logic, 187-221 [Zbl 1226.03025]
Farmer, William M., Andrews’ type theory with undefinedness, 223-242 [Zbl 1226.03017]
Kaminski, Mark; Smolka, Gert, A finite axiomatization of propositional type theory in pure lambda calculus, 243-258 [Zbl 1226.03019]
Dowek, Gilles, Skolemization in simple type theory: the logical and the theoretical points of view, 259-270 [Zbl 1226.03016]
Gabbay, Murdoch J.; Mathijssen, Aad, The lambda-calculus is nominal algebraic, 271-302 [Zbl 1226.03028]
Pfenning, Frank, Church and Curry: combining intrinsic and extrinsic typing, 303-338 [Zbl 1226.03020]
Kirchner, Claude; Kirchner, Florent; Kirchner, Hélène, Strategic computation and deduction, 339-364 [Zbl 1226.03027]
Andrews, Peter B.; Bishop, Matthew; Issar, Sunil; Nesmith, Dan; Pfenning, Frank; Xi, Hongwei, TPS: A theorem proving system for classical type theory, 367-399 [Zbl 1226.03026]
Benzmüller, Christoph; Paulson, Lawrence C., Exploring properties of normal multimodal logics in simple type theory with Leo-II, 401-421 [Zbl 1227.03017]
Miller, Dale, A proof-theoretic approach to the static analysis of logic programs, 423-442 [Zbl 1226.03041]
Xi, Hongwei, ATS/LF: A type system for constructing proofs as total functional programs, 443-467 [Zbl 1226.68026]
03-06 Proceedings, conferences, collections, etc. pertaining to mathematical logic and foundations
00B30 Festschriften
01A60 History of mathematics in the 20th century
01A70 Biographies, obituaries, personalia, bibliographies
03-03 History of mathematical logic and foundations
03B15 Higher-order logic; type theory (MSC2010)
03B35 Mechanization of proofs and logical operations
03B40 Combinatory logic and lambda calculus
03F05 Cut-elimination and normal-form theorems
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Biographic References:
Andrews, Peter B.