Title

Authors

Contact Affiliation

Staged Allocation: A Compositional Technique for Specifying and Implementing Procedure Calling Conventions

Reuben Olinsky, Christian Lindig and Norman Ramsey

Harvard University

Small Bisimulations for Reasoning About Higher-Order Imperative Programs

Vasileios Koutavas and Mitchell Wand

Northeastern University

The Next 700 Data Description Languages

Kathleen Fisher, Yitzhak Mandelbaum and David Walker

Princeton University

Decidability and Proof Systems for Language-Based Noninterference Relations

Mads Dam

KTH

Polymorphic Regular Tree Types and Patterns

Jérôme Vouillon

CNRS and Université Paris 7

Harmless Advice

Daniel Dantas and David Walker

Princeton University

Formal certification of a compiler back-end, or: programming a compiler with a proof assistant

Xavier Leroy

INRIA Rocquencourt

A Logic for Information Flow Analysis of Pointer Programs

Torben Amtoft, Sruthi Bandhakavi and Anindya Banerjee

Kansas State University

Compiler-Directed Channel Allocation for Saving Power in On-Chip Networks

Guangyu Chen, Feihui Li and Mahmut Kandemir

Pennsylvania State University

Stratified type inference for generalized algebraic data types

François Pottier and Yann Régis-Gianas

INRIA

Adventures in Time and Space

James S. Royer

Syracuse University

Environmental Analysis via $\Delta$CFA

Matthew Might and Olin Shivers

Georgia Institute of Technology

Fast and Loose Reasoning is Morally Correct

Nils Anders Danielsson, Jeremy Gibbons, John Hughes and Patrik Jansson

Chalmers University of Technology

Frame rules from answer types for code pointers

Hayo Thielecke

University of Birmingham

Modular Set-Based Analysis from Contracts

Philippe Meunier, Robert Bruce Findler and Matthias Felleisen

Northeastern University

A Virtual Class Calculus

Erik Ernst and Klaus Ostermann and William R. Cook

University of Aarhus

Associating Synchronization Constraints with Data in an Object-Oriented Language

Mandana Vaziri, Frank Tip and Julian Dolby

IBM Research

A Hierarchical Model of Data Locality

Chengliang Zhang, Yutao Zhong, Mitsunori Ogihara and Chen Ding

University of Rochester

Certified Assembly Programming with Embedded Code Pointers

Zhaozhong Ni and Zhong Shao

Yale University

Interruptible Iterators

Jed Liu, Aaron Kimball and Andrew C. Myers

Cornell University

Specifying C++ concepts

Gabriel Dos Reis and Bjarne Stroustrup

Texas A&M University

Verifying Properties of Well-Founded Linked Lists

Shuvendu K. Lahiri and Shaz Qadeer

Microsoft Research

A Verifiable SSA Program Representation for Aggressive Compiler Optimization

Vijay S Menon, Neal Glew, Brian R Murphy, Andrew McCreight, Tatiana Shpeisman, Ali-Reza Adl-Tabatabai and Leaf Petersen

Intel Corporation

A Fixpoint Calculus for Local and Global Program Flows

Rajeev Alur, Swarat Chaudhuri, and P. Madhusudan

University of Pennsylvania

On Flow-Sensitive Security Types

Sebastian Hunt and David Sands

City University

Protecting Representation with Effect Encapsulation

Yi Lu and John Potter

UNSW

The Essence of Command Injection Attacks in Web Applications

Zhendong Su and Gary Wassermann

University of California, Davis

Autolocker: Synchronization Inference for Atomic Sections

Bill McCloskey, Feng Zhou, David Gay and Eric Brewer

UC Berkeley

Hybrid Type Checking

Cormac Flanagan

UCSC

Engineering with Logic: HOL Specification and Symbolic-Evaluation Testing for TCP Implementations

Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith and Keith Wansbrough

University of Cambridge

A Polymorphic Modal Type System for Lisp-like Multi-Staged Languages

Ik-Soon Kim and Kwangkeun Yi and Cristiano Calcagno

Seoul National University

N-Synchronous Kahn Networks

Albert Cohen, Christine Eisenbeis, Mard Duranton, Claire Pagetti, Florence Plateau and Marc Pouzet

INRIA Futurs

Simplifying Reductions

Gautam Gupta and Sanjay Rajopadhye

Colorado State University