Rastislav Bodík, Rupak Majumdar
Proceedings of the 43rd Symposium on Principles of Programming Languages
POPL, 2016.

@proceedings{POPL-2016,
	editor        = "Rastislav Bodík and Rupak Majumdar",
	isbn          = "978-1-4503-3549-2",
	publisher     = "{ACM}",
	title         = "{Proceedings of the 43rd Symposium on Principles of Programming Languages}",
	year          = 2016,
}

Contents (62 items)

POPL-2016-McKinley #nondeterminism #programming

Programming the world of uncertain things (keynote) (KSM), pp. 1–2.

POPL-2016-Murray #hybrid #synthesis

Synthesis of reactive controllers for hybrid systems (keynote) (RMM), p. 3.

POPL-2016-Walker #programming language #research

Confluences in programming languages research (keynote) (DW), p. 4.

POPL-2016-BrownP #normalisation #self

Breaking through the normalization barrier: a self-interpreter for f-omega (MB, JP), pp. 5–17.

POPL-2016-AltenkirchK #induction #type system #using

Type theory in type theory using quotient inductive types (TA, AK), pp. 18–29.

POPL-2016-CaiGO #data type #programming #recursion

System f-omega with equirecursive types for datatype-generic programming (YC, PGG, KO), pp. 30–43.

POPL-2016-CurienFM #calculus #formal method #modelling

A theory of effects and resources: adjunction models and polarised calculi (PLC, MPF, GMM), pp. 44–56.

POPL-2016-MuraseT0SU #functional #higher-order #source code #verification

Temporal verification of higher-order functional programs (AM, TT, NK0, RS, HU0), pp. 57–68.

POPL-2016-PlotkinBLRV #network #scalability #symmetry #using #verification

Scaling network verification using symmetry and surgery (GDP, NB, NPL, AR, GV), pp. 69–83.

POPL-2016-BrotherstonGKR #induction #logic #model checking

Model checking for symbolic-heap separation logic with inductive predicates (JB, NG, MIK, RR), pp. 84–96.

POPL-2016-KoskinenY #reachability

Reducing crash recoverability to reachability (EK, JY), pp. 97–108.

POPL-2016-ZhangMNN #satisfiability

Query-guided maximum satisfiability (XZ, RM, AVN, MN), pp. 109–122.

POPL-2016-LinB #equation #logic #string #towards #transducer #word

String solving with word equations and transducers: towards a logic for analysing mutation XSS (AWL, PB), pp. 123–136.

POPL-2016-CardelliTTV #difference #symbolic computation

Symbolic computation of differential equivalences (LC, MT, MT, AV), pp. 137–150.

POPL-2016-HagueKO #automaton #bound #higher-order

Unboundedness and downward closures of higher-order pushdown automata (MH, JK, CHLO), pp. 151–163.

POPL-2016-DevriesePP #approximate #compilation

Fully-abstract compilation by approximate back-translation (DD, MP, FP), pp. 164–177.

POPL-2016-KangKHDV #compilation #lightweight #verification

Lightweight verification of separate compilation (JK, YK, CKH, DD, VV), pp. 178–190.

POPL-2016-RobbinsKS #data type #decompiler #recursion #semantics

From MinX to MinC: semantics-driven decompilation of recursive datatypes (ER, AK, TS), pp. 191–203.

POPL-2016-LorenzenE

Sound type-dependent syntactic language extension (FL, SE), pp. 204–216.

POPL-2016-PadonISKS #decidability #induction #invariant

Decidability of inferring inductive invariants (OP, NI, SS, AK, MS), pp. 217–231.

POPL-2016-Lavaee

The hardness of data packing (RL), pp. 232–242.

POPL-2016-GimenezM #complexity #interactive

The complexity of interaction (SG, GM), pp. 243–255.

POPL-2016-SwamyHKRDFBFSKZ #dependent type #multi

Dependent types and multi-monadic effects in F (NS, CH, CK, AR, ADL, SF, KB, CF, PYS, MK, JKZ, SZB), pp. 256–270.

POPL-2016-BorgstromGORSS #named #probability #programming

Fabular: regression formulas as probabilistic programming (JB, ADG, LO, CVR, AS, MS), pp. 271–283.

POPL-2016-GrathwohlHRST #compilation #named #nondeterminism #streaming #transducer

Kleenex: compiling nondeterministic transducers to deterministic streaming transducers (NBBG, FH, UTR, KAS, SPT), pp. 284–297.

POPL-2016-LongR #automation #generative #learning

Automatic patch generation by learning correct code (FL, MR), pp. 298–312.

POPL-2016-KatzEY #modelling #predict #using

Estimating types in binaries using predictive modeling (OK, REY, EY), pp. 313–326.

POPL-2016-ChatterjeeFNH #algorithm #analysis #probability #problem #source code #termination

Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs (KC, HF0, PN0, RH), pp. 327–342.

POPL-2016-SinghG #data type #spreadsheet #using

Transforming spreadsheet data types using examples (RS, SG), pp. 343–356.

POPL-2016-LesaniBC #consistency #distributed #named

Chapar: certified causally consistent distributed key-value stores (ML, CJB, AC), pp. 357–370.

POPL-2016-GotsmanYFNS #consistency #distributed #reasoning

'Cause I'm strong enough: reasoning about consistency choices in distributed systems (AG, HY, CF0, MN, MS0), pp. 371–384.

POPL-2016-LiangF #concurrent #logic #scheduling

A program logic for concurrent objects under fair scheduling (HL, XF), pp. 385–399.

POPL-2016-DragoiHZ #algorithm #distributed #fault tolerance #named

PSync: a partially synchronous language for fault-tolerant distributed algorithms (CD, TAH, DZ), pp. 400–415.

POPL-2016-0008E #data type #type inference

Principal type inference for GADTs (SC0, ME), pp. 416–428.

POPL-2016-GarciaCT #type system

Abstracting gradual typing (RG, AMC, ÉT), pp. 429–442.

POPL-2016-CiminiS #algorithm #generative #type system

The gradualizer: a methodology and algorithm for generating gradual type systems (MC, JGS), pp. 443–455.

POPL-2016-TakikawaFGNVF #question #type system

Is sound gradual typing dead? (AT, DF, BG, MSN, JV, MF), pp. 456–468.

POPL-2016-OcteauJDMB0KT #android #component #modelling #probability #static analysis

Combining static analysis with probabilistic models to enable market-scale Android inter-component analysis (DO, SJ, MD, PDM, AB, LL0, JK, YLT), pp. 469–484.

POPL-2016-GrigoreY #abstraction #probability #refinement

Abstraction refinement guided by a learnt probabilistic model (RG, HY), pp. 485–498.

POPL-2016-0001NMR #invariant #learning #using

Learning invariants using decision trees and implication counterexamples (PG0, DN, PM, DR), pp. 499–512.

POPL-2016-EmmiE #data type #type inference

Symbolic abstract data type inference (ME, CE), pp. 513–525.

POPL-2016-BhaskaracharyaB #approach #named #optimisation

SMO: an integrated approach to intra-array and inter-array storage optimization (SGB, UB, AC0), pp. 526–538.

POPL-2016-BaoKPRS #named #source code #verification

PolyCheck: dynamic verification of iteration space transformations on affine programs (WB, SK, LNP, FR, PS), pp. 539–554.

POPL-2016-AndryscoJL #float #performance

Printing floating-point numbers: a faster, always correct method (MA, RJ, SL), pp. 555–567.

POPL-2016-OrchardY

Effects as sessions, sessions as effects (DAO, NY), pp. 568–581.

POPL-2016-JiaGP #higher-order #monitoring

Monitors and blame assignment for higher-order session types (LJ, HG, FP), pp. 582–594.

POPL-2016-SangiorgiV #bisimulation #higher-order #probability

Environmental bisimulations for probabilistic higher-order languages (DS, VV), pp. 595–607.

POPL-2016-FlurGPSSMDS #architecture #concurrent #modelling

Modelling the ARMv8 architecture, operationally: concurrency and ISA (SF, KEG, CP, SS, AS, LM, WD, PS), pp. 608–621.

POPL-2016-Pichon-Pharabod #concurrent #optimisation #semantics

A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions (JPP, PS), pp. 622–633.

POPL-2016-BattyDW

Overhauling SC atomics in C11 and OpenCL (MB, AFD, JW), pp. 634–648.

POPL-2016-LahavGV #consistency

Taming release-acquire consistency (OL, NG, VV), pp. 649–662.

POPL-2016-RepsTP #program analysis

Newtonian program analysis via tensor product (TWR, ET, PP), pp. 663–677.

POPL-2016-WuXCZZ #approach #named #performance

Casper: an efficient approach to call trace collection (RW, XX0, SCC, HZ0, CZ), pp. 678–690.

POPL-2016-GilrayL0MH #analysis #automaton #control flow #for free

Pushdown control-flow analysis for free (TG, SL, MDA0, MM, DVH), pp. 691–704.

POPL-2016-Flatt #set

Binding as sets of scopes (MF), pp. 705–717.

POPL-2016-HasuoSC #algebra #metric #model checking

Lattice-theoretic progress measures and coalgebraic model checking (IH, SS, CC), pp. 718–732.

POPL-2016-ChatterjeeGIP #algebra #algorithm #component #concurrent #constant

Algorithms for algebraic path properties in concurrent systems of constant treewidth components (KC, AKG, RIJ, AP), pp. 733–747.

POPL-2016-MuroyaHH #geometry #interactive #recursion

Memoryful geometry of interaction II: recursion and adequacy (KM, NH, IH), pp. 748–760.

POPL-2016-RaychevBVK #learning #semistructured data #source code

Learning programs from noisy data (VR, PB, MTV, AK0), pp. 761–774.

POPL-2016-BornholtTGC #optimisation #sketching #synthesis

Optimizing synthesis with metasketches (JB, ET, DG, LC), pp. 775–788.

POPL-2016-AlbarghouthiDG #specification #synthesis

Maximal specification synthesis (AA, ID, AG), pp. 789–801.

POPL-2016-FrankleOWZ #synthesis

Example-directed synthesis: a type-theoretic interpretation (JF, PMO, DW, SZ), pp. 802–815.