Typed Lambda Calculi and Applications

Completeness Theorems and ?-Calculus.- Completeness Theorems and ?-Calculus.- A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code: Abstract.- Can Proofs Be Animated By Games?.- Contributed Papers.- Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs.- The Monadic Second Order Theory of Trees Given by Arbitrary Level-Two Recursion Schemes Is Decidable.- A Feasible Algorithm for Typing in Elementary Affine Logic.- Practical Inference for Type-Based Termination in a Polymorphic Setting.- Relational Reasoning in a Nominal Semantics for Storage.- Filters on CoInductive Streams, an Application to Eratosthenes' Sieve.- Recursive Functions with Higher Order Domains.- Elementary Affine Logic and the Call-by-Value Lambda Calculus.- Rank-2 Intersection and Polymorphic Recursion.- Arithmetical Proofs of Strong Normalization Results for the Symmetric ??-Calculus.- Subtyping Recursive Types Modulo Associative Commutative Products.- Galois Embedding from Polymorphic Types into Existential Types.- On the Degeneracy of ?-Types in Presence of Computational Classical Logic.- Semantic Cut Elimination in the Intuitionistic Sequent Calculus.- The Elimination of Nesting in SPCF.- Naming Proofs in Classical Propositional Logic.- Reducibility and ???-Lifting for Computation Types.- Privacy in Data Mining Using Formal Methods.- L3: A Linear Language with Locations.- Binding Signatures for Generic Contexts.- Proof Contexts with Late Binding.- The -Calculus. Functional Programming with Higher-Order Encodings.- A Lambda Calculus for Quantum Computation with Classical Control.- Continuity and Discontinuity in Lambda Calculus.- Call-by-Name and Call-by-Value as Token-Passing Interaction Nets.- Avoiding Equivariance inAlpha-Prolog.- Higher-Order Abstract Non-interference.