Theoretical Computer Science Logic, semantics and theory of programming Volume 212, Numbers 1-2, 6 February 1999 Gentzen Guest Editors: C. Bohm 1. Guessarian Abstracted/Indexed in: ACM Computing Reviews, Compuscience, Computer Abstracts, Current Contents: Engineering, Technology & Applied Science, Engineering Index/Com- pendex, INSPEC Information Services, Mathematical Reviews, Zentralblatt fur Mathematik Contents Foreword C. Bohm and |. Guessarian Contributions M. Benke Some complexity bounds for subtype inequalities A. Berarducci and M. Dezani-Ciancaglini Infinite A-calculus and types H. Boley Functional-logic integration via minimal reciprocal extensions V. Bono and M. Bugliesi Matching for the lambda calculus of objects R. Dyckhoff and L. Pinto Permutability of proofs in intuitionistic sequent calculi M. Emms and H. Leib Extending the type checker of Standard ML by polymorphic recursion F. Honsell and M. Lenisa Semantical analysis of perpetual strategies in A-calculus B. Intrigila and M. Venturini Zilli Orders, reduction graphs and spectra A. Piperno An algebraic view of the B6hm-out technique H. Schwichtenberg Termination of permutative conversions in intuitionistic Gentzen calculi D. Spreen On functions preserving levels of approximation: A refined model construction for various lambda calculi Contents EATCS Bulletin Number 66 Author index volume 212