Typed lambda calculi and applications. 5th international conference, TLCA 2001, Kraków, Poland, May 2--5, 2001. Proceedings (Q5933584)

The articles of this volume will be reviewed individually. The preceding conference (4th, 1999) has been reviewed (see Zbl 0911.00022). Indexed articles: \textit{Danvy, Olivier}, Many happy returns, 1 [Zbl 0981.68619] \textit{Normann, Dag}, Definability of total objects in PCF and related calculi, 4-5 [Zbl 0981.68585] \textit{Altenkirch, Thorsten}, Representations of first order function types as terminal coalgebras, 8-21 [Zbl 0981.68110] \textit{Altenkirch, Thorsten; Coquand, Thierry}, A finitary subsystem of the polymorphic \(\lambda\)-calculus, 22-28 [Zbl 0981.03020] \textit{Berger, Martin; Honda, Kohei; Yoshida, Nobuko}, Sequentiality and the \(\pi\)-calculus, 29-45 [Zbl 0981.68037] \textit{Cardelli, Luca; Gordon, Andrew D.}, Logical properties of name restriction, 46-60 [Zbl 0981.68036] \textit{Chroboczek, Juliusz}, Subtyping recusive games, 61-75 [Zbl 1024.68018] \textit{Coppola, Paolo; Martini, Simone}, Typing lambda terms in elementary logic with linear constraints, 76-90 [Zbl 0981.03028] \textit{Danner, Norman}, Ramified recurrence with dependent types, 91-105 [Zbl 1002.03038] \textit{Di Gianantonio, Pietro}, Game semantics for the pure lazy \(\lambda\)-calculus, 106-120 [Zbl 0981.03022] \textit{Dougherty, Dan; Lescanne, Pierre}, Reductions, intersection types, and explicit substitutions, 121-135 [Zbl 0981.68024] \textit{Dowek, Gilles}, The Stratified Foundations as a theory modulo, 136-150 [Zbl 1002.03042] \textit{Filinski, Andrzej}, Normalization by evaluation for the computational lambda-calculus, 151-165 [Zbl 0981.68023] \textit{Geuvers, Herman}, Induction is not derivable in second order dependent type theory, 166-181 [Zbl 0981.03023] \textit{de Groote, Philippe}, Strong normalization of classical natural deduction with disjunction, 182-196 [Zbl 0981.03027] \textit{Haghverdi, Esfandiar}, Partially additive categories and fully complete models of linear logic, 197-216 [Zbl 0981.03065] \textit{Jay, C. Barry}, Distinguishing data structures and functions: the constructor calculus and functorial types, 217-239 [Zbl 0981.68027] \textit{Joly, Thierry}, The finitely generated types of the \(\lambda\)-calculus, 240-252 [Zbl 1002.03014] \textit{Knapik, Teodor; Niwinski, Damian; Urzyczyn, Paweł}, Deciding monadic theories of hyperalgebraic trees, 253-267 [Zbl 0981.03012] \textit{Laird, James}, A deconstruction of non-deterministic classical cut elimination, 268-282 [Zbl 0981.03057] \textit{Laurent, Olivier}, A token machine for full geometry of interaction. Extended abstract, 283-297 [Zbl 0981.03515] \textit{Leiß, Hans}, Second-order pre-logical relations and representation independence, 298-314 [Zbl 0981.03026] \textit{de'Liguoro, Ugo}, Characterizing convergent terms in object calculi via intersection types, 315-328 [Zbl 0981.03021] \textit{Matthes, Ralph}, Parigot's second order \(\lambda\mu\)-calculus and inductive types, 329-343 [Zbl 0981.03024] \textit{Miquel, Alexandre}, The implicit calculus of constructions. extending pure type systems with an intersection type binder and subtyping, 344-359 [Zbl 0981.03029] \textit{Murawski, Andrzej S.; Ong, C.-H. Luke}, Evolving games and essential nets for affine polymorphism, 360-375 [Zbl 0981.03064] \textit{Padovani, Vincent}, Retracts in simple types, 376-384 [Zbl 0981.03025] \textit{Pinto, Jorge Sousa}, Parallel implementation models for the \(\lambda\)-calculus using the geometry of interaction. Extended abstract, 385-399 [Zbl 0981.68500] \textit{Schubert, Aleksy}, The complexity of \(\beta\)-reduction in low orders, 400-414 [Zbl 0981.68025] \textit{Urban, Christian}, Strong normalisation for a Gentzen-like cut-elimination procedure, 415-429 [Zbl 0981.03058]