SPECIAL ISSUE:
Selected Papers of the Conference "Typed Lambda Calculi and Applications 2009"
Brasilia, Brazil, 2009

Preface Pierre-Louis Curien, Patrick Baillot, Luca Paolini


Initial Algebra Semantics for Cyclic Sharing Tree Structures
Makoto Hamana


Interactive Learning-Based Realizability for Heyting Arithmetic with EM_₁
Federico Aschieri and Stefano Berardi


Weak omega-categories from intensional type theory
Peter LeFa Lumsdaine


Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance
William Lovas and Frank Pfenning


Bounded Linear Logic, Revisited
Ugo Dal Lago and Martin Hofmann


A Logical Foundation for Environment Classifiers
Takeshi Tsukada and Atsushi Igarashi


On the meaning of logical completeness
Michele Basaldella and Kazushige Terui


Semantics of Typed Lambda-Calculus with Constructors
Barbara Petit


Existential witness extraction in classical realizability and via a negative translation
Alexandre Miquel


A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
Andreas Abel, Thierry Coquand and Miguel Pagano


Realizability algebras: a program to well order R
Jean-Louis Krivine


On the mathematical synthesis of equational logics
Marcelo Fiore and Chung-Kil Hur


Realizability algebras II : new models of ZF + DC
Jean-Louis Krivine


Derivation Lengths Classification of Gödel's T Extending Howard's Assignment
Gunnar Wilken and Andreas Weiermann

DOI: 10.2168/LMCS-TCLA:2009