This page will soon grow in content and contain information about the scope of this research track.

Wed 20 Jan

10:30 - 12:10: Research Papers - Track 1: Algorithmic Verification at Grand Bay North
Chair(s): Arie GurfinkelCarnegie Mellon University

10:30 - 10:55
Talk

Temporal Verification of Higher-order Functional Programs

Akihiro Murase, Tachio TerauchiJAIST, Naoki KobayashiUniversity of Tokyo, Ryosuke SatoUniversity of Tokyo, Hiroshi UnnoUniversity of Tsukuba

10:55 - 11:20
Talk

Scaling Network Verification using Symmetry and Surgery

Gordon Plotkin, Nikolaj BjørnerMicrosoft Research, Nuno P. LopesMicrosoft Research, Andrey RybalchenkoMicrosoft Research, George VargheseMicrosoft Research

11:20 - 11:45
Talk

Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates

James Brotherston, Nikos Gorogiannis, Max Kanovich, Reuben Rowe

11:45 - 12:10
Talk

Reducing Crash Recoverability to Reachability

Eric KoskinenYale University, Junfeng YangColumbia University

10:30 - 12:10: Research Papers - Track 2: Types and Foundations at Grand Bay South
Chair(s): Robert AtkeyUniversity of Strathclyde

10:30 - 10:55
Talk

Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega

Matt BrownUCLA, Jens PalsbergUniversity of California, Los Angeles

Media Attached File Attached

10:55 - 11:20
Talk

Type Theory in Type Theory using Quotient Inductive Types

Thorsten AltenkirchUniversity of Nottingham, Ambrus KaposiUniversity of Nottingham

Media Attached File Attached

11:20 - 11:45
Talk

System Fω with Equirecursive Types for Datatype-generic Programming

Yufei CaiUniversity of Tübingen, Germany, Paolo G. GiarrussoUniversity of Tübingen, Germany, Klaus OstermannUniversity of Tübingen, Germany

Media Attached

11:45 - 12:10
Talk

A Theory of Effects and Resources: Adjunction Models and Polarised Calculi

Pierre-Louis CurienUniv. Paris Diderot and INRIA Paris-Rocquencourt, Marcelo FioreComputer Laboratory, University of Cambridge, Guillaume Munch-MaccagnoniComputer Laboratory, University of Cambridge

14:20 - 16:00: Research Papers - Track 1: Decision Procedures at Grand Bay North
Chair(s): Loris D'AntoniUniversity of Pennsylvania

14:20 - 14:45
Talk

Query-Guided Maximum Satisfiability

Xin ZhangGeorgia Tech, Ravi MangalGeorgia Institute of Technology, Aditya NoriMicrosoft Research, UK, Mayur NaikGeorgia Tech

File Attached

14:45 - 15:10
Talk

String Solving with Word Equations and Transducers: Decidability and Applications to Detecting Mutation XSS

Anthony Widjaja LinYale-NUS College, Singapore, Pablo BarceloUniversity of Chile, Chile

Media Attached

15:10 - 15:35
Talk

Symbolic Computation of Differential Equivalences

Luca CardelliMicrosoft Research and University of Oxford, Mirco TribastoneIMT Institute for Advanced Studies Lucca, Italy, Max TschaikowskiIMT Institute for Advanced Studies Lucca, Italy, Andrea VandinIMT Institute for Advanced Studies Lucca, Italy

Media Attached

15:35 - 16:00
Talk

Unboundedness and Downward Closures of Higher-Order Pushdown Automata

Matthew HagueRoyal Holloway University of London, UK, Jonathan KochemsDepartment of Computer Science, University of Oxford, C.-H. Luke OngUniversity of Oxford, UK

Media Attached

14:20 - 16:00: Research Papers - Track 2: Correct Compilation at Grand Bay South
Chair(s): Jens PalsbergUniversity of California, Los Angeles

14:20 - 14:45
Talk

Fully-Abstract Compilation by Approximate Back-Translation

Dominique DevrieseiMinds - Distrinet, KU Leuven, Marco PatrignaniKU Leuven, Frank PiessensiMinds - Distrinet, KU Leuven

Pre-print Media Attached

14:45 - 15:10
Talk

Lightweight Verification of Separate Compilation

Jeehoon KangSeoul National University, Yoonseung KimSeoul National University (South Korea), Chung-Kil HurSeoul National University, Derek DreyerMPI-SWS, Viktor VafeiadisMPI-SWS, Germany

Media Attached File Attached

15:10 - 15:35
Talk

From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes

Ed RobbinsKent, Andy KingKent, Tom SchrijversKU Leuven

Media Attached

15:35 - 16:00
Talk

Sound Type-dependent Syntactic Language Extension

Florian LorenzenTU Berlin, Sebastian ErdwegTU Darmstadt, Germany

Pre-print Media Attached File Attached

16:30 - 17:45: Research Papers - Track 1: Language Design at Grand Bay North
Chair(s): David WalkerPrinceton University

16:30 - 16:55
Talk

Dependent Types and Multi-Monadic Effects in F*

Nikhil SwamyMicrosoft Research, Cătălin HriţcuINRIA Paris, Chantal KellerMSR-INRIA, Aseem RastogiUniversity of Maryland, College Park, Antoine Delignat-LavaudINRIA, Simon ForestENS, Karthikeyan BhargavanINRIA, Cédric FournetMicrosoft Research, Pierre-Yves StrubIMDEA Software Institute, Markulf KohlweissMicrosoft Research, Jean-Karim ZinzindohouéINRIA, Santiago Zanella-BéguelinMicrosoft Research

Pre-print Media Attached

16:55 - 17:20
Talk

Fabular: Regression Formulas as Probabilistic Programming

Johannes BorgströmUppsala University, Andrew D. GordonMicrosoft Research and University of Edinburgh, Long OuyangStanford University, Claudio RussoMicrosoft Research, Adam ŚcibiorUniversity of Cambridge, Marcin SzymczakUniversity of Edinburgh

Media Attached

17:20 - 17:45
Talk

Kleenex: Compiling Nondeterministic Transducers to Deterministic Streaming Transducers

Bjørn Bugge GrathwohlDIKU, University of Copenhagen, Fritz HengleinDIKU, Denmark, Ulrik Terp RasmussenDIKU, University of Copenhagen, Kristoffer Aalund SøholmJobindex, Denmark, Sebastian Paaske TørholmJobindex, Denmark

Media Attached

16:30 - 17:45: Research Papers - Track 2: Decidability and complexity at Grand Bay South
Chair(s): C.-H. Luke OngUniversity of Oxford, UK

16:30 - 16:55
Talk

Decidability of Inferring Inductive Invariants

Oded PadonTel Aviv University, Neil ImmermanUniversity of Massachusetts, Amherst, Sharon Shoham, Aleksandr KarbyshevTel Aviv University, Mooly SagivTel Aviv University

Media Attached

16:55 - 17:20
Talk

The Hardness of Data Packing

Rahman Lavaee, Chen DingUniversity of Rochester

Media Attached

17:20 - 17:45
Talk

The Complexity of Interaction

Stéphane GimenezUniversity of Innsbruck, Georg MoserUniversity of Innsbruck

Media Attached

19:00 - 22:00: Research Papers - Banquet at Dali Museum

Thu 21 Jan

10:30 - 12:10: Research Papers - Track 1: Foundations of distributed systems at Grand Bay North
Chair(s): Mooly SagivTel Aviv University

10:30 - 10:55
Talk

Certified Causally Consistent Distributed Key-Value Stores

Mohsen LesaniMIT, Christian J. BellMIT CSAIL, Adam ChlipalaMIT

Media Attached

10:55 - 11:20
Talk

'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems

Alexey GotsmanIMDEA, Hongseok YangUniversity of Oxford, UK, Carla FerreiraUniversidade Nova Lisboa, Mahsa NajafzadehUPMC & INRIA, Marc ShapiroInria & LIP6

Media Attached

11:20 - 11:45
Talk

A Program Logic for Concurrent Objects under Fair Scheduling

Hongjin LiangUniversity of Science and Technology of China, Xinyu FengUniversity of Science and Technology of China

Media Attached

11:45 - 12:10
Talk

PSync: a partially synchronous language for fault-tolerant distributed algorithms

Cezara DrăgoiINRIA, ENS, CNRS, Thomas A. HenzingerIST Austria, Damien ZuffereyMIT

Link to publication DOI Pre-print Media Attached File Attached

10:30 - 12:10: Research Papers - Track 2: Probabilistic and statistical analysis at Grand Bay South
Chair(s): Aditya NoriMicrosoft Research, UK

10:30 - 10:55
Talk

Prophet: Automatic Patch Generation via Learning from Successful Patches

Fan LongMIT CSAIL, Martin RinardMassachusetts Institute of Technology, USA

Media Attached

10:55 - 11:20
Talk

Estimating types in binaries using predictive modeling

Omer KatzTechnion, Israel Institute of Technology, Ran El-YanivTechnion, Israel Institute of Technology, Eran YahavTechnion

Media Attached File Attached

11:20 - 11:45
Talk

Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs

Krishnendu ChatterjeeIST Austria, Hongfei FuIST Austria, Rouzbeh HasheminezhadSharif University, Petr NovotnyIST Austria

Media Attached

11:45 - 12:10
Talk

Transforming Spreadsheet Data Types using Examples

Rishabh SinghMicrosoft Research, Sumit GulwaniMicrosoft Research

Media Attached

14:20 - 16:00: Research Papers - Track 1: Learning and verification at Grand Bay North
Chair(s): David MonniauxCNRS, VERIMAG

14:20 - 14:45
Talk

Combining Static Analysis with Probabilistic Models to Enable Market-Scale Analysis

Damien OcteauUniversity of Wisconsin and Pennsylvania State University, Somesh JhaUniversity of Wisconsin, Madison, Matthew DeringPennsylvania State University, Patrick McDanielPennsylvania State University, Alexandre BartelTechnical University Darmstadt, Hongyu LiRice University, Jacques KleinUniversity of Luxembourg, Yves Le TraonUniversity of Luxembourg

Media Attached

14:45 - 15:10
Talk

Abstraction Refinement Guided by a Learnt Probabilistic Model

Radu GrigoreUniversity of Oxford, Hongseok YangUniversity of Oxford, UK

Media Attached

15:10 - 15:35
Talk

Learning Invariants using Decision Trees and Implication Counterexamples

Pranav GargUniversity of Illinois at Urbana-Champaign, Daniel NeiderUniversity of Illinois at Urbana-Champaign, P. MadhusudanUniversity of Illinois at Urbana-Champaign, Dan RothUniversity of Illinois at Urbana-Champaign

Media Attached

15:35 - 16:00
Talk

Symbolic Abstract Data Type Inference

Michael EmmiIMDEA Software Institute, Constantin EneaLIAFA, Université Paris Diderot

Media Attached

14:20 - 16:00: Research Papers - Track 2: Types, Generally or Gradually at Grand Bay South
Chair(s): Tiark RompfPurdue & Oracle Labs

14:20 - 14:45
Talk

Principal Type Inference for GADTs

Sheng ChenUniversity of louisiana at Lafayette, Martin ErwigOregon State University

Media Attached

14:45 - 15:10
Talk

Abstracting Gradual Typing

Ronald GarciaUniversity of British Columbia, Alison M. Clark, Éric TanterUniversity of Chile, Chile

Link to publication Media Attached

15:10 - 15:35
Talk

The Gradualizer: a methodology and algorithm for generating gradual type systems

Matteo CiminiIndiana University, Jeremy G. SiekIndiana University

Media Attached

15:35 - 16:00
Talk

Is Sound Gradual Typing Dead?

Asumu TakikawaNortheastern University, Daniel FelteyNortheastern University, Ben GreenmanNortheastern University, Max New, Jan VitekNortheastern University, Matthias FelleisenNortheastern University

Pre-print Media Attached File Attached

16:30 - 17:45: Research Papers - Track 1: Optimization at Grand Bay North
Chair(s): Mayur NaikGeorgia Tech

16:30 - 16:55
Talk

SMO: An Integrated Approach to Intra-Array and Inter-Array Storage Optimization

Somashekaracharya G BhaskaracharyaIndian Institute of Science and National Instruments, Uday BondhugulaIndian Institute of Science, Albert CohenINRIA

Media Attached File Attached

16:55 - 17:20
Talk

PolyCheck: Dynamic Verification of Iteration Space Transformations on Affine Programs

Wenlei Bao, Sriram KrishnamoorthyPacific Northwest National Laboratories, Louis-Noel PouchetOhio State University, Fabrice RastelloINRIA, France, P. SadayappanOhio State University

Media Attached

17:20 - 17:45
Talk

Printing Floating-Point Numbers: A Faster, Always Correct Method

Marc AndryscoUniversity of California, San Diego, Ranjit JhalaUniversity of California, San Diego, Sorin LernerUniversity of California, San Diego

Media Attached

16:30 - 17:45: Research Papers - Track 2: Sessions and processes at Grand Bay South
Chair(s): Matteo MaffeiSaarland University

16:30 - 16:55
Talk

Effects as sessions, sessions as effects

Dominic OrchardImperial College London, Nobuko YoshidaImperial College London, UK

Pre-print Media Attached

16:55 - 17:20
Talk

Monitors and Blame Assignment for Higher-Order Session Types

Limin JiaCarnegie Mellon University, Hannah GommerstadtCarnegie Mellon University, Frank PfenningCarnegie Mellon University

Media Attached File Attached

17:20 - 17:45
Talk

Environmental Bisimulations for Probabilistic Higher-Order Languages

Davide SangiorgiUniversity of Bologna, Valeria VignudelliUniversity of Bologna/INRIA

Media Attached

18:00 - 19:00: Research Papers - SIGPLAN Awards; Program Chair's Report; and SIGPLAN Business Meeting at Grand Bay North
Chair(s): Michael HicksUniversity of Maryland at College Park, USA

Fri 22 Jan

10:30 - 12:10: Research Papers - Track 1: Program Design and Analysis at Grand Bay North
Chair(s): Manu SridharanSamsung Research America

10:30 - 10:55
Talk

Newtonian Program Analysis via Tensor Product

Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc., Emma TuretskyCS Dept., Univ. of Wisconsin-Madison, Prathmesh PrabhuGoogle

Media Attached

10:55 - 11:20
Talk

Casper: An Efficient Approach to Call Trace Collection

Rongxin WuDepartment of Computer Science and Engineering, The Hong Kong University of Science and Technology, Xiao XiaoThe Hong Kong University of Science and Technology, Shing-Chi CheungDepartment of Computer Science and Engineering, The Hong Kong University of Science and Technology, Hongyu ZhangMicrosoft Research, Charles ZhangHKUST

Media Attached

11:20 - 11:45
Talk

Pushdown Control-flow Analysis for Free

Thomas GilrayUniversity of Utah, Steven Lyde, Michael D. AdamsUniversity of Utah, Matthew MightUniversity of Utah, USA, David Van HornUniversity of Maryland, College Park

Pre-print Media Attached

11:45 - 12:10
Talk

Binding as Sets of Scopes

Matthew FlattUniversity of Utah

Pre-print Media Attached

10:30 - 12:10: Research Papers - Track 2: Semantics and memory models at Grand Bay South
Chair(s): Alexey GotsmanIMDEA

10:30 - 10:55
Talk

Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA

Shaked FlurUniversity of Cambridge, Kathryn E. GrayUniversity of Cambridge, Christopher PulteUniversity of Cambridge, Susmit SarkarUniversity of St Andrews, Luc MarangetINRIA Rocquencourt, Ali SezginUniversity of Cambridge, Will DeaconARM Ltd., Peter SewellUniversity of Cambridge

Media Attached File Attached

10:55 - 11:20
Talk

A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions

Jean Pichon-PharabodUniversity of Cambridge, Peter SewellUniversity of Cambridge

File Attached

11:20 - 11:45
Talk

Overhauling SC atomics in C11 and OpenCL

John WickersonImperial College London, Mark BattyUniversity of Cambridge, Alastair DonaldsonImperial College London

Pre-print File Attached

11:45 - 12:10
Talk

Taming Release-Acquire Consistency

Ori LahavMPI-SWS, Nick GiannarakisMPI-SWS, Viktor VafeiadisMPI-SWS, Germany

Pre-print Media Attached File Attached

14:20 - 16:00: Research Papers - Track 1: Synthesis at Grand Bay North
Chair(s): Roberto GiacobazziUniversity of Verona, Italy

14:20 - 14:45
Talk

Learning Programs from Noisy Data

Veselin RaychevETH Zurich, Pavol BielikETH Zurich, Switzerland, Martin VechevETH Zurich, Andreas KrauseETH Zurich

Link to publication DOI Pre-print Media Attached File Attached

14:45 - 15:10
Talk

Optimizing Synthesis with Metasketches

James BornholtUniversity of Washington, Emina TorlakUniversity of Washington, Dan GrossmanUniversity of Washington, USA, Luis CezeUniversity of Washington, USA

Pre-print Media Attached

15:10 - 15:35
Talk

Maximal Specification Synthesis

Aws AlbarghouthiUniversity of Wisconsin–Madison, Isil DilligUniversity of Texas, Austin, Arie GurfinkelCarnegie Mellon University

Pre-print Media Attached

15:35 - 16:00
Talk

Example-Directed Synthesis: A Type-Theoretic Interpretation

Jonathan FranklePrinceton University, Peter-Michael OseraGrinnell College, David WalkerPrinceton University, Steve ZdancewicUniversity of Pennsylvania

Pre-print Media Attached File Attached

14:20 - 15:35: Research Papers - Track 2: Foundations of Model Checking at Grand Bay South
Chair(s): Alexandra SilvaRadboud University Nijmegen

14:20 - 14:45
Talk

Lattice-Theoretic Progress Measures and Coalgebraic Model Checking

Ichiro HasuoUniversity of Tokyo, Shunsuke ShimizuUniversity of Tokyo, Corina CirsteaUniversity of Southampton

Media Attached

14:45 - 15:10
Talk

Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components

Krishnendu ChatterjeeIST Austria, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, Andreas Pavlogiannis

Media Attached

15:10 - 15:35
Talk

Memoryful Geometry of Interaction II: Recursion and Adequacy

Koko MuroyaUniversity of Tokyo, Naohiko HoshinoKyoto University, Ichiro HasuoUniversity of Tokyo

Media Attached

Call for Papers

Scope

The annual Symposium on Principles of Programming Languages is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome, on topics ranging from formal frameworks to experience reports. Papers discussing new ideas and new areas are encouraged, as are papers (often called "pearls") that elucidate existing concepts in ways that yield new insights. We are looking for any submission with the potential to make enduring contributions to the theory, design, implementation or application of programming languages.

Evaluation

The program committee will evaluate the technical contribution of each submission as well as its accessibility to both experts and the general POPL audience. All papers will be judged on significance, originality, relevance, correctness, and clarity.

Explaining a known idea in a new way may make as strong a contribution as inventing a new idea. Hence, we encourage the submission of pearls: elegant essays that explain an old idea, but do so in a new way that clarifies the idea and yields new insights. There is no formal separation of categories; pearls will be held to the same standards as any other paper.

Each paper should explain its contributions in both general and technical terms, identifying what has been accomplished, explaining why it is significant, and comparing it with previous work. Authors should strive to make their papers understandable to a broad audience. Advice on writing technical papers can be found on the SIGPLAN author information page.

A document that details principles underlying organizational and reviewing policies can be found here.

A document containing frequently asked questions about the reviewing and submission process, especially as it pertains to double-blind reviewing, can be found here.

Important Dates

Paper registration	3 July 2015, AOE
Paper submission	10 July 2015, AOE
Submission URL	https://popl16.hotcrp.com/
Author response period	17 September, 12:00 noon CET - 20 September, 11:00pm CET
Author notification	05 October 2015
Camera-ready deadline	05 November 2015
Main conference	20-22 January 2016
Co-located events	17-19, 23 January 2016

Submission guidelines

Prior to the registration deadline, the authors will register their paper by uploading information on the submission title, abstract (of at most 300 words), authors, topics, and conflicts to the conference web site. Papers that are not registered on time will be rejected.

Prior to the final paper submission deadline, the authors will upload their full paper in double blind format and formatted according to the ACM proceedings format. Each paper should have no more than 12 pages of text, excluding bibliography, in at least 9 pt format. Papers may be resubmitted multiple times up until the deadline. The last version submitted before the deadline will be the version that is reviewed. Papers that exceed the length requirement or are submitted late will be rejected. All deadlines are firm.

We encourage authors to provide any supplementary material that is required to support the claims made in the paper, such as detailed proofs, proof scripts, or experimental data. These materials should be uploaded at submission time, as a single pdf or a tarball, not via a URL. It will be made available to reviewers only after they have submitted their first-draft reviews and hence need not be anonymized. Reviewers are under no obligation to look at the supplementary material but may refer to it if they have questions about the material in the body of the paper.

Templates for ACM format are available for Word Perfect, Microsoft Word, and LaTeX at http://www.sigplan.org/Resources/Author (use the 9 pt preprint template). Submissions should be in PDF and printable on US Letter and A4 sized paper.

Submitted papers must adhere to the SIGPLAN Republication Policy and the ACM Policy on Plagiarism. Concurrent submissions to other conferences, workshops, journals, or similar forums of publication are not allowed.

AUTHORS TAKE NOTE: The official publication date is the date the proceedings are made available in the ACM Digital Library. This date may be up to two weeks prior to the first day of your conference. The official publication date affects the deadline for any patent filings related to published work. (For those rare conferences whose proceedings are published in the ACM Digital Library after the conference is over, the official publication date remains the first day of the conference.)

POPL 2016 will employ a lightweight double-blind reviewing process. To facilitate this, submitted papers must adhere to two rules:

author names and institutions must be omitted, and
references to authors' own related work should be in the third person (e.g., not "We build on our previous work ..." but rather "We build on the work of ...").

The purpose of this process is to help the PC and external reviewers come to an initial judgement about the paper without bias, not to make it impossible for them to discover the authors if they were to try. Nothing should be done in the name of anonymity that weakens the submission or makes the job of reviewing the paper more difficult (e.g., important background references should not be omitted or anonymized). In addition, authors should feel free to disseminate their ideas or draft versions of their paper as they normally would. For instance, authors may post drafts of their papers on the web or give talks on their research ideas. David Walker has put together a document answering frequently asked questions that should address many common concerns.

ARTIFACT EVALUATION: Authors of accepted papers will be invited to formally submit supporting materials to the Artifact Evaluation process. Artifact Evaluation is run by a separate committee whose task is to assess how the artifacts support the work described in the papers. This submission is voluntary and will not influence the final decision regarding the papers. Papers that go through the Artifact Evaluation process successfully will receive a seal of approval printed on the papers themselves. Additional information is to be found on the POPL AEC web page. Authors of accepted papers are encouraged to make these materials publicly available upon publication of the proceedings, by including them as "source materials" in the ACM Digital Library.

Accepted Papers

	Title
	'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, Marc Shapiro Media Attached
	A Program Logic for Concurrent Objects under Fair Scheduling Hongjin Liang, Xinyu Feng Media Attached
	A Theory of Effects and Resources: Adjunction Models and Polarised Calculi Pierre-Louis Curien, Marcelo Fiore, Guillaume Munch-Maccagnoni
	A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions Jean Pichon-Pharabod, Peter Sewell File Attached
	Abstracting Gradual Typing Ronald Garcia, Alison M. Clark, Éric Tanter Link to publication Media Attached
	Abstraction Refinement Guided by a Learnt Probabilistic Model Radu Grigore, Hongseok Yang Media Attached
	Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs Krishnendu Chatterjee, Hongfei Fu, Rouzbeh Hasheminezhad, Petr Novotny Media Attached
	Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth Components Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, Andreas Pavlogiannis Media Attached
	Binding as Sets of Scopes Matthew Flatt Pre-print Media Attached
	Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega Matt Brown, Jens Palsberg Media Attached File Attached
	Casper: An Efficient Approach to Call Trace Collection Rongxin Wu, Xiao Xiao, Shing-Chi Cheung, Hongyu Zhang, Charles Zhang Media Attached
	Certified Causally Consistent Distributed Key-Value Stores Mohsen Lesani, Christian J. Bell, Adam Chlipala Media Attached
	Combining Static Analysis with Probabilistic Models to Enable Market-Scale Analysis Damien Octeau, Somesh Jha, Matthew Dering, Patrick McDaniel, Alexandre Bartel, Hongyu Li, Jacques Klein, Yves Le Traon Media Attached
	Decidability of Inferring Inductive Invariants Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, Mooly Sagiv Media Attached
	Dependent Types and Multi-Monadic Effects in F* Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoué, Santiago Zanella-Béguelin Pre-print Media Attached
	Effects as sessions, sessions as effects Dominic Orchard, Nobuko Yoshida Pre-print Media Attached
	Environmental Bisimulations for Probabilistic Higher-Order Languages Davide Sangiorgi, Valeria Vignudelli Media Attached
	Estimating types in binaries using predictive modeling Omer Katz, Ran El-Yaniv, Eran Yahav Media Attached File Attached
	Example-Directed Synthesis: A Type-Theoretic Interpretation Jonathan Frankle, Peter-Michael Osera, David Walker, Steve Zdancewic Pre-print Media Attached File Attached
	Fabular: Regression Formulas as Probabilistic Programming Johannes Borgström, Andrew D. Gordon, Long Ouyang, Claudio Russo, Adam Ścibior, Marcin Szymczak Media Attached
	From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes Ed Robbins, Andy King, Tom Schrijvers Media Attached
	Fully-Abstract Compilation by Approximate Back-Translation Dominique Devriese, Marco Patrignani, Frank Piessens Pre-print Media Attached
	Is Sound Gradual Typing Dead? Asumu Takikawa, Daniel Feltey, Ben Greenman, Max New, Jan Vitek, Matthias Felleisen Pre-print Media Attached File Attached
	Kleenex: Compiling Nondeterministic Transducers to Deterministic Streaming Transducers Bjørn Bugge Grathwohl, Fritz Henglein, Ulrik Terp Rasmussen, Kristoffer Aalund Søholm, Sebastian Paaske Tørholm Media Attached
	Lattice-Theoretic Progress Measures and Coalgebraic Model Checking Ichiro Hasuo, Shunsuke Shimizu, Corina Cirstea Media Attached
	Learning Invariants using Decision Trees and Implication Counterexamples Pranav Garg, Daniel Neider, P. Madhusudan, Dan Roth Media Attached
	Learning Programs from Noisy Data Veselin Raychev, Pavol Bielik, Martin Vechev, Andreas Krause Link to publication DOI Pre-print Media Attached File Attached
	Lightweight Verification of Separate Compilation Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis Media Attached File Attached
	Maximal Specification Synthesis Aws Albarghouthi, Isil Dillig, Arie Gurfinkel Pre-print Media Attached
	Memoryful Geometry of Interaction II: Recursion and Adequacy Koko Muroya, Naohiko Hoshino, Ichiro Hasuo Media Attached
	Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates James Brotherston, Nikos Gorogiannis, Max Kanovich, Reuben Rowe
	Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Luc Maranget, Ali Sezgin, Will Deacon, Peter Sewell Media Attached File Attached
	Monitors and Blame Assignment for Higher-Order Session Types Limin Jia, Hannah Gommerstadt, Frank Pfenning Media Attached File Attached
	Newtonian Program Analysis via Tensor Product Thomas Reps, Emma Turetsky, Prathmesh Prabhu Media Attached
	Optimizing Synthesis with Metasketches James Bornholt, Emina Torlak, Dan Grossman, Luis Ceze Pre-print Media Attached
	Overhauling SC atomics in C11 and OpenCL John Wickerson, Mark Batty, Alastair Donaldson Pre-print File Attached
	PSync: a partially synchronous language for fault-tolerant distributed algorithms Cezara Drăgoi, Thomas A. Henzinger, Damien Zufferey Link to publication DOI Pre-print Media Attached File Attached
	PolyCheck: Dynamic Verification of Iteration Space Transformations on Affine Programs Wenlei Bao, Sriram Krishnamoorthy, Louis-Noel Pouchet, Fabrice Rastello, P. Sadayappan Media Attached
	Principal Type Inference for GADTs Sheng Chen, Martin Erwig Media Attached
	Printing Floating-Point Numbers: A Faster, Always Correct Method Marc Andrysco, Ranjit Jhala, Sorin Lerner Media Attached
	Prophet: Automatic Patch Generation via Learning from Successful Patches Fan Long, Martin Rinard Media Attached
	Pushdown Control-flow Analysis for Free Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, David Van Horn Pre-print Media Attached
	Query-Guided Maximum Satisfiability Xin Zhang, Ravi Mangal, Aditya Nori, Mayur Naik File Attached
	Reducing Crash Recoverability to Reachability Eric Koskinen, Junfeng Yang
	SMO: An Integrated Approach to Intra-Array and Inter-Array Storage Optimization Somashekaracharya G Bhaskaracharya, Uday Bondhugula, Albert Cohen Media Attached File Attached
	Scaling Network Verification using Symmetry and Surgery Gordon Plotkin, Nikolaj Bjørner, Nuno P. Lopes, Andrey Rybalchenko, George Varghese
	Sound Type-dependent Syntactic Language Extension Florian Lorenzen, Sebastian Erdweg Pre-print Media Attached File Attached
	String Solving with Word Equations and Transducers: Decidability and Applications to Detecting Mutation XSS Anthony Widjaja Lin, Pablo Barcelo Media Attached
	Symbolic Abstract Data Type Inference Michael Emmi, Constantin Enea Media Attached
	Symbolic Computation of Differential Equivalences Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin Media Attached
	System Fω with Equirecursive Types for Datatype-generic Programming Yufei Cai, Paolo G. Giarrusso, Klaus Ostermann Media Attached
	Taming Release-Acquire Consistency Ori Lahav, Nick Giannarakis, Viktor Vafeiadis Pre-print Media Attached File Attached
	Temporal Verification of Higher-order Functional Programs Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno
	The Complexity of Interaction Stéphane Gimenez, Georg Moser Media Attached
	The Gradualizer: a methodology and algorithm for generating gradual type systems Matteo Cimini, Jeremy G. Siek Media Attached
	The Hardness of Data Packing Rahman Lavaee, Chen Ding Media Attached
	Transforming Spreadsheet Data Types using Examples Rishabh Singh, Sumit Gulwani Media Attached
	Type Theory in Type Theory using Quotient Inductive Types Thorsten Altenkirch, Ambrus Kaposi Media Attached File Attached
	Unboundedness and Downward Closures of Higher-Order Pushdown Automata Matthew Hague, Jonathan Kochems, C.-H. Luke Ong Media Attached