Electronic Notes in Theoretical Computer Science, Volume 132

Volume 132, Number 1, May 2005

• Jens Knoop, George C. Necula, Wolf Zimmermann:
  Preface. 1-3
  
• Sorin Lerner, Todd D. Millstein, Craig Chambers:
  Cobalt: A Language for Writing Provably-Sound Compiler Optimizations. 5-17
  
• Sabine Glesner, Simone Forster, Matthias Jäger:
  A Program Result Checker for the Lexical Analysis of the GNU C Compiler. 19-35
  
• Arnd Poetzsch-Heffter, Marek Gawkowski:
  Towards Proof Generating Compilers. 37-51
  
• Benjamin Goldberg, Lenore D. Zuck, Clark W. Barrett:
  Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers. 53-71
  
• Sabine Glesner:
  A Proof Calculus for Natural Semantics Based on Greatest Fixed Point Semantics. 73-93
  
• Karsten Klohs, Uwe Kastens:
  Memory Requirements of Java Bytecode Verification on Limited Devices. 95-111
  
• Elvira Albert, Germán Puebla, Manuel V. Hermenegildo:
  An Abstract Interpretation-based Approach to Mobile Code Safety. 113-129
  
• Sid Ahmed Ali Touati:
  On the Optimality of Register Saturation. 131-148