Typed lambda calculi and applications

InhaltsverzeichnisOn 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.