## Pawel Urzyczyn

*Proceedings of the Seventh International Conference on Typed Lambda Calculi and Applications*

TLCA, 2005.

@proceedings{TLCA-2005, address = "Nara, Japan", editor = "Pawel Urzyczyn", isbn = "3-540-25593-1", publisher = "{Springer International Publishing}", series = "{Lecture Notes in Computer Science}", title = "{Proceedings of the Seventh International Conference on Typed Lambda Calculi and Applications}", volume = 3461, year = 2005, }

### Contents (30 items)

- TLCA-2005-Coquand #theorem #λ-calculus
- Completeness Theorems and λ-Calculus (TC), pp. 1–9.
- TLCA-2005-Felty #approach #semantics #tutorial
- A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code: Abstract (APF), p. 10.
- TLCA-2005-Hayashi #game studies #proving #question
- Can Proofs Be Animated By Games? (SH), pp. 11–22.
- TLCA-2005-AbelC #algorithm #framework #logic #similarity
- Untyped Algorithmic Equality for Martin-Löf’s Logical Framework with Surjective Pairs (AA, TC), pp. 23–38.
- TLCA-2005-AehligMO #decidability #higher-order #monad #recursion
- The Monadic Second Order Theory of Trees Given by Arbitrary Level-Two Recursion Schemes Is Decidable (KA, JGdM, CHLO), pp. 39–54.
- TLCA-2005-BaillotT #algorithm #logic #type system
- A Feasible Algorithm for Typing in Elementary Affine Logic (PB, KT), pp. 55–70.
- TLCA-2005-BartheGP #polymorphism #termination #type system
- Practical Inference for Type-Based Termination in a Polymorphic Setting (GB, BG, FP), pp. 71–85.
- TLCA-2005-BentonL #reasoning #relational #semantics
- Relational Reasoning in a Nominal Semantics for Storage (NB, BL), pp. 86–101.
- TLCA-2005-Bertot #induction
- Filters on CoInductive Streams, an Application to Eratosthenes’ Sieve (YB), pp. 102–115.
- TLCA-2005-BoveC #higher-order #recursion
- Recursive Functions with Higher Order Domains (AB, VC), pp. 116–130.
- TLCA-2005-CoppolaLR #call-by #logic #λ-calculus
- Elementary Affine Logic and the Call-by-Value λ Calculus (PC, UDL, SRDR), pp. 131–145.
- TLCA-2005-Damiani #polymorphism #recursion
- Rank-2 Intersection and Polymorphic Recursion (FD), pp. 146–161.
- TLCA-2005-DavidN #normalisation #proving #symmetry #λ-calculus #μ-calculus
- Arithmetical Proofs of Strong Normalization Results for the Symmetric λμ-Calculus (RD, KN), pp. 162–178.
- TLCA-2005-CosmoPR #commutative #recursion #type system
- Subtyping Recursive Types Modulo Associative Commutative Products (RDC, FP, DR), pp. 179–193.
- TLCA-2005-Fujita #polymorphism
- Galois Embedding from Polymorphic Types into Existential Types (KeF), pp. 194–208.
- TLCA-2005-Herbelin #logic #on the
- On the Degeneracy of Σ-Types in Presence of Computational Classical Logic (HH), pp. 209–220.
- TLCA-2005-Hermant #calculus #semantics
- Semantic Cut Elimination in the Intuitionistic Sequent Calculus (OH), pp. 221–233.
- TLCA-2005-Laird
- The Elimination of Nesting in SPCF (JL), pp. 234–245.
- TLCA-2005-LamarcheS #logic #proving
- Naming Proofs in Classical Propositional Logic (FL, LS), pp. 246–261.
- TLCA-2005-LindleyS
- Reducibility and TT-Lifting for Computation Types (SL, IS), pp. 262–277.
- TLCA-2005-MatwinFHC #data mining #formal method #mining #privacy #using
- Privacy in Data Mining Using Formal Methods (SM, APF, ITH, VC), pp. 278–292.
- TLCA-2005-MorrisettAF #linear #named
- L3: A Linear Language with Locations (GM, AJA, MF), pp. 293–307.
- TLCA-2005-PowerT
- Binding Signatures for Generic Contexts (JP, MT), pp. 308–323.
- TLCA-2005-PrevostoB #proving
- Proof Contexts with Late Binding (VP, SB), pp. 324–338.
- TLCA-2005-SchurmannPS #calculus #encoding #functional #higher-order #programming
- The [triangle]-Calculus. Functional Programming with Higher-Order Encodings (CS, AP, JS), pp. 339–353.
- TLCA-2005-SelingerV #quantum #λ-calculus
- A λ Calculus for Quantum Computation with Classical Control (PS, BV), pp. 354–368.
- TLCA-2005-SeveriV #λ-calculus
- Continuity and Discontinuity in λ Calculus (PS, FJdV), pp. 369–385.
- TLCA-2005-Sinot #call-by #interactive
- Call-by-Name and Call-by-Value as Token-Passing Interaction Nets (FRS), pp. 386–400.
- TLCA-2005-UrbanC #prolog
- Avoiding Equivariance in αProlog (CU, JC), pp. 401–416.
- TLCA-2005-Zanardini #higher-order
- Higher-Order Abstract Non-interference (DZ), pp. 417–432.

5 ×#logic

5 ×#λ-calculus

4 ×#higher-order

4 ×#proving

4 ×#recursion

3 ×#polymorphism

3 ×#semantics

3 ×#type system

2 ×#algorithm

2 ×#calculus

5 ×#λ-calculus

4 ×#higher-order

4 ×#proving

4 ×#recursion

3 ×#polymorphism

3 ×#semantics

3 ×#type system

2 ×#algorithm

2 ×#calculus