Abstract is missing.
- Mathematical Synthesis of Equational Deduction SystemsMarcelo P. Fiore, Chung-Kil Hur. 1-2 [doi]
- A Pronominal Approach to Binding and ComputationRobert Harper, Daniel R. Licata, Noam Zeilberger. 3-4 [doi]
- A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof IrrelevanceAndreas Abel, Thierry Coquand, Miguel Pagano. 5-19 [doi]
- Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM1Federico Aschieri, Stefano Berardi. 20-34 [doi]
- Syntax for Free: Representing Syntax with Binding Using ParametricityRobert Atkey. 35-49 [doi]
- On the Meaning of Logical CompletenessMichele Basaldella, Kazushige Terui. 50-64 [doi]
- Thick Subtrees, Games and ExperimentsPierre Boudes. 65-79 [doi]
- Bounded Linear Logic, RevisitedUgo Dal Lago, Martin Hofmann. 80-94 [doi]
- Partial Orders, Event Structures and Linear StrategiesClaudia Faggian, Mauro Piccolo. 95-111 [doi]
- Existential Type Systems with No Types in TermsKen-etsu Fujita, Aleksy Schubert. 112-126 [doi]
- Initial Algebra Semantics for Cyclic Sharing StructuresMakoto Hamana. 127-141 [doi]
- An Operational Account of Call-by-Value Minimal and Classical lambda-Calculus in Natural Deduction FormHugo Herbelin, Stéphane Zimmermann. 142-156 [doi]
- Refinement Types as Proof IrrelevanceWilliam Lovas, Frank Pfenning. 157-171 [doi]
- Weak omega-Categories from Intensional Type TheoryPeter LeFanu Lumsdaine. 172-187 [doi]
- Relating Classical Realizability and Negative Translation for Existential Witness ExtractionAlexandre Miquel. 188-202 [doi]
- Session-Based Communication Optimisation for Higher-Order Mobile ProcessesDimitris Mostrous, Nobuko Yoshida. 203-218 [doi]
- The Cut-Elimination Theorem for Differential Nets with PromotionMichele Pagani. 219-233 [doi]
- A Polymorphic Type System for the Lambda-Calculus with ConstructorsBarbara Petit. 234-248 [doi]
- Kripke Semantics for Martin-Löf s Extensional Type TheorySteven Awodey, Florian Rabe. 249-263 [doi]
- On the Values of Reducibility CandidatesColin Riba. 264-278 [doi]
- Lexicographic Path InductionJeffrey Sarnat, Carsten Schürmann. 279-293 [doi]
- Parametricity for Haskell with Imprecise Error SemanticsFlorian Stenger, Janis Voigtländer. 294-308 [doi]
- Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear LogicLutz Straßburger. 309-324 [doi]
- Algebraic Totality, towards CompletenessChristine Tasson. 325-340 [doi]
- A Logical Foundation for Environment ClassifiersTakeshi Tsukada, Atsushi Igarashi. 341-355 [doi]
- Inhabitation of Low-Rank Intersection TypesPawel Urzyczyn. 356-370 [doi]
- Differential Linear Logic and PolarizationLionel Vaux. 371-385 [doi]
- Complexity of Gödel s T in lambda-FormulationGunnar Wilken, Andreas Weiermann. 386-400 [doi]
- The Computational SLR: A Logic for Reasoning about Computational IndistinguishabilityYu Zhang. 401-415 [doi]