Abstract is missing.
- On a Logical Foundation for Explicit SubstitutionsFrank Pfenning. 1 [doi]
- From Proof-Nets to Linear Logic Type Systems for Polynomial Time ComputingPatrick Baillot. 2-7 [doi]
- Strong Normalization and Equi-(Co)Inductive TypesAndreas Abel. 8-22 [doi]
- Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable MovesStefano Berardi. 23-38 [doi]
- The Safe Lambda CalculusWilliam Blum, C.-H. Luke Ong. 39-53 [doi]
- Intuitionistic Refinement CalculusSylvain Boulmé. 54-69 [doi]
- Computation by ProphecyAna Bove, Venanzio Capretta. 70-83 [doi]
- An Arithmetical Proof of the Strong Normalization for the ::::lambda:::: -Calculus with Recursive Equations on TypesRené David, Karim Nour. 84-101 [doi]
- Embedding Pure Type Systems in the Lambda-Pi-Calculus ModuloDenis Cousineau 0002, Gilles Dowek. 102-117 [doi]
- Completing Herbelin s ProgrammeJosé Espírito Santo. 118-132 [doi]
- Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent CalculiJosé Espírito Santo, Ralph Matthes, Luis Pinto. 133-147 [doi]
- Ludics is a Model for the Finitary Linear Pi-CalculusClaudia Faggian, Mauro Piccolo. 148-162 [doi]
- Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear LogicMarcelo P. Fiore. 163-177 [doi]
- The Omega Rule is P::1:::::1:::-Complete in the ::::lambdabeta:::: -CalculusBenedetto Intrigila, Richard Statman. 178-193 [doi]
- Weakly Distributive DomainsYing Jiang, Guo-Qiang Zhang. 194-206 [doi]
- Initial Algebra Semantics Is Enough!Patricia Johann, Neil Ghani. 207-222 [doi]
- A Substructural Type System for Delimited ContinuationsOleg Kiselyov, Chung-chieh Shan. 223-239 [doi]
- The Inhabitation Problem for Rank Two Intersection TypesDariusz Kusmierek. 240-254 [doi]
- Extensional Rewriting with SumsSam Lindley. 255-271 [doi]
- Higher-Order Logic Programming Languages with Constraints: A SemanticsJames Lipton, Susana Nieva. 272-289 [doi]
- Predicative Analysis of Feasibility and DiagonalizationJean-Yves Marion. 290-304 [doi]
- Edifices and Full Abstraction for the Symmetric Interaction CombinatorsDamiano Mazza. 305-320 [doi]
- Two Session Typing Systems for Higher-Order Mobile ProcessesDimitris Mostrous, Nobuko Yoshida. 321-335 [doi]
- An Isomorphism Between Cut-Elimination Procedure and Proof ReductionKoji Nakazawa. 336-350 [doi]
- Polynomial Size Analysis of First-Order FunctionsOlha Shkaravska, Ron van Kesteren, Marko C. J. D. van Eekelen. 351-365 [doi]
- Simple Saturated Sets for Disjunction and Second-Order Existential QuantificationMakoto Tatsuta. 366-380 [doi]
- Convolution [ (l)]m-CalculusLionel Vaux. 381-395 [doi]