| 000 | 04853nam a22006015i 4500 | ||
|---|---|---|---|
| 001 | 978-3-642-02273-9 | ||
| 003 | DE-He213 | ||
| 005 | 20240730185659.0 | ||
| 007 | cr nn 008mamaa | ||
| 008 | 100301s2009 gw | s |||| 0|eng d | ||
| 020 |
_a9783642022739 _9978-3-642-02273-9 |
||
| 024 | 7 |
_a10.1007/978-3-642-02273-9 _2doi |
|
| 050 | 4 | _aQA267-268.5 | |
| 072 | 7 |
_aUYA _2bicssc |
|
| 072 | 7 |
_aCOM014000 _2bisacsh |
|
| 072 | 7 |
_aUYA _2thema |
|
| 082 | 0 | 4 |
_a005.131 _223 |
| 245 | 1 | 0 |
_aTyped Lambda Calculi and Applications _h[electronic resource] : _b9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009, Proceedings / _cedited by Pierre-Louis Curien. |
| 250 | _a1st ed. 2009. | ||
| 264 | 1 |
_aBerlin, Heidelberg : _bSpringer Berlin Heidelberg : _bImprint: Springer, _c2009. |
|
| 300 |
_aXIII, 417 p. _bonline resource. |
||
| 336 |
_atext _btxt _2rdacontent |
||
| 337 |
_acomputer _bc _2rdamedia |
||
| 338 |
_aonline resource _bcr _2rdacarrier |
||
| 347 |
_atext file _bPDF _2rda |
||
| 490 | 1 |
_aTheoretical Computer Science and General Issues, _x2512-2029 ; _v5608 |
|
| 505 | 0 | _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. | |
| 520 | _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. | ||
| 650 | 0 |
_aMachine theory. _9140245 |
|
| 650 | 0 |
_aComputer science _xMathematics. _93866 |
|
| 650 | 0 |
_aComputer science. _99832 |
|
| 650 | 0 |
_aArtificial intelligence. _93407 |
|
| 650 | 0 |
_aMathematical logic. _92258 |
|
| 650 | 1 | 4 |
_aFormal Languages and Automata Theory. _9140246 |
| 650 | 2 | 4 |
_aMathematics of Computing. _931875 |
| 650 | 2 | 4 |
_aComputer Science Logic and Foundations of Programming. _942203 |
| 650 | 2 | 4 |
_aSymbolic and Algebraic Manipulation. _955589 |
| 650 | 2 | 4 |
_aArtificial Intelligence. _93407 |
| 650 | 2 | 4 |
_aMathematical Logic and Foundations. _934712 |
| 700 | 1 |
_aCurien, Pierre-Louis. _eeditor. _4edt _4http://id.loc.gov/vocabulary/relators/edt _9140247 |
|
| 710 | 2 |
_aSpringerLink (Online service) _9140248 |
|
| 773 | 0 | _tSpringer Nature eBook | |
| 776 | 0 | 8 |
_iPrinted edition: _z9783642022722 |
| 776 | 0 | 8 |
_iPrinted edition: _z9783642022746 |
| 830 | 0 |
_aTheoretical Computer Science and General Issues, _x2512-2029 ; _v5608 _9140249 |
|
| 856 | 4 | 0 | _uhttps://doi.org/10.1007/978-3-642-02273-9 |
| 912 | _aZDB-2-SCS | ||
| 912 | _aZDB-2-SXCS | ||
| 912 | _aZDB-2-LNC | ||
| 942 | _cELN | ||
| 999 |
_c92946 _d92946 |
||