Typed Lambda Calculi and Applications: 6th International Conference, TLCA 2003, Valencia, Spain, June 10-12, 2003, Proceedings (Lecture Notes in Computer Science)

This book constitutes the refereed proceedings of the 6th International Conference on Typed Lambda Calculi and Applications, TLCA 2003, held in Valencia, Spain in June 2003. The 21 revised full papers presented were carefully reviewed and selected from 40 submissions. The volume reports research results on all current aspects of typed lambda calculi, ranging from theoretical and methodological issues to the application of proof assistants. This volume represents the proceedings of the 6th International Conference on Typed Lambda Calculi and Applications, TLCA 2003, held in Valencia, Spain on 10–12 June 2003 in conjunction with CADE and RTA. It contains 21 c- tributions which were selected from 40 submissions. Three invited talks by D. McAllester, G. Gonthier, and R. Loader are not included in this volume. The editor wishes to thank the members of the Program Committee and the referees for their help in putting together a very attractive program. April 2003 Martin Hofmann Program Committee A. Asperti J. Palsberg (University of Bologna) (Purdue University) T. Coquand H. Schwichtenberg (Chalmers University, G ̈ oteborg) (University of Munich) V. Danos N. Shankar (University Paris VII) (SRI International, Menlo Park) M. Hofmann P. Urzyczyn (Chair, University of Munich) (Warsaw University) P. -A. Mellies (CNRS, Paris) Steering Committee S. Abramsky H. Barendregt (Chair, Oxford University) (University of Nijmegen) M. Dezani-Ciancaglini R. Hindley (University of Torino) (University of Swansea) VI Preface Referees A. Abel T. Altenkirch A. Asperti P. Baillot G. Barthe M. Benke N. Benton U. Berger J. Chrzaszcz A. Compagnoni T. Coquand R. di Cosmo P. -L. Curien V. Danos R. Dyckho? T. Ehrhard C. Faggian C. Fuehrmann H. Geuvers J. Goubault P. de Groote R. Hasegawa H. Herbelin M. Hofmann G. Hutton B. Jay F. Joachimski J. B. Joinet A. J. Kfoury U. Dal Lago F. Lamarche H. Leiss T. Loew J. Longley P. Manoury S. Martini R. Matthes M. Mauny J. Termination and Productivity Checking with Continuous Types....Pages 1-15 Derivatives of Containers....Pages 16-30 Max-Plus Quasi-interpretations....Pages 31-45 Inductive Types in the Calculus of Algebraic Constructions....Pages 46-59 On Strong Normalization in the Intersection Type Discipline....Pages 60-74 Relative Definability and Models of Unary PCF....Pages 75-89 Principal Typing in Elementary Affine Logic....Pages 90-104 A Logical Framework with Dependently Typed Records....Pages 105-119 A Sound and Complete CPS-Translation for λμ-Calculus....Pages 120-134 Abstraction Barrier-Observing Relational Parametricity....Pages 135-152 Encoding of the Halting Problem into the Monster Type and Applications....Pages 153-166 Well-Going Programs Can Be Typed....Pages 167-179 Parameterizations and Fixed-Point Operators on Control Categories....Pages 180-194 Functional In-Place Update with Layered Datatype Sharing....Pages 195-210 A Fully Abstract Bidomain Model of Unary FPC....Pages 211-225 On a Semantic Definition of Data Independence....Pages 226-240 Nondeterministic Light Logics and NP-Time....Pages 241-255 Polarized Proof Nets with Cycles and Fixpoints Semantics....Pages 256-270 Observational Equivalence and Program Extraction in the Coq Proof Assistant....Pages 271-285 Permutative Conversions in Intuitionistic Multiary Sequent Calculi with Cuts....Pages 286-300 A Universal Embedding for the Higher Order Structure of Computational Effects....Pages 301-315