Proceedings of the 43rd Symposium on Principles of Programming Languages
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter

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

PLT
DBLP
Scholar
ACM DL
Full names Links ISxN
@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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.