CatarinaCoquand ChalmersUniversity,Sweden RadhiaCousot EcolePolytechnique,France OlivierDanvy UniversityofAarhus,Denmark AndrzejFilinski UniversityofAarhus,Denmark YoshihikoFutamura WasedaUniversity,Japan FritzHenglein ITUniversity,Denmark PeterLee CarnegieMellonUniversity,USA Y. AnnieLiu SUNYStonyBrook,USA DaveMacQueen BellLabs,USA JamesS. Royer SyracuseUniversity,USA MortenHeineSørensen ITPractice,Denmark CarolynL. Talcott StanfordUniversity,USA JonLWhite CommerceOne,Inc. ,USA Additional Referees ZinoBenaissa,EdoardoS. Biagioni,HowardA. Blair,CraigChambers,Wei- NganChin,LarsR. Clausen,PierreCointe,ThierryCoquand,NielsDamgaard, DanielDamian,DamienDoligez,R´emiDouence,R. KentDybvig,PavelEmel- nov,GilbertoFil´e,JohnGallagher,RobertoGiacobazzi,RobertGl¨ uck,John Hatcli?,NevinHeintze,ThomasHildebrandt,ZhenjiangHu,DieterHutter, KazuhikoKakehi,JerzyKarczmarczuk,AndyKing,NaokiKobayashi,Zenjiro Konishi,KimG. Larsen,MarioLatendresse,JuliaL. Lawall,MichaelLeuschel, JakobLichtenberg,FrancescoLogozzo,HenningMakholm,JacquesMalenfant, BrianMayoh,AntoineMin´e,TorbenÆ. Mogensen,EugenioMoggi,DavidM- niaux,PeterD. Mosses,JoachimNiehren,SusanOlder,AlbertoPettorossi, Franco ¸isPottier,MaurizioProietti,AarneRanta,JakobRehof,JohnReppy, Laurent R´ eveill`ere,MartinC. Rinard,Kristo?erH. Rose,AbhikRoychoudhury, LouisSalvail,Jo~aoSaraiva,DavidA. Schmidt,JensPeterSecher,MarioS¨udholt, S. DoaitseSwierstra,HaraldSøndergaard,ArnaudVenet,HongweiXi,ZheYang, Kwangkeun Yi. TableofContents InvitedOpeningTalk Program Analysis for Implicit Computational Complexity. 1 NeilD. Jones ContributedPapers Deriving Pre-conditions for Array Bound Check Elimination. 2 Wei-NganChin,Siau-ChengKhoo,DanaN. Xu Type Systems for Useless-Variable Elimination. 25 AdamFischbach,JohnHannan Boolean Constraints for Binding-Time Analysis. 39 KevinGlynn,PeterJ. Stuckey,MartinSulzmann,HaraldSøndergaard Constraint Abstractions. 63 J¨orgenGustavsson,JosefSvenningsson Implementing Circularity Using Partial Evaluation.