Typed Lambda Calculi and Applications

Table of Contents

1. Altmetric Badge
   Book Overview
2. Altmetric Badge
   Chapter 1 Completeness Theorems and λ -Calculus
3. Altmetric Badge
   Chapter 2 A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code: Abstract
4. Altmetric Badge
   Chapter 3 Can Proofs Be Animated By Games?
5. Altmetric Badge
   Chapter 4 Untyped Algorithmic Equality for Martin-Löf’s Logical Framework with Surjective Pairs
6. Altmetric Badge
   Chapter 5 The Monadic Second Order Theory of Trees Given by Arbitrary Level-Two Recursion Schemes Is Decidable
7. Altmetric Badge
   Chapter 6 A Feasible Algorithm for Typing in Elementary Affine Logic
8. Altmetric Badge
   Chapter 7 Practical Inference for Type-Based Termination in a Polymorphic Setting
9. Altmetric Badge
   Chapter 8 Relational Reasoning in a Nominal Semantics for Storage
10. Altmetric Badge
    Chapter 9 Filters on CoInductive Streams, an Application to Eratosthenes’ Sieve
11. Altmetric Badge
    Chapter 10 Recursive Functions with Higher Order Domains
12. Altmetric Badge
    Chapter 11 Elementary Affine Logic and the Call-by-Value Lambda Calculus
13. Altmetric Badge
    Chapter 12 Rank-2 Intersection and Polymorphic Recursion
14. Altmetric Badge
    Chapter 13 Arithmetical Proofs of Strong Normalization Results for the Symmetric λμ -Calculus
15. Altmetric Badge
    Chapter 14 Subtyping Recursive Types Modulo Associative Commutative Products
16. Altmetric Badge
    Chapter 15 Galois Embedding from Polymorphic Types into Existential Types
17. Altmetric Badge
    Chapter 16 On the Degeneracy of Σ-Types in Presence of Computational Classical Logic
18. Altmetric Badge
    Chapter 17 Semantic Cut Elimination in the Intuitionistic Sequent Calculus
19. Altmetric Badge
    Chapter 18 The Elimination of Nesting in SPCF
20. Altmetric Badge
    Chapter 19 Naming Proofs in Classical Propositional Logic
21. Altmetric Badge
    Chapter 20 Reducibility and ⊤ ⊤-Lifting for Computation Types
22. Altmetric Badge
    Chapter 21 Privacy in Data Mining Using Formal Methods
23. Altmetric Badge
    Chapter 22 L 3 : A Linear Language with Locations
24. Altmetric Badge
    Chapter 23 Binding Signatures for Generic Contexts
25. Altmetric Badge
    Chapter 24 Proof Contexts with Late Binding
26. Altmetric Badge
    Chapter 25 The $\nabla$ -Calculus. Functional Programming with Higher-Order Encodings
27. Altmetric Badge
    Chapter 26 A Lambda Calculus for Quantum Computation with Classical Control
28. Altmetric Badge
    Chapter 27 Continuity and Discontinuity in Lambda Calculus
29. Altmetric Badge
    Chapter 28 Call-by-Name and Call-by-Value as Token-Passing Interaction Nets
30. Altmetric Badge
    Chapter 29 Avoiding Equivariance in Alpha-Prolog
31. Altmetric Badge
    Chapter 30 Higher-Order Abstract Non-interference