Skip to content
An unofficial list of papers accepted to POPL 2013.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Failed to load latest commit information.


An unofficial list of papers accepted to POPL 2013, with hyperlinks to PDFs where possible.

Day 1


Full Abstraction for Nominal Scott Domains

  • S. Lösch
  • A. Pitts

The sequential semantics of producer effect systems.

  • R. Tate

Copatterns: programming infinite structures by observations.

  • A. Abel
  • B. Pientka
  • D. Thibodeau
  • A. Setzer

Verification & Static Analysis

Cache and I/O efficient functional algorithms.

  • G. Blelloch
  • R. Harper

On the linear ranking problem for integer linear-constraint loops. (arXiv)

  • A. Ben-Amram
  • S. Genaim

Advanced automata minimization.

  • R. Mayr
  • L. Clemente


Automating relatively complete verification of higher-order functional programs.

  • H. Unno
  • T. Terauchi
  • N. Kobayashi

Abstraction and invariance for algebraically indexed types.

  • R. Atkey
  • P. Johann
  • A. Kennedy

Static and dynamic semantics of NoSQL languages.

  • V. Benzaken
  • G. Castagna
  • K. Nguyễn
  • J. Siméon

Abstract Interpretation

Quantitative abstraction refinement.

  • P. Cerny
  • T. Henzinger
  • A. Radhakrishna

Inductive data flow graphs.

  • A. Farzan
  • Z. Kincaid
  • A. Podelski

Abstract conflict driven learning.

  • V. D'Silva
  • L. Haller
  • D. Kroening


The lambda lambda-bar calculus.

  • A. Goyet

The Geometry of Types. (arXiv)

  • U. Lago
  • B. Petit

Universal properties for impure programming languages.

  • S. Staton
  • P. Levy

Proofs & Verification

The power of parameterization in coinductive proof.

  • C. Hur
  • G. Neis
  • D. Dreyer
  • V. Vafeiadis

Meta-theory a la carte.

  • B. Delaware
  • B. Oliveira
  • T. Schrijvers

A theorem prover for Boolean BI.

  • J. Park
  • J. Seo
  • S. Park

Day 2

Concurrency & Design

Library abstraction for C/C++ concurrency.

  • M. Batty
  • M. Dodds
  • A. Gotsman

Fault tolerance via idempotence.

  • G. Ramalingam
  • K. Vaswani

Deadlock-freedom-by-design: multiparty asynchronous global programming.

  • M. Carbone
  • F. Montesi

Separation Logic

The type discipline of behavioral separation.

  • L. Caires
  • J. Seco

Views: compositional reasoning for concurrent programs.

  • T. Dinsdale-Young
  • L. Birkedal
  • P. Gardner
  • M. Parkinson
  • H. Yang

High-level separation Logic for low-level code.

  • J. Jensen
  • N. Benton
  • A. Kennedy


Quantitative relaxation of concurrent data structures.

  • T. Henzinger
  • C. Kirsch
  • H. Payer
  • A. Sezgin
  • A. Sokolova

Plan B: a buffered memory model for Java.

  • D. Demange
  • V. Laporte
  • L. Zhao
  • S. Jagannathan
  • D. Pichardie
  • J. Vitek

Logical relations for fine-grained concurrency.

  • A. Turon
  • J. Thamsborg
  • A. Ahmed
  • L. Birkedal
  • D. Dreyer


Towards fully automatic placement of security sanitizers and declassifiers.

  • B. Livshits
  • S. Chong

Linear dependent types for differential privacy.

  • M. Gaboardi
  • A. Haeberlen
  • J. Hsu
  • A. Narayan
  • B. Pierce

Fully abstract compilation to JavaScript.

  • C. Fournet
  • N. Swamy
  • J. Chen
  • P. Dagand
  • P. Strub
  • B. Livshits

Day 3

Models & Semantics

A model-learner pattern for Bayesian reasoning.

  • A. Gordon
  • M. Aizatulin
  • J. Borgstroem
  • G. Claret
  • T. Graepel
  • A. Nori
  • S. Rajamani
  • C. Russo

Hyperstream processing systems: nonstandard modeling of continuous-time signals.

  • K. Suenaga
  • H. Sekine
  • I. Hasuo

HALO: From Haskell to first-order logic through denotational semantics.

  • D. Vytiniotis
  • S. Jones
  • K. Claessen
  • D. Rosén

Synthesis & Verification

Sigma*: Symbolic Learning of Stream Filters.

  • M. Botincan
  • D. Babic

Checking NFA equivalence with bisimulations up to congruence.

  • F. Bonchi
  • D. Pous

Synthesis of biological models from mutation experiments.

  • A. Köksal
  • Y. Pu
  • S. Srivastava
  • R. Bodík
  • J. Fisher
  • N. Piterman


Sub-polyhedral scheduling using (unit-)two-variable-per-inequality polyhedra.

  • R. Upadrasta
  • A. Cohen

Optimizing data structures in high-level programs: new directions for extensible compilers based on staging.

  • T. Rompf
  • A. Sujeeth
  • N. Amin
  • K. Brown
  • V. Jovanovic
  • H. Lee
  • M. Jonalagedda
  • K. Olukotun
  • M. Odersky

Principled parsing for indentation-sensitive languages.

  • M. Adams

Analysis & Logics

The ramifications of sharing in data structures.

  • A. Hobor
  • J. Villard

Complete instantiation-based interpolation.

  • N. Totla
  • T. Wies

Automatic detection of floating-point exceptions.

  • E. Barr
  • T. Vo
  • V. Le
  • Z. Su

Subjective auxiliary state for coarse-grained concurrency.

  • R. Ley-Wild
  • A. Nanevski

PLPV 2013

Modular Type-Safety Proofs in Agda.

  • Christopher Schwaab
  • Jeremy Siek

Compiling Contextual Objects: Bringing Higher-Order Abstract Syntax to Programmers.

  • Francisco Ferreira
  • Brigitte Pientka
  • Stefan Monnier

A Static Cost Analysis for a Higher-Order Language. (arXiv)

  • Norman Danner
  • Jennifer Paykin
  • James Royer

Towards Formal Verification of TLS Network Packet Processing in C.

  • Reynald Affeldt
  • Nicolas Marti

Automated Analysis of Rule-Based Access Control Policies.

  • Clara Bertolissi
  • Worachet Uttha

Causality For Free! Parametricity Implies Causality for Functional Reactive Programs.

  • Alan Jeffrey

Temporal Logic with “Until”: Functional Reactive Programming with Processes and Concrete Process Categories.

  • Wolfgang Jeltsch
Something went wrong with that request. Please try again.