POPL 2004 program

Venice, Italy, January 14-16, 2004

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

9:00-10:00. Invited talk

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

10:30-12:30. Session 1

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).

14:00-15:30. Session 2

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).

16:00-17:30. Session 3

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).

Thursday, January 15th

9:00-10:00. SIGPLAN Programming Language Achievement Award lecture

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

10:30-12:30. Session 4

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).

14:00-15:30. Session 5

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).

16:00-17:00. Session 6

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).

Friday, January 16th

9:00-10:00. Invited talk

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

10:30-12:30. Session 7

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).

14:00-15:30. Session 8

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).

16:00-17:30. Session 9

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).