Venues / POPL /

POPL 2014

55 papers

30 years of research and development around Coq · Gérard P. Huet, Hugo Herbelin
A Galois connection calculus for abstract interpretation · Patrick Cousot, Radhia Cousot
A constraint-based approach to solving games on infinite graphs · Tewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, Andrey Rybalchenko
A nonstandard standardization theorem · Beniamino Accattoli, Eduardo Bonelli, Delia Kesner, Carlos Lombardi
A proof system for separation logic with magic wand · Wonyeol Lee, Sungwoo Park
A relationally parametric model of dependent type theory · Robert Atkey, Neil Ghani, Patricia Johann
A sound and complete abstraction for reasoning about parallel prefix sums · Nathan Chong, Alastair F. Donaldson, Jeroen Ketema
A trusted mechanised JavaScript specification · Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene + 2 more
A type-directed abstraction refinement approach to higher-order model checking · Steven J. Ramsay, Robin P. Neatherway, C.-H. Luke Ong
A verified information-flow architecture · Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie + 3 more
Abstract acceleration of general linear loops · Bertrand Jeannet, Peter Schrammel, Sriram Sankaranarayanan
Abstract effects and proof-relevant logical relations · Nick Benton, Martin Hofmann, Vivek Nigam
Abstract satisfaction · Vijay Victor D'Silva, Leopold Haller, Daniel Kroening
An operational and axiomatic semantics for non-determinism and sequence points in C · Robbert Krebbers
Applying quantitative semantics to higher-order quantum computing · Michele Pagani, Peter Selinger, Benoît Valiron
Authenticated data structures, generically · Andrew Miller, Michael Hicks, Jonathan Katz, Elaine Shi
Backpack: retrofitting Haskell with interfaces · Scott Kilpatrick, Derek Dreyer, Simon L. Peyton Jones, Simon Marlow
Battery transition systems · Udi Boker, Thomas A. Henzinger, Arjun Radhakrishna
Bias-variance tradeoffs in program analysis · Rahul Sharma, Aditya V. Nori, Alex Aiken
Bridging boolean and quantitative synthesis using smoothed proof search · Swarat Chaudhuri, Martin Clochard, Armando Solar-Lezama
CakeML: a verified implementation of ML · Ramana Kumar, Magnus O. Myreen, Michael Norrish, Scott Owens
Closed type families with overlapping equations · Richard A. Eisenberg, Dimitrios Vytiniotis, Simon L. Peyton Jones, Stephanie Weirich
Combining proofs and programs in a dependently typed language · Chris Casinghino, Vilhelm Sjöberg, Stephanie Weirich
Consistency analysis of decision-making programs · Swarat Chaudhuri, Azadeh Farzan, Zachary Kincaid
Counter-factual typing for debugging type errors · Sheng Chen, Martin Erwig
Fair reactive programming · Andrew Cave, Francisco Ferreira, Prakash Panangaden, Brigitte Pientka
Fissile type analysis: modular checking of almost everywhere invariants · Devin Coughlin, Bor-Yuh Evan Chang
Freeze after writing: quasi-deterministic parallel programming with LVars · Lindsey Kuper, Aaron Turon, Neelakantan R. Krishnaswami, Ryan R. Newton
From parametricity to conservation laws, via Noether's theorem · Robert Atkey
Game semantics for interface middleweight Java · Andrzej S. Murawski, Nikos Tzevelekos
Gradual typing embedded securely in JavaScript · Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub + 1 more
Minimization of symbolic automata · Loris D'Antoni, Margus Veanes
Modular reasoning about concurrent higher-order imperative programs · Lars Birkedal
Modular reasoning about heap paths via effectively propositional formulas · Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv
Modular, higher-order cardinality analysis in theory and practice · Ilya Sergey, Dimitrios Vytiniotis, Simon L. Peyton Jones
NetkAT: semantic foundations for networks · Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger + 1 more
On coinductive equivalences for higher-order probabilistic functional programs · Ugo Dal Lago, Davide Sangiorgi, Michele Alberti
Optimal dynamic partial order reduction · Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, Konstantinos Sagonas
Parametric completeness for separation theories · James Brotherston, Jules Villard
Parametric effect monads and semantics of effect systems · Shin-ya Katsumata
Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation · Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, Hyeonseung Im, Sergueï Lenglet, Luca Padovani
Probabilistic coherence spaces are fully abstract for probabilistic PCF · Thomas Ehrhard, Christine Tasson, Michele Pagani
Probabilistic relational verification for cryptographic implementations · Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella-Béguelin
Profiling for laziness · Stephen Chang, Matthias Felleisen
Proof search for propositional abstract separation logics via labelled sequents · Zhe Hou, Ranald Clouston, Rajeev Goré, Alwen Tiu
Proofs that count · Azadeh Farzan, Zachary Kincaid, Andreas Podelski
Replicated data types: specification, verification, optimality · Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, Marek Zawirski
Sound compilation of reals · Eva Darulova, Viktor Kuncak
Sound input filter generation for integer overflow errors · Fan Long, Stelios Sidiroglou-Douskos, Deokhwan Kim, Martin C. Rinard
Symbolic optimization with SMT solvers · Yi Li, Aws Albarghouthi, Zachary Kincaid, Arie Gurfinkel, Marsha Chechik
Tabular: a schema-driven probabilistic programming language · Andrew D. Gordon, Thore Graepel, Nicolas Rolland, Claudio V. Russo, Johannes Borgström, John Guiver
The essence of Reynolds · Stephen Brookes, Peter W. O'Hearn, Uday S. Reddy
Toward general diagnosis of static errors · Danfeng Zhang, Andrew C. Myers
Tracing compilation by abstract interpretation · Stefano Dissegna, Francesco Logozzo, Francesco Ranzato
Verifying eventual consistency of optimistic replication systems · Ahmed Bouajjani, Constantin Enea, Jad Hamza