TY  - BOOK
AU  - Kahle,Reinhard
AU  - Schroeder-Heister,Peter Joseph
AU  - Stärk,Robert F.
ED  - PTCS 2001
TI  - Proof theory in computer science: international seminar, PTCS 2001, Dagstuhl Castle, Germany, October 7-12, 2001 : proceedings 
T2  - Lecture notes in computer science,
SN  - 9783540455042
AV  - QA76.9.A96 P753 2001
U1  - 004/.01/5113 21
PY  - 2001///
CY  - Berlin, New York
PB  - Springer
KW  - Automatic theorem proving
KW  - Congresses
KW  - Théorèmes
KW  - Démonstration automatique
KW  - Congrès
KW  - fast
KW  - proceedings (reports)
KW  - aat
KW  - Conference papers and proceedings
KW  - lcgft
KW  - Actes de congrès
KW  - rvmgf
N1  - Includes bibliographical references and index; Linear ramified higher type recursion and parallel complexity / Klaus Aehlig . [and others] -- Reflective [lambda]-calculus / Jesse Alt and Sergei Artemov -- A note on the proof-theoretic strength of a single application of the schema of identity / Matthias Baaz and Christian G. Fermuller -- Comparing the complexity of cut-elimination methods / Matthias Baaz and Alexander Leitsch -- Program extraction from Gentzen's proof of transfinite induction up to [epsilon]₀ / Ulrich Berger -- Coherent bicartesian and sesquicartesian categories / Kosta Dosen and Zoran Petric -- Indexed induction-recursion / Peter Dybjer and Anton Setzer -- Modeling meta-logical features in a calculus with frozen variables / Birgit Elbl -- Proof theory and post-turing analysis / Lew Gordeew -- Interpolation for natural deduction with generalized eliminations / Ralph Matthes -- Implicit characterizations of Pspace / Isabel Oitavem -- Iterate logic / Peter H. Schmitt -- Constructive foundations for featherweight Java / Thomas Studer
N2  - This book constitutes the refereed proceedings of the International Seminar on Proof Theory in Computer Science, PTCS 2001, held in Dagstuhl Castle, Germany, in October 2001. The 13 thoroughly revised full papers were carefully reviewed and selected for inclusion in the book. Among the topics addressed are higher type recursion, lambda calculus, complexity theory, transfinite induction, categories, induction-recursion, post-Turing analysis, natural deduction, implicit characterization, iterate logic, and Java programming
UR  - https://link.springer.com/10.1007/3-540-45504-3
ER  -