4. TLCA 1999: L'Aquila, Italy

@proceedings{DBLP:conf/tlca/1999,
  editor    = {Jean-Yves Girard},
  title     = {Typed Lambda Calculi and Applications, 4th International Conference,
               TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings},
  booktitle = {TLCA},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1581},
  year      = {1999},
  isbn      = {3-540-65763-0},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

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
  

Last update Fri May 25 08:43:12 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page