+612 9045 4394
Typed Lambda Calculi and Applications : 4th International Conference, Tlca'99, l'Aquila, Italy, April 7-9, 1999, Proceedings - Jean-Yves Girard

Typed Lambda Calculi and Applications

4th International Conference, Tlca'99, l'Aquila, Italy, April 7-9, 1999, Proceedings

By: Jean-Yves Girard (Editor)


Published: 24th March 1999
Ships: 5 to 9 business days
5 to 9 business days
or 4 easy payments of $39.60 with Learn more

Thisvolumerepresents the proceedings ofthe Fourth International Conference onTypedLambdaCalculiandApplications, TLCA'99, heldinL'Aquila, on7-9 April1999. It contains25contributions. Fiftywere submitted, their overallqualitywas high, and selection was di?cult. The Programme Committee is very grateful toeveryonewhosubmittedapaper. Italsocontainstwopapersintroducingthe "demos"of"tlcasoftware,"i. e. industrialproductsmakinguseoftypedlamb- calculi. Thetutorialson - DenotationalsemanticsbyThomasEhrhardandJohnLongley, and - IntersectiontypesbyMarioCoppoandMariangiolaDezaniarenotincluded inthisvolume. Theeditor wishestothankthemembersoftheProgrammeCommitteeand theOrganizingCommitteelisted, fortheir hard work andsupport, witha s- cial mention for Benedetto Intrigila. He also thanks Corrado Boh ] m for kindly acceptingthe taskofdeliveringabanquetspeech. Theeditor alsoexpresses hisgratitude to allthereferees listed on the next page, as wellas tothose whowishnotto belisted fortheiressential assistance andtimegenerouslygiven. Marseille, January1999 Jean-YvesGirard ProgrammeCommittee S. Abramsky(Edinburgh) T. Coquand(Got ] eborg) J. -Y. Girard(Marseille)(Chair) R. Hindley(Swansea) J. -L. Krivine(Paris) J. Reynolds(Pittsburgh) S. Ronchi(Torino) A. Scedrov(Philadelphia) T. Streicher(Darmstadt) M. Takahashi(T^ oky^ o) P. Urzyczyn(Warszawa) OrganizingCommittee F. Corradini, A. Formisano, B. Intrigila, (Chair), M. -C. Meo, M. Nesi, A. Pierantonio, I. Salvo, S. Sorgi (Dip. Matematica, L'AquilaandDip. Informatica, LaSapienza, Roma) Referees Y. Akama T. Altenkirch F. Barbanera H. Barendregt O. Bastonero S. Berardi A. Berarducci C. Berline V. Bono M. Bugliesi F. Cardone G. Castagna I. Cervesato G. Chen R. Cockett A. Compagnoni M. Coppo T. Crolard P. -L. Curien V. Danos R. Davies P. DeGroote U. DeLiguoro M. Dezani R. Dickho? H. Geuvers N. Ghani P. Giannini S. Guerrini B. Harper R. Hasegawa H. Herbelin M. Hofmann K. Honda R. Jagadeesan T. Jim Y. Kameyama M. Kanovich R. Kashima Y. Kinoshita T. Kurata Y. Lafont J. Laird F. Lamarche P. B. Levy C. McBride M. Marz R. Matthes P. -A. Mellies G. Mitschke H. Nickau S. Nishizaki M. Parigot C. Paulin F. Pfenning B.

Invited demonstrations
The Coordination Language Facility and Applicationsp. 1
AnnoDomini in Practice: A Type-Theoretic Approach to the Year 2000 Problemp. 6
Modules in Non-commutative Logicp. 14
Elementary Complexity and Geometry of Interactionp. 25
Quantitative Semantics Revisitedp. 40
Total Functionals and Well-Founded Strategiesp. 54
Counting a Type's Principal Inhabitantsp. 69
Useless-Code Detection and Elimination for PCF with Algebraic Data typesp. 83
Every Unsolvable ¿ Term has a Decorationp. 98
Game Semantics for Untyped ¿ß¿-Calculusp. 114
A Finite Axiomatization of Inductive-Recursive Definitionsp. 129
Lambda Definability with Sums via Grothendieck Logical Relationsp. 147
Explicitly Typed ¿¿-Calculus for Polymorphism and Call-by-Valuep. 162
Soundness of the Logical Framework for Its Typed Operational Semanticsp. 177
Logical Predicates for Intuitionistic Linear Type Theoriesp. 198
Polarized Proof-Nets: Proof-Nets for LCp. 213
Call-by-Push-Value: A Subsuming Paradigmp. 228
A Study of Abramsky's Linear Chemical Abstract Machinep. 243
Resource Interpretations, Bunched Implications and the ¿¿-Calculusp. 258
A Curry-Howard Isomorphism for Compilation and Program Executionp. 280
Natural Deduction for Intuitionistic Non-commutative Linear Logicp. 295
A Logic for Abstract Data Types as Existential Typesp. 310
Characterising Explicit Substitutions which Preserve Terminationp. 325
Explicit Environmentsp. 340
Consequences of Jacopini's Theorem: Consistent Equalities and Equationsp. 355
Strong Normalisation of Cut-Elimination in Classical Logicp. 365
Pure Type Systems with Subtypingp. 381
Author Indexp. 397
Table of Contents provided by Publisher. All Rights Reserved.

ISBN: 9783540657637
ISBN-10: 3540657630
Series: Lecture Notes in Computer Science,
Audience: General
Format: Paperback
Language: English
Number Of Pages: 404
Published: 24th March 1999
Country of Publication: DE
Dimensions (cm): 23.39 x 15.6  x 2.13
Weight (kg): 0.58