POPL 2004 program

Registration will take place Tuesday, January 13th from 17.30 to 19.30, and Wednesday, January 14th from 8.00 to 9.00.

Wednesday, January 14th

Coinductive Techniques in Programming Languages: Davide Sangiorgi (University of Bologna).

Symbolic Transfer Function-based Approaches to Certified Compilation: Xavier Rival (École Normale Supérieure)
Simple Relational Correctness Proofs for Static Analyses and Program Transformations: Nick Benton (Microsoft Research)
Incremental Execution of Transformation Specifications: Ganesh Sittampalam, Oege de Moor (Oxford University), and Ken Friis Larsen (IT University of Copenhagen).
Formalization of Generics for the .NET Common Language Runtime: Dachuan Yu (Yale University), Andrew Kennedy, and Don Syme (Microsoft Research).

Semantic Types: A Fresh Look at the Ideal Model for Types: Jérôme Vouillon and Paul-André Melliès (CNRS, University Paris 7).
Extensional Normalisation and Type-Directed Partial Evaluation for Typed Lambda Calculus with Sums: Vincent Balat (University Paris 7), Roberto Di Cosmo (University Paris 7 and INRIA Rocquencourt), Marcelo Fiore (Cambridge University).
Isomorphisms of Generic Recursive Polynomial Types: Marcelo Fiore (Cambridge University).

Polymorphic Typed Defunctionalization: François Pottier and Nadji Gauthier (INRIA Rocquencourt).
Free Theorems in the Presence of seq: Patricia Johann (Rutgers University) and Janis Voigtländer (Dresden University of Technology).
Parsing Expression Grammars: A Recognition-Based Syntactic Foundation: Bryan Ford (Massachusetts Institute of Technology).

Towards a Grainless Semantics for Shared Variable Concurrency: John C. Reynolds (Carnegie Mellon University). (Slides available online.)

Asynchronous and Deterministic Objects: Denis Caromel, Ludovic Henrio, and Bernard Paul Serpette (INRIA Sophia-Antipolis).
A Logic You Can Count On: Silvano Dal Zilio, Denis Lugiez, and Charles Meyssonnier (CNRS, University of Provence).
Channel Dependent Types for Higher-Order Mobile Processes: Nobuko Yoshida (Imperial College London).
A Bisimulation for Dynamic Sealing: Eijiro Sumii and Benjamin C. Pierce (University of Pennsylvania).

An Abstract Interpretation-Based Framework for Software Watermarking: Patrick Cousot (École Normale Supérieure) and Radhia Cousot (CNRS, École Polytechnique).
Abstract Non-Interference: Parameterizing Non-Interference by Abstract Interpretation: Roberto Giacobazzi and Isabella Mastroeni (University of Verona).
A Semantics for Web Services Authentication: Karthikeyan Bhargavan, Cédric Fournet, and Andrew D. Gordon (Microsoft Research).

The Space Cost of Lazy Reference Counting: Hans-J. Boehm (HP Laboratories).
Local Reasoning about a Copying Garbage Collector: Lars Birkedal, Noah Torp-Smith (IT University of Copenhagen), and John C. Reynolds (Carnegie Mellon University).

An Automata Theoretic Approach to Software Model Checking: Javier Esparza (University of Stuttgart).

Abstractions from Proofs: Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar (University of California at Berkeley), and Kenneth L. McMillan (Cadence Berkeley Labs).
Summarizing procedures in concurrent programs: Shaz Qadeer, Sriram K. Rajamani, and Jakob Rehof (Microsoft Research).
Atomizer: A Dynamic Atomicity Checker For Multithreaded Programs: Cormac Flanagan (University of California at Santa Cruz), Stephen N. Freund (Williams College).
Separation and Information Hiding: Peter W. O'Hearn (Queen Mary University of London), Hongseok Yang (Korea Advanced Institute of Science and Technology), and John C. Reynolds (Carnegie Mellon University).

Tridirectional Typechecking: Joshua Dunfield and Frank Pfenning (Carnegie Mellon University).
A Type System for Well-Founded Recursion: Derek Dreyer (Carnegie Mellon University).
Principal Typings for Java-Like Languages: Davide Ancona and Elena Zucca (University of Genova).

Non-linear Loop Invariant Generation using Gröbner Bases: Sriram Sankaranarayanan, Henny B. Sipma, and Zohar Manna (Stanford University).
Precise Interprocedural Analysis through Linear Algebra: Markus Müller-Olm (FernUniversität Hagen) and Helmut Seidl (Technische Universität München).
Global Value Numbering using Random Interpretation: Sumit Gulwani and George C. Necula (University of California at Berkeley).