POPL '14- Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Full Citation in the ACM Digital Library

SESSION: Milner award

Modular reasoning about concurrent higher-order imperative programs

• Lars Birkedal

SESSION: SIGPLAN achievement award

A galois connection calculus for abstract interpretation

• Patrick` Cousot
• Radhia Cousot

SESSION: Type system design

• Nate Foster

Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation

• Giuseppe Castagna
• Kim Nguyen
• Zhiwu Xu
• Hyeonseung Im
• Sergueï Lenglet
• Luca Padovani

Backpack: retrofitting Haskell with interfaces

• Scott Kilpatrick
• Derek Dreyer
• Simon Peyton Jones
• Simon Marlow

Combining proofs and programs in a dependently typed language

• Chris Casinghino
• Vilhelm Sjöberg
• Stephanie Weirich

SESSION: Program analysis 1

• Xavier Rival

Tracing compilation by abstract interpretation

• Stefano Dissegna
• Francesco Logozzo
• Francesco Ranzato

A type-directed abstraction refinement approach to higher-order model checking

• Steven J. Ramsay
• Robin P. Neatherway
• C.-H. Luke Ong

Fissile type analysis: modular checking of almost everywhere invariants

• Devin Coughlin
• Bor-Yuh Evan Chang

SESSION: Semantics of systems

• James Cheney

A trusted mechanised JavaScript specification

• Martin Bodin
• Arthur Chargueraud
• Daniele Filaretti
• Philippa Gardner
• Sergio Maffeis
• Daiva Naudziuniene
• Alan Schmitt
• Gareth Smith

An operational and axiomatic semantics for non-determinism and sequence points in C

• Robbert Krebbers

NetKAT: semantic foundations for networks

• Carolyn Jane Anderson
• Nate Foster
• Arjun Guha
• Jean-Baptiste Jeannin
• Dexter Kozen
• Cole Schlesinger
• David Walker

SESSION: Program analysis 2

• Thomas Wies

Bias-variance tradeoffs in program analysis

• Rahul Sharma
• Aditya V. Nori
• Alex Aiken

Abstract satisfaction

• Vijay D'Silva
• Leopold Haller
• Daniel Kroening

Proofs that count

• Azadeh Farzan
• Zachary Kincaid
• Andreas Podelski

SESSION: Verified systems

• Aaron Turon

A verified information-flow architecture

• Arthur Azevedo de Amorim
• Nathan Collins
• André DeHon
• Delphine Demange
• Cătălin Hriţcu
• David Pichardie
• Benjamin C. Pierce
• Randy Pollack
• Andrew Tolmach

CakeML: a verified implementation of ML

• Ramana Kumar
• Magnus O. Myreen
• Michael Norrish
• Scott Owens

Probabilistic relational verification for cryptographic implementations

• Gilles Barthe
• Cédric Fournet
• Benjamin Grégoire
• Pierre-Yves Strub
• Nikhil Swamy
• Santiago Zanella-Béguelin

SESSION: Synthesis

• Aditya Nori

Bridging boolean and quantitative synthesis using smoothed proof search

• Swarat Chaudhuri
• Martin Clochard
• Armando Solar-Lezama

A constraint-based approach to solving games on infinite graphs

• Tewodros Beyene
• Swarat Chaudhuri
• Corneliu Popeea
• Andrey Rybalchenko

Sound compilation of reals

• Eva Darulova
• Viktor Kuncak

SESSION: SIGPLAN software systems award

30 years of research and development around Coq

• Gérard Huet
• Hugo Herbelin

SESSION: In memory of John Reynolds

The essence of Reynolds

• Stephen Brookes
• Peter W. O'Hearn
• Uday Reddy

SESSION: Concurrent programming models

• Viktor Vafeiadis

Freeze after writing: quasi-deterministic parallel programming with LVars

• Lindsey Kuper
• Aaron Turon
• Neelakantan R. Krishnaswami
• Ryan R. Newton

Replicated data types: specification, verification, optimality

• Sebastian Burckhardt
• Alexey Gotsman
• Hongseok Yang
• Marek Zawirski

Verifying eventual consistency of optimistic replication systems

• Ahmed Bouajjani
• Constantin Enea
• Jad Hamza

SESSION: Probability

• Nikhil Swamy

On coinductive equivalences for higher-order probabilistic functional programs

• Ugo Dal Lago
• Davide Sangiorgi
• Michele Alberti

Probabilistic coherence spaces are fully abstract for probabilistic PCF

• Thomas Ehrhard
• Christine Tasson
• Michele Pagani

Tabular: a schema-driven probabilistic programming language

• Andrew D. Gordon
• Thore Graepel
• Nicolas Rolland
• Claudio Russo
• Johannes Borgstrom
• John Guiver

SESSION: Functional programming 1

• Alan Jeffrey

Modular, higher-order cardinality analysis in theory and practice

• Ilya Sergey
• Dimitrios Vytiniotis
• Simon Peyton Jones

Profiling for laziness

• Stephen Chang
• Matthias Felleisen

Fair reactive programming

• Andrew Cave
• Francisco Ferreira
• Prakash Panangaden
• Brigitte Pientka

SESSION: Reasoning

• Andrey Rybalchenko

Optimal dynamic partial order reduction

• Parosh Abdulla
• Stavros Aronis
• Bengt Jonsson
• Konstantinos Sagonas

Modular reasoning about heap paths via effectively propositional formulas

• Shachar Itzhaky
• Anindya Banerjee
• Neil Immerman
• Ori Lahav
• Aleksandar Nanevski
• Mooly Sagiv

A sound and complete abstraction for reasoning about parallel prefix sums

• Nathan Chong
• Alastair F. Donaldson
• Jeroen Ketema

SESSION: Security

• Ross Tate

Authenticated data structures, generically

• Andrew Miller
• Michael Hicks
• Jonathan Katz
• Elaine Shi

Gradual typing embedded securely in JavaScript

• Nikhil Swamy
• Cedric Fournet
• Aseem Rastogi
• Karthikeyan Bhargavan
• Juan Chen
• Pierre-Yves Strub
• Gavin Bierman

Sound input filter generation for integer overflow errors

• Fan Long
• Stelios Sidiroglou-Douskos
• Deokhwan Kim
• Martin Rinard

SESSION: Separation logic

• Andrew W. Appel

Parametric completeness for separation theories

• James Brotherston
• Jules Villard

Proof search for propositional abstract separation logics via labelled sequents

• Zhé Hóu
• Ranald Clouston
• Rajeev Goré
• Alwen Tiu

A proof system for separation logic with magic wand

• Wonyeol Lee
• Sungwoo Park

SESSION: Semantic models 1

• Nick Benton

From parametricity to conservation laws, via Noether's theorem

• Robert Atkey

A relationally parametric model of dependent type theory

• Robert Atkey
• Neil Ghani
• Patricia Johann

Game semantics for interface middleweight Java

• Andrzej S. Murawski
• Nikos Tzevelekos

SESSION: Program analysis 3

• Ahmed Bouajjani

Abstract acceleration of general linear loops

• Bertrand Jeannet
• Peter Schrammel
• Sriram Sankaranarayanan

Minimization of symbolic automata

• Loris D'Antoni
• Margus Veanes

Consistency analysis of decision-making programs

• Swarat Chaudhuri
• Azadeh Farzan
• Zachary Kincaid

SESSION: Static errors

• Stephanie Weirich

Toward general diagnosis of static errors

• Danfeng Zhang
• Andrew C. Myers

Counter-factual typing for debugging type errors

• Sheng Chen
• Martin Erwig

SESSION: Model checking and SMT

• Noam Rinetzky

Battery transition systems

• Udi Boker
• Thomas A. Henzinger
• Arjun Radhakrishna

Symbolic optimization with SMT solvers

• Yi Li
• Aws Albarghouthi
• Zachary Kincaid
• Arie Gurfinkel
• Marsha Chechik

SESSION: Semantic models 2

• Lars Birkedal

Abstract effects and proof-relevant logical relations

• Nick Benton
• Martin Hofmann
• Vivek Nigam

Parametric effect monads and semantics of effect systems

• Shin-ya Katsumata

Applying quantitative semantics to higher-order quantum computing

• Michele Pagani
• Peter Selinger
• Benoît Valiron

SESSION: Functional programming 2

• Neelakantan R. Krishnaswami

A nonstandard standardization theorem

• Beniamino Accattoli
• Eduardo Bonelli
• Delia Kesner
• Carlos Lombardi

Closed type families with overlapping equations

• Richard A. Eisenberg
• Dimitrios Vytiniotis
• Simon Peyton Jones
• Stephanie Weirich