04237nam 22007575 450 99646626600331620230221145336.01-280-95552-X97866109555273-540-73228-410.1007/978-3-540-73228-0(CKB)1000000000478510(EBL)3037318(SSID)ssj0000263306(PQKBManifestationID)11225342(PQKBTitleCode)TC0000263306(PQKBWorkID)10272744(PQKB)11007022(DE-He213)978-3-540-73228-0(MiAaPQ)EBC3037318(MiAaPQ)EBC6706829(Au-PeEL)EBL6706829(PPN)123728061(EXLCZ)99100000000047851020100301d2007 u| 0engur|n|---|||||txtccrTyped Lambda Calculi and Applications[electronic resource] 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings /edited by Simona Ronchi Della Rocca1st ed. 2007.Berlin, Heidelberg :Springer Berlin Heidelberg :Imprint: Springer,2007.1 online resource (404 p.)Theoretical Computer Science and General Issues,2512-2029 ;4583Description based upon print version of record.3-540-73227-6 Includes bibliographical references and index.On a Logical Foundation for Explicit Substitutions -- From Proof-Nets to Linear Logic Type Systems for Polynomial Time Computing -- Strong Normalization and Equi-(Co)Inductive Types -- Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable Moves -- The Safe Lambda Calculus -- Intuitionistic Refinement Calculus -- Computation by Prophecy -- An Arithmetical Proof of the Strong Normalization for the ?-Calculus with Recursive Equations on Types -- Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo -- Completing Herbelin’s Programme -- Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi -- Ludics is a Model for the Finitary Linear Pi-Calculus -- Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic -- The Omega Rule is -Complete in the ??-Calculus -- Weakly Distributive Domains -- Initial Algebra Semantics Is Enough! -- A Substructural Type System for Delimited Continuations -- The Inhabitation Problem for Rank Two Intersection Types -- Extensional Rewriting with Sums -- Higher-Order Logic Programming Languages with Constraints: A Semantics -- Predicative Analysis of Feasibility and Diagonalization -- Edifices and Full Abstraction for the Symmetric Interaction Combinators -- Two Session Typing Systems for Higher-Order Mobile Processes -- An Isomorphism Between Cut-Elimination Procedure and Proof Reduction -- Polynomial Size Analysis of First-Order Functions -- Simple Saturated Sets for Disjunction and Second-Order Existential Quantification -- Convolution -Calculus.Theoretical Computer Science and General Issues,2512-2029 ;4583Machine theoryComputer scienceComputer programmingCompilers (Computer programs)Formal Languages and Automata TheoryComputer Science Logic and Foundations of ProgrammingProgramming TechniquesCompilers and InterpretersMachine theory.Computer science.Computer programming.Compilers (Computer programs).Formal Languages and Automata Theory.Computer Science Logic and Foundations of Programming.Programming Techniques.Compilers and Interpreters.511.35Ronchi Della Rocca S(Simona),International Conference on Typed Lambda Calculi and ApplicationsMiAaPQMiAaPQMiAaPQBOOK996466266003316Typed Lambda Calculi and Applications772124UNISA00919nam0-22003011i-450 99000481378040332120241211120955.0000481378FED01000481378(Aleph)000481378FED0119990604d1981----km-y0itay50------baitaITa-------001yyViaggio nell'italiano popolarestrumenti per l'educazione linguisticaEdgardo Tito SaronneBolognaIl Mulinoc1981232 p.ill.22 cmStudi e ricerche133Lingua italianaInsegnamento agli adulti450.7Saronne,Edgardo Tito<1936- >192276ITUNINA20050221RICAUNIMARCBK990004813780403321458 SARO 02Ist.f.m.34244FLFBCFLFBCViaggio nell'italiano popolare150540UNINA