Typed Lambda Calculi and Applications [[electronic resource] ] : 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings / / edited by Simona Ronchi Della Rocca

• Record Nr.: UNISA996466266003316
• Pubbl/distr/stampa: Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007
• ISBN: 1-280-95552-X; 9786610955527; 3-540-73228-4
• Edizione: [1st ed. 2007.]
• Descrizione fisica: 1 online resource (404 p.)
• Collana: Theoretical Computer Science and General Issues, , 2512-2029 ; ; 4583
• Disciplina: 511.35
• Soggetti: Machine 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
• Lingua di pubblicazione: Inglese
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Note generali: Description based upon print version of record.
• Nota di bibliografia: Includes bibliographical references and index.
• Nota di contenuto: 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.