LEADER 05337nam 22007695 450 001 996465858003316 005 20230406065746.0 010 $a1-280-38300-3 010 $a9786613560919 010 $a3-642-02273-1 024 7 $a10.1007/978-3-642-02273-9 035 $a(CKB)1000000000754000 035 $a(SSID)ssj0000320540 035 $a(PQKBManifestationID)11237913 035 $a(PQKBTitleCode)TC0000320540 035 $a(PQKBWorkID)10248658 035 $a(PQKB)10221123 035 $a(DE-He213)978-3-642-02273-9 035 $a(MiAaPQ)EBC3064358 035 $a(PPN)136306691 035 $a(EXLCZ)991000000000754000 100 $a20100301d2009 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aTyped Lambda Calculi and Applications$b[electronic resource] $e9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009, Proceedings /$fedited by Pierre-Louis Curien 205 $a1st ed. 2009. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2009. 215 $a1 online resource (XIII, 417 p.) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v5608 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-642-02272-3 320 $aIncludes bibliographical references and index. 327 $aMathematical Synthesis of Equational Deduction Systems -- A Pronominal Approach to Binding and Computation -- A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance -- Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1 -- Syntax for Free: Representing Syntax with Binding Using Parametricity -- On the Meaning of Logical Completeness -- Thick Subtrees, Games and Experiments -- Bounded Linear Logic, Revisited -- Partial Orders, Event Structures and Linear Strategies -- Existential Type Systems with No Types in Terms -- Initial Algebra Semantics for Cyclic Sharing Structures -- An Operational Account of Call-by-Value Minimal and Classical ?-Calculus in ?Natural Deduction? Form -- Refinement Types as Proof Irrelevance -- Weak ?-Categories from Intensional Type Theory -- Relating Classical Realizability and Negative Translation for Existential Witness Extraction -- Session-Based Communication Optimisation for Higher-Order Mobile Processes -- The Cut-Elimination Theorem for Differential Nets with Promotion -- A Polymorphic Type System for the Lambda-Calculus with Constructors -- Kripke Semantics for Martin-Löf?s Extensional Type Theory -- On the Values of Reducibility Candidates -- Lexicographic Path Induction -- Parametricity for Haskell with Imprecise Error Semantics -- Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic -- Algebraic Totality, towards Completeness -- A Logical Foundation for Environment Classifiers -- Inhabitation of Low-Rank Intersection Types -- Differential Linear Logic and Polarization -- Complexity of Gödel?s T in ?-Formulation -- The Computational SLR: A Logic for Reasoning about Computational Indistinguishability. 330 $aThis book constitutes the refereed proceedings of the 9th International Conference on Typed Lambda Calculi and Applications, TLCA 2009, held in Brasilia, Brazil in July 2008 in conjunction with RTA 2007, the 19th International Conference on Rewriting Techniques and Applications as part of RDP 2009, the 5th International Conference on Rewriting, Deduction, and Programming. The 27 revised full papers presented together with 2 invited talks were carefully reviewed and selected from 53 submissions. The papers present original research results that are broadly relevant to the theory and applications of typed calculi and address a wide variety of topics such as proof-theory, semantics, implementation, types, and programming. 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v5608 606 $aMachine theory 606 $aComputer science?Mathematics 606 $aComputer science 606 $aArtificial intelligence 606 $aMathematical logic 606 $aFormal Languages and Automata Theory 606 $aMathematics of Computing 606 $aComputer Science Logic and Foundations of Programming 606 $aSymbolic and Algebraic Manipulation 606 $aArtificial Intelligence 606 $aMathematical Logic and Foundations 615 0$aMachine theory. 615 0$aComputer science?Mathematics. 615 0$aComputer science. 615 0$aArtificial intelligence. 615 0$aMathematical logic. 615 14$aFormal Languages and Automata Theory. 615 24$aMathematics of Computing. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aSymbolic and Algebraic Manipulation. 615 24$aArtificial Intelligence. 615 24$aMathematical Logic and Foundations. 676 $a005.131 702 $aCurien$b Pierre-Louis$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aInternational Conference on Typed Lambda Calculi and Applications 906 $aBOOK 912 $a996465858003316 996 $aTyped Lambda Calculi and Applications$9772124 997 $aUNISA