## 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)

- 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.

6 ×#logic

5 ×#type system

4 ×#linear

3 ×#proving

3 ×#semantics

2 ×#algebra

2 ×#deduction

2 ×#difference

2 ×#higher-order

2 ×#on the

5 ×#type system

4 ×#linear

3 ×#proving

3 ×#semantics

2 ×#algebra

2 ×#deduction

2 ×#difference

2 ×#higher-order

2 ×#on the