Typed lambda calculi and applications. 4th international conference, TLCA '99. L'Aquila, Italy, April 7--9, 1999. Proceedings (Q1284360)

The articles of mathematical interest will be reviewed individually. The preceding conference (2nd, 1995) has been announced (see Zbl 0813.68040). Indexed articles: \textit{Abrusci, V. Michele}, Modules in non-commutative logic, 14-24 [Zbl 0931.03068] \textit{Baillot, Patrick; Pedicini, Marco}, Elementary complexity and geometry of interaction. (Extended abstract), 25-39 [Zbl 0931.03045] \textit{Barreiro, Nuno; Ehrhard, Thomas}, Quantitative semantics revisited. (Extended abstract), 40-53 [Zbl 0931.03046] \textit{Berardi, Stefano; de'Liguoro, Ugo}, Total functionals and well-founded strategies. (Extended abstract), 54-68 [Zbl 0932.03014] \textit{Broda, Sabine; Damas, Luís}, Counting a type's principal inhabitants. (Extended abstract), 69-82 [Zbl 0932.03015] \textit{David, René}, Every unsolvable \(\lambda\) term has a decoration, 98-113 [Zbl 0931.03020] \textit{Di Gianantonio, Pietro; Franco, Gianluca; Honsell, Furio}, Game semantics for untyped \(\lambda\beta\eta\)-calculus, 114-128 [Zbl 0931.03021] \textit{Dybjer, Peter; Setzer, Anton}, A finite axiomatization of inductive-recursive definitions, 129-146 [Zbl 0931.03069] \textit{Fiore, Marcelo; Simpson, Alex}, Lambda definability with sums via Grothendieck logical relations, 147-161 [Zbl 0929.18004] \textit{Fujita, Ken-etsu}, Explicitly typed \(\lambda\mu\)-calculus for polymorphism and call-by-value, 162-176 [Zbl 0933.03009] \textit{Goguen, Healfdene}, Soundness of the logical framework for its typed operational semantics. Extended abstract, 177-197 [Zbl 0931.03023] \textit{Hasegawa, Masahito}, Logical predicates for intuitionistic linear type theories, 198-212 [Zbl 0931.03036] \textit{Laurent, Olivier}, Polarized proof-nets: Proof-nets for LC. (Extended abstract), 213-227 [Zbl 0933.03081] \textit{Mikami, Seikoh; Akama, Yohji}, A study of Abramsky's linear chemical abstract machine, 243-257 [Zbl 0931.03024] \textit{O'Hearn, Peter W.}, Resource interpretations, bunched implications and the \(\alpha\lambda\)-calculus. (Preliminary version), 258-279 [Zbl 0931.03025] \textit{Ohori, Atsushi}, A Curry-Howard isomorphism for compilation and program execution. (Extended abstract), 280-294 [Zbl 0932.03031] \textit{Polakow, Jeff; Pfenning, Frank}, Natural deduction for intuitionistic non-commutative linear logic, 295-309 [Zbl 0931.03071] \textit{Poll, Erik; Zwanenburg, Jan}, A logic for abstract data types as existential types, 310-324 [Zbl 0931.03026] \textit{Ritter, Eike}, Characterising explicit substitutions which preserve termination. (Extended abstract), 325-339 [Zbl 0931.03027] \textit{Sato, Masahiko; Sakurai, Takafumi; Burstall, Rod}, Explicit environments. (Extended abstract), 340-354 [Zbl 0931.03028] \textit{Statman, Rick}, Consequences of Jacopini's theorem: Consistent equalities and equations, 355-364 [Zbl 0931.03029] \textit{Urban, C.; Bierman, G. M.}, Strong normalisation of cut-elimination in classical logic, 365-380 [Zbl 0934.03074] \textit{Zwanenburg, Jan}, Pure type systems with subtyping. (Extended abstract), 381-396 [Zbl 0933.03033]