03777nam a22005655i 4500001001800000003000900018005001700027007001500044008004100059020001800100024003100118050001700149050001600166072001600182072001600198072002300214072002300237082001500260245022500275264006100500300003200561336002600593337002600619338003600645347002400681490005800705505069200763520101501455650002202470650005002492650001602542650002002558650002402578650002902602650002202631650005202653650004002705650004602745650004502791650003702836650004702873700003002920700003902950700003002989710003403019773002003053776003603073830005803109856004403167978-3-540-45504-2DE-He21320170515111530.0cr nn 008mamaa121227s2001 gw | s |||| 0|eng d a97835404550427 a10.1007/3-540-45504-32doi 4aQA76.7-76.73 4aQA76.76.C65 7aUMX2bicssc 7aUMC2bicssc 7aCOM0510102bisacsh 7aCOM0100002bisacsh04a005.1322310aProof Theory in Computer Scienceh[electronic resource] :bInternational Seminar, PTCS 2001 Dagstuhl Castle, Germany, October 7–12, 2001 Proceedings /cedited by Reinhard Kahle, Peter Schroeder-Heister, Robert Stärk. 1aBerlin, Heidelberg :bSpringer Berlin Heidelberg,c2001. aX, 246 p.bonline resource. atextbtxt2rdacontent acomputerbc2rdamedia aonline resourcebcr2rdacarrier atext filebPDF2rda1 aLecture Notes in Computer Science,x0302-9743 ;v21830 aLinear Ramified Higher Type Recursion and Parallel Complexity -- Reflective ?-Calculus -- A Note on the Proof-Theoretic Strength of a Single Application of the Schema of Identity -- Comparing the Complexity of Cut-Elimination Methods -- Program Extraction from Gentzen’s Proof of Transfinite Induction up to ?0 -- Coherent Bicartesian and Sesquicartesian Categories -- Indexed Induction-Recursion -- Modeling Meta-logical Features in a Calculus with Frozen Variables -- Proof Theory and Post-turing Analysis -- Interpolation for Natural Deduction with Generalized Eliminations -- Implicit Characterizations of Pspace -- Iterate logic -- Constructive Foundations for Featherweight Java. aProof theory has long been established as a basic discipline of mathematical logic. It has recently become increasingly relevant to computer science. The - ductive apparatus provided by proof theory has proved useful for metatheoretical purposes as well as for practical applications. Thus it seemed to us most natural to bring researchers together to assess both the role proof theory already plays in computer science and the role it might play in the future. The form of a Dagstuhl seminar is most suitable for purposes like this, as Schloß Dagstuhl provides a very convenient and stimulating environment to - scuss new ideas and developments. To accompany the conference with a proc- dings volume appeared to us equally appropriate. Such a volume not only ?xes basic results of the subject and makes them available to a broader audience, but also signals to the scienti?c community that Proof Theory in Computer Science (PTCS) is a major research branch within the wider ?eld of logic in computer science. 0aComputer science. 0aProgramming languages (Electronic computers). 0aAlgorithms. 0aComputer logic. 0aMathematical logic. 0aArtificial intelligence.14aComputer Science.24aProgramming Languages, Compilers, Interpreters.24aMathematical Logic and Foundations.24aArtificial Intelligence (incl. Robotics).24aMathematical Logic and Formal Languages.24aLogics and Meanings of Programs.24aAlgorithm Analysis and Problem Complexity.1 aKahle, Reinhard.eeditor.1 aSchroeder-Heister, Peter.eeditor.1 aStärk, Robert.eeditor.2 aSpringerLink (Online service)0 tSpringer eBooks08iPrinted edition:z9783540427520 0aLecture Notes in Computer Science,x0302-9743 ;v218340uhttp://dx.doi.org/10.1007/3-540-45504-3