Typed Lambda Calculi and Applications
Springer Berlin (Verlag)
978-3-540-73227-3 (ISBN)
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.
Erscheint lt. Verlag | 15.6.2007 |
---|---|
Reihe/Serie | Lecture Notes in Computer Science | Theoretical Computer Science and General Issues |
Zusatzinfo | X, 400 p. |
Verlagsort | Berlin |
Sprache | englisch |
Maße | 155 x 235 mm |
Gewicht | 635 g |
Themenwelt | Informatik ► Theorie / Studium ► Compilerbau |
Schlagworte | Categorical methods • Computational Logic • Deduction • formal methods • Hardcover, Softcover / Informatik, EDV/Informatik • HC/Informatik, EDV/Informatik • Higher-Order Logic • Lambda Calculus • Logic • Logical relations • Program Logics • programming • programming calculi • Programming language • Programming Theory • Program Semantics • Proof • Proof theory • Quantification • reduction • Rewriting • Semantics • sequent calculus • Type Systems |
ISBN-10 | 3-540-73227-6 / 3540732276 |
ISBN-13 | 978-3-540-73227-3 / 9783540732273 |
Zustand | Neuware |
Haben Sie eine Frage zum Produkt? |
aus dem Bereich