LEADER 04237nam  22007575  450 
001 996466266003316
005 20230221145336.0
010   $a1-280-95552-X
010   $a9786610955527
010   $a3-540-73228-4
024 7 $a10.1007/978-3-540-73228-0
035   $a(CKB)1000000000478510
035   $a(EBL)3037318
035   $a(SSID)ssj0000263306
035   $a(PQKBManifestationID)11225342
035   $a(PQKBTitleCode)TC0000263306
035   $a(PQKBWorkID)10272744
035   $a(PQKB)11007022
035   $a(DE-He213)978-3-540-73228-0
035   $a(MiAaPQ)EBC3037318
035   $a(MiAaPQ)EBC6706829
035   $a(Au-PeEL)EBL6706829
035   $a(PPN)123728061
035   $a(EXLCZ)991000000000478510
100   $a20100301d2007      u|             0
101 0 $aeng
135   $aur|n|---|||||
181   $ctxt
182   $cc
183   $acr
200 10$aTyped Lambda Calculi and Applications$b[electronic resource] $e8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings /$fedited by Simona Ronchi Della Rocca
205   $a1st ed. 2007.
210  1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2007.
215   $a1 online resource (404 p.)
225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v4583
300   $aDescription based upon print version of record.
311   $a3-540-73227-6 
320   $aIncludes bibliographical references and index.
327   $aOn 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.
410  0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v4583
606   $aMachine theory
606   $aComputer science
606   $aComputer programming
606   $aCompilers (Computer programs)
606   $aFormal Languages and Automata Theory
606   $aComputer Science Logic and Foundations of Programming
606   $aProgramming Techniques
606   $aCompilers and Interpreters
615  0$aMachine theory.
615  0$aComputer science.
615  0$aComputer programming.
615  0$aCompilers (Computer programs).
615 14$aFormal Languages and Automata Theory.
615 24$aComputer Science Logic and Foundations of Programming.
615 24$aProgramming Techniques.
615 24$aCompilers and Interpreters.
676   $a511.35
702   $aRonchi Della Rocca$b S$g(Simona),
712 12$aInternational Conference on Typed Lambda Calculi and Applications
801  0$bMiAaPQ
801  1$bMiAaPQ
801  2$bMiAaPQ
906   $aBOOK
912   $a996466266003316
996   $aTyped Lambda Calculi and Applications$9772124
997   $aUNISA