zbMATH — the first resource for mathematics

Typed lambda calculi and applications. 9th international conference, TLCA 2009, Brasilia, Brazil, July 1–3, 2009. Proceedings. (English) Zbl 1165.03001
Lecture Notes in Computer Science 5608. Berlin: Springer (ISBN 978-3-642-02272-2/pbk). xiii, 417 p. (2009).

Show indexed articles as search result.

The articles of this volume will be reviewed individually. The preceding conference has been reviewed (see Zbl 1120.03002).
Indexed articles:
Abel, Andreas; Coquand, Thierry; Pagano, Miguel, A modular type-checking algorithm for type theory with singleton types and proof irrelevance, 5-19 [Zbl 1246.03025]
Aschieri, Federico; Berardi, Stefano, Interactive learning-based realizability interpretation for Heyting arithmetic with \(\mathrm{EM}_1\), 20-34 [Zbl 1201.03051]
Atkey, Robert, Syntax for free: representing syntax with binding using parametricity, 35-49 [Zbl 1246.68084]
Basaldella, Michele; Terui, Kazushige, On the meaning of logical completeness, 50-64 [Zbl 1246.03076]
Boudes, Pierre, Thick subtrees, games and experiments, 65-79 [Zbl 1246.03077]
Dal Lago, Ugo; Hofmann, Martin, Bounded linear logic, revisited, 80-94 [Zbl 1211.03089]
Faggian, Claudia; Piccolo, Mauro, Partial orders, event structures and linear strategies, 95-111 [Zbl 1246.03078]
Fujita, Ken-etsu; Schubert, Aleksy, Existential type systems with no types in terms, 112-126 [Zbl 1246.03028]
Hamana, Makoto, Initial algebra semantics for cyclic sharing structures, 127-141 [Zbl 1246.68160]
Herbelin, Hugo; Zimmermann, Stéphane, An operational account of call-by-value minimal and classical \(\lambda \)-calculus in “natural deduction” form, 142-156 [Zbl 1246.03030]
Lovas, William; Pfenning, Frank, Refinement types as proof irrelevance, 157-171 [Zbl 1202.68107]
Lumsdaine, Peter LeFanu, Weak \(\omega \)-categories from intensional type theory, 172-187 [Zbl 1200.03050]
Miquel, Alexandre, Relating classical realizability and negative translation for existential witness extraction, 188-202 [Zbl 1218.03015]
Mostrous, Dimitris; Yoshida, Nobuko, Session-based communication optimisation for higher-order mobile processes, 203-218 [Zbl 1246.68069]
Pagani, Michele, The cut-elimination theorem for differential nets with promotion, 219-233 [Zbl 1246.03079]
Petit, Barbara, A polymorphic type system for the lambda-calculus with constructors, 234-248 [Zbl 1218.03018]
Awodey, Steve; Rabe, Florian, Kripke semantics for Martin-Löf’s extensional type theory, 249-263 [Zbl 1246.03022]
Riba, Colin, On the values of reducibility candidates, 264-278 [Zbl 1246.03031]
Sarnat, Jeffrey; Schürmann, Carsten, Lexicographic path induction, 279-293 [Zbl 1246.68078]
Stenger, Florian; Voigtländer, Janis, Parametricity for Haskell with imprecise error semantics, 294-308 [Zbl 1246.68087]
Straßburger, Lutz, Some observations on the proof theory of second order propositional multiplicative linear logic, 309-324 [Zbl 1246.03080]
Tasson, Christine, Algebraic totality, towards completeness, 325-340 [Zbl 1246.03081]
Tsukada, Takeshi; Igarashi, Atsushi, A logical foundation for environment classifiers, 341-355 [Zbl 1211.68064]
Urzyczyn, Paweł, Inhabitation of low-rank intersection types, 356-370 [Zbl 1246.03034]
Vaux, Lionel, Differential linear logic and polarization, 371-385 [Zbl 1246.03082]
Wilken, Gunnar; Weiermann, Andreas, Complexity of Gödel’s T in \(\lambda \)-formulation, 386-400 [Zbl 1238.03024]
Zhang, Yu, The computational SLR: a logic for reasoning about computational indistinguishability, 401-415 [Zbl 1246.94042]

03-06 Proceedings, conferences, collections, etc. pertaining to mathematical logic and foundations
68-06 Proceedings, conferences, collections, etc. pertaining to computer science
03B40 Combinatory logic and lambda calculus
68N18 Functional programming and lambda calculus
00B25 Proceedings of conferences of miscellaneous specific interest
Full Text: DOI arXiv