Pierre-Louis Curien
Proceedings of the Ninth International Conference on Typed Lambda Calculi and Applications
TLCA, 2009.

@proceedings{TLCA-2009,
	address       = "Brasilia, Brazil",
	doi           = "10.1007/978-3-642-02273-9",
	editor        = "Pierre-Louis Curien",
	isbn          = "978-3-642-02272-2",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Ninth International Conference on Typed Lambda Calculi and Applications}",
	volume        = 5608,
	year          = 2009,
}

Contents (29 items)

6 ×#logic
5 ×#type system
4 ×#linear
3 ×#proving
3 ×#semantics
2 ×#algebra
2 ×#deduction
2 ×#difference
2 ×#higher-order
2 ×#on the

TLCA-2009-FioreH #deduction #equation #synthesis

Mathematical Synthesis of Equational Deduction Systems (MPF, CKH), pp. 1–2.

TLCA-2009-HarperLZ #approach

A Pronominal Approach to Binding and Computation (RH, DRL, NZ), pp. 3–4.

TLCA-2009-AbelCP #algorithm #composition #proving #type system

A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance (AA, TC, MP), pp. 5–19.

TLCA-2009-AschieriB #interactive

Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM1 (FA, SB), pp. 20–34.

TLCA-2009-Atkey #for free #parametricity #representation #syntax #using

Syntax for Free: Representing Syntax with Binding Using Parametricity (RA), pp. 35–49.

TLCA-2009-BasaldellaT #logic #on the

On the Meaning of Logical Completeness (MB, KT), pp. 50–64.

TLCA-2009-Boudes #game studies

Thick Subtrees, Games and Experiments (PB), pp. 65–79.

TLCA-2009-LagoH #bound #linear #logic #revisited

Bounded Linear Logic, Revisited (UDL, MH), pp. 80–94.

TLCA-2009-FaggianP #linear #partial order

Partial Orders, Event Structures and Linear Strategies (CF, MP), pp. 95–111.

TLCA-2009-FujitaS #type system

Existential Type Systems with No Types in Terms (KeF, AS), pp. 112–126.

TLCA-2009-Hamana #algebra #semantics

Initial Algebra Semantics for Cyclic Sharing Structures (MH), pp. 127–141.

TLCA-2009-HerbelinZ #call-by #deduction #λ-calculus

An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form (HH, SZ), pp. 142–156.

TLCA-2009-LovasP #proving #refinement

Refinement Types as Proof Irrelevance (WL, FP), pp. 157–171.

TLCA-2009-Lumsdaine #type system

Weak ω-Categories from Intensional Type Theory (PLL), pp. 172–187.

TLCA-2009-Miquel

Relating Classical Realizability and Negative Translation for Existential Witness Extraction (AM), pp. 188–202.

TLCA-2009-MostrousY #communication #higher-order #mobile #optimisation #process

Session-Based Communication Optimisation for Higher-Order Mobile Processes (DM, NY), pp. 203–218.

TLCA-2009-Pagani #difference #theorem

The Cut-Elimination Theorem for Differential Nets with Promotion (MP), pp. 219–233.

TLCA-2009-Petit #polymorphism #type system #λ-calculus

A Polymorphic Type System for the λ-Calculus with Constructors (BP), pp. 234–248.

TLCA-2009-AwodeyR #semantics #type system

Kripke Semantics for Martin-Löf’s Extensional Type Theory (SA, FR), pp. 249–263.

TLCA-2009-Riba #on the

On the Values of Reducibility Candidates (CR), pp. 264–278.

TLCA-2009-SarnatS #induction

Lexicographic Path Induction (JS, CS), pp. 279–293.

TLCA-2009-StengerV #fault #haskell #parametricity #semantics

Parametricity for Haskell with Imprecise Error Semantics (FS, JV), pp. 294–308.

TLCA-2009-Strassburger #higher-order #linear #logic #multi #proving

Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic (LS), pp. 309–324.

TLCA-2009-Tasson #algebra #towards

Algebraic Totality, towards Completeness (CT), pp. 325–340.

TLCA-2009-TsukadaI #classification #logic

A Logical Foundation for Environment Classifiers (TT, AI), pp. 341–355.

TLCA-2009-Urzyczyn #rank

Inhabitation of Low-Rank Intersection Types (PU), pp. 356–370.

TLCA-2009-Vaux #difference #linear #logic

Differential Linear Logic and Polarization (LV), pp. 371–385.

TLCA-2009-WilkenW #complexity

Complexity of Gödel’s T in λ-Formulation (GW, AW), pp. 386–400.

TLCA-2009-Zhang #logic #reasoning

The Computational SLR: A Logic for Reasoning about Computational Indistinguishability (YZ), pp. 401–415.