![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
4th TLCA 1999: L'Aquila, Italy
- Jean-Yves Girard:
Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings. Lecture Notes in Computer Science 1581, Springer 1999, ISBN 3-540-65763-0
Invited demonstrations
- Jean-Marc Andreoli:
The Coordination Language Facility and Applications. 1-5 - Peter Harry Eidorff, Fritz Henglein, Christian Mossin, Henning Niss, Morten Heine Sørensen, Mads Tofte:
AnnoDomini in Practice: A Type-Theoretic Approach to the Year 2000 Problem. 6-13
Contributions
- V. Michele Abrusci:
Modules in Non-communicative Logic. 14-24 - Patrick Baillot, Marco Pedicini
:
Elementary Complexity and Geometry of Interaction. 25-39 - Nuno Barreiro, Thomas Ehrhard:
Quantitative Semantics Revisited. 40-53 - Stefano Berardi, Ugo de'Liguoro:
Total Functionals and Well-Founded Strategies. 54-68 - Sabine Broda
, Luís Damas:
Counting a Type's Principal Inhabitants. 69-82 - Ferruccio Damiani:
Useless-Code Detection and Elimination for PCF with Algebraic Data types. 83-97 - René David:
Every Unsolvable lambda Term has a Decoration. 98-113 - Pietro Di Gianantonio, Gianluca Franco, Furio Honsell:
Game Semantics for Untyped lambda beta eta-Calculus. 114-128 - Peter Dybjer, Anton Setzer:
A Finite Axiomatization of Inductive-Recursive Definitions. 129-146 - Marcelo P. Fiore, Alex K. Simpson:
Lambda Definability with Sums via Grothendieck Logical Relations. 147-161 - Ken-etsu Fujita:
Explicitly Typed lambda µ-Calculus for Polymorphism an Call-by-Value. 162-176 - Healfdene Goguen:
Soundness of the Logical Framework for Its Typed Operational Semantics. 177-197 - Masahito Hasegawa:
Logical Predicates for Intuitionistic Linear Type Theories. 198-212 - Olivier Laurent:
Polarized Proof-Nets: Proof-Nets for LC. 213-227 - Paul Blain Levy:
Call-by-Push-Value: A Subsuming Paradigm. 228-242 - Seikoh Mikami, Yohji Akama
:
A Study of Abramsky's Linear Chemical Abstract Machine. 243-257 - Peter W. O'Hearn:
Resource Interpretations, Bunched Implications and the alpha lambda-Calculus. 258-279 - Atsushi Ohori:
A Curry-Howard Isomorphism for Compilation and Program Execution. 280-294 - Jeff Polakow, Frank Pfenning:
Natural Deduction for Intuitionistic Non-communicative Linear Logic. 295-309 - Erik Poll, Jan Zwanenburg:
A Logic for Abstract Data Types as Existential Types. 310-324 - Eike Ritter:
Characterising Explicit Substitutions which Preserve Termination. 325-339 - Masahiko Sato, Takafumi Sakurai, Rod M. Burstall:
Explicit Environments. 340-354 - Richard Statman:
Consequences of Jacopini's Theorem: Consistent Equalities and Equations. 355-364 - Christian Urban, Gavin M. Bierman:
Strong Normalisation of Cut-Elimination in Classical Logic. 365-380 - Jan Zwanenburg:
Pure Type Systems with Subtyping. 381-396
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.