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)

5 ×#logic
5 ×#λ-calculus
4 ×#higher-order
4 ×#proving
4 ×#recursion
3 ×#polymorphism
3 ×#semantics
3 ×#type system
2 ×#algorithm
2 ×#calculus

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.