Proceedings of the Seventh International Conference on Typed Lambda Calculi and Applications
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter

Pawel Urzyczyn
Proceedings of the Seventh International Conference on Typed Lambda Calculi and Applications
TLCA, 2005.

FM
DBLP
Scholar
Full names Links ISxN
@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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.