This special issue of Logical Methods in Computer Science contains extended and revised versions of selected papers from the Conference on Typed Lambda Calculi and Applications (TLCA '09), held in Brasilia, Brazil, on July 1-3, 2009. All submissions for this special issue underwent a new reviewing process, in accordance with the usual high standards of LMCS.

We think that together the papers of this volume cover a large range of active research directions within the field of lambda calculi and applications and illustrate the vitality of this area.

• The papers "Semantics of Typed Lambda-Calculus with Constructors" (by B. Petit) and "Derivation Lengths Classification of Gödel's T Extending Howard's Assignment" (by G. Wilken, A. Weiermann) study extensions of lambda calculus and their dynamic properties.
• The article "A Logical Foundation for Environment Classifiers" (by T. Tsukada and A. Igarashi) deals with the logical approach to the theory of multistage programming.
• Three papers then explore the area of type theory and logical frameworks, either from a syntactic or from a semantic point of view: "Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance" (by W. Lovas and F. Pfenning), "A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance" (by A. Abel, T. Coquand and M. Pagano), "Weak omega-categories from intensional type theory" (by P. Lumsdaine).
• The topic of categorical approaches to universal algebra is also addressed, with the papers "On the mathematical synthesis of equational logics" (by M. Fiore and C.-K. Hur) and "Initial Algebra Semantics for Cyclic Sharing Tree Structures" (by M. Hamana).
• Two papers deal with linear logic or game-interpretation of proofs: "Bounded Linear Logic, Revisited" (by U. Dal Lago and M. Hofmann), "On the meaning of logical completeness" (by M. Basaldella and K. Terui).
• Finally the topic of realizability is considered by four papers, with applications to the study of classical logic and to relative consistency results in set theory: "Existential witness extraction in classical realizability and via a negative translation" (by A. Miquel), "Interactive Learning-Based Realizability for Heyting Arithmetic with EM₁" (by F. Aschieri and S. Berardi), "Realizability algebras: a program to well order R", "Realizability algebras II : new models of ZF + DC" (by J.-L. Krivine).

We thank the authors for their contributions, the reviewers for their hard work, and the managing editor for special issues Benjamin Pierce for encouraging us to edit this volume.