Ranjit Jhala, Andrew Myers
Proceedings of the 45th Symposium on Principles of Programming Languages
POPL, 2018.

@proceedings{POPL-2018,
	editor        = "Ranjit Jhala and Andrew Myers",
	journal       = "{Proceedings of the ACM on Programming Languages}",
	publisher     = "{ACM}",
	title         = "{Proceedings of the 45th Symposium on Principles of Programming Languages}",
	year          = 2018,
}

Contents (66 items)

POPL-2018-DevriesePP #parametricity

Parametricity versus the universal type (DD, MP, FP), p. 23.

POPL-2018-MajumdarN #debugging #effectiveness #question #random testing #testing #why

Why is random testing effective for partition tolerance bugs? (RM, FN), p. 24.

POPL-2018-BaoKPS #behaviour #modelling #source code

Analytical modeling of cache behavior for affine programs (WB, SK, LNP, PS), p. 26.

POPL-2018-Kuncar0 #higher-order #safety

Safety and conservativity of definitions in HOL and Isabelle/HOL (OK, AP0), p. 26.

POPL-2018-EmmiE #concurrent #monitoring

Sound, complete, and tractable linearizability monitoring for concurrent collections (ME, CE), p. 27.

POPL-2018-BrownP #normalisation #partial evaluation

Jones-optimal partial evaluation by specialization-safe normalization (MB, JP), p. 28.

POPL-2018-BurnOR #higher-order #horn clause #verification

Higher-order constrained horn clauses for verification (TCB, CHLO, SJR), p. 28.

POPL-2018-Danielsson #using

Up-to techniques using sized types (NAD), p. 28.

POPL-2018-EhrhardPT #higher-order #probability #programming

Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming (TE, MP, CT), p. 28.

POPL-2018-FluckigerSYGAV #correctness #optimisation

Correctness of speculative optimizations with dynamic deoptimization (OF, GS, MHY, AG, AA, JV), p. 28.

POPL-2018-GrossmanAGMRSZ #contract #detection #effectiveness #online

Online detection of effectively callback free objects with applications to smart contracts (SG, IA, GGG, YM, NR, MS, YZ), p. 28.

POPL-2018-InalaS #named #spreadsheet #using #web

WebRelate: integrating web data with spreadsheets using examples (JPI, RS), p. 28.

POPL-2018-MazzaPV #approximate

Polyadic approximations, fibrations and intersection types (DM, LP, PV), p. 28.

POPL-2018-McIverMKK #proving #termination

A new proof rule for almost-sure termination (AM, CM, BLK, JPK), p. 28.

POPL-2018-MeloRAP #c #semantics #source code

Inference of static semantics for incomplete C programs (LTCM, RGR, MRdA, FMQP), p. 28.

POPL-2018-SinghPV #abstract domain

A practical construction for decomposing numerical abstract domains (GS, MP, MTV), p. 28.

POPL-2018-TimanySKB #encapsulation #logic #monad #proving

A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST (AT, LS, MKJ, LB), p. 28.

POPL-2018-0001DLC #equivalence #verification

Verifying equivalence of database-driven applications (YW0, ID, SKL, WRC), p. 29.

POPL-2018-0001OV #decidability #type system

Decidability of conversion for type theory in type theory (AA0, JÖ, AV), p. 29.

POPL-2018-0001ST #higher-order #nondeterminism #refinement #source code #type system #verification

Relatively complete refinement type system for verification of higher-order non-deterministic programs (HU0, YS, TT), p. 29.

POPL-2018-Ahman #algebra

Handling fibred algebraic effects (DA), p. 29.

POPL-2018-BartheEGHS #probability #proving #source code

Proving expected sensitivity of probabilistic programs (GB, TE, BG, JH, PYS), p. 29.

POPL-2018-BernardyBNJS #haskell #higher-order #linear #polymorphism

Linear Haskell: practical linearity in a higher-order polymorphic language (JPB, MB, RRN, SPJ, AS), p. 29.

POPL-2018-Campora0EW #migration

Migrating gradual types (JPCI, SC0, ME, EW), p. 29.

POPL-2018-CapriottiK #category theory

Univalent higher categories via complete Semi-Segal types (PC, NK), p. 29.

POPL-2018-ChangKT #execution #symbolic computation

Symbolic types for lenient symbolic execution (SC, AK, ET), p. 29.

POPL-2018-ChenCHLW #constraints #decidability #string #what

What is decidable about string constraints with the ReplaceAll function (TC, YC, MH, AWL, ZW), p. 29.

POPL-2018-ClairambaultGM #higher-order #recursion

Linearity in higher-order recursion schemes (PC, CG, ASM), p. 29.

POPL-2018-DongolJR #architecture #memory management #transaction

Transactions in relaxed memory architectures (BD, RJ, JR), p. 29.

POPL-2018-KoH #axiom #bidirectional #programming

An axiomatic basis for bidirectional programming (HSK, ZH), p. 29.

POPL-2018-LiY #algorithm #analysis #problem #quantum #source code #termination

Algorithmic analysis of termination problems for quantum programs (YL, MY), p. 29.

POPL-2018-OderskyBLBMS #named

Simplicitly: foundations and applications of implicit function types (MO, OB, FL, AB, HM, SS), p. 29.

POPL-2018-PulteFDFSS #axiom #concurrent #modelling #multi

Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8 (CP, SF, WD, JF, SS, PS), p. 29.

POPL-2018-ScibiorKVSYCOMH #higher-order #validation

Denotational validation of higher-order Bayesian inference (AS, OK, MV, SS, HY, YC, KO, SKM, CH, ZG), p. 29.

POPL-2018-TaLKC #automation #logic #synthesis

Automated lemma synthesis in symbolic-heap separation logic (QTT, TCL, SCK, WNC), p. 29.

POPL-2018-AhmanFHMRS

Recalling a witness: foundations and applications of monotonic state (DA, CF, CH, KM, AR, NS), p. 30.

POPL-2018-AlbarghouthiH #difference #privacy #proving

Synthesizing coupling proofs of differential privacy (AA, JH), p. 30.

POPL-2018-BiernackiPPS #algebra #relational

Handle with care: relational interpretation of algebraic effects and handlers (DB, MP, PP, FS), p. 30.

POPL-2018-ChalupaCPSV #partial order #reduction

Data-centric dynamic partial order reduction (MC, KC, AP, NS, KV), p. 30.

POPL-2018-ChatterjeeCP #alias #analysis #data flow #reachability

Optimal Dyck reachability for data-dependence and alias analysis (KC, BC, AP), p. 30.

POPL-2018-FarzanK #game studies #linear #synthesis

Strategy synthesis for linear arithmetic games (AF, ZK), p. 30.

POPL-2018-LampropoulosPP #generative #induction

Generating good generators for inductive relations (LL, ZP, BCP), p. 30.

POPL-2018-LodingMP #proving #quantifier

Foundations for natural proofs and quantifier instantiation (CL, PM, LP), p. 30.

POPL-2018-MiltnerFPWZ #lens

Synthesizing bijective lenses (AM, KF, BCP, DW, SZ), p. 30.

POPL-2018-NguyenGTH #contract #higher-order #source code #verification

Soft contract verification for higher-order stateful programs (PCN, TG, STH, DVH), p. 30.

POPL-2018-SergeyWT #distributed #programming #protocol #proving

Programming and proving with distributed protocols (IS, JRW, ZT), p. 30.

POPL-2018-WangDS #abstraction #refinement #synthesis #using

Program synthesis using abstraction refinement (XW0, ID, RS), p. 30.

POPL-2018-WilliamsR #approach #ml

A principled approach to ornamentation in ML (TW, DR), p. 30.

POPL-2018-KrishnaSW #abstraction #composition #concurrent #data type

Go with the flow: compositional abstractions for concurrent data structures (SK, DES, TW), p. 31.

POPL-2018-LiangF #concurrent

Progress of concurrent objects with partial methods (HL, XF), p. 31.

POPL-2018-VazouTCSNWJ #refinement #smt #verification

Refinement reflection: complete verification with SMT (NV, AT, VC, RGS, RRN, PW, RJ), p. 31.

POPL-2018-AgrawalC0 #approach #performance #probability #ranking #source code #termination

Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs (SA, KC, PN0), p. 32.

POPL-2018-HolikJLRV #constraints #string #transducer

String constraints with concatenation and transducers solved efficiently (LH, PJ, AWL, PR, TV), p. 32.

POPL-2018-Kokologiannakis #c #c++ #concurrent #effectiveness #model checking

Effective stateless model checking for C/C++ concurrency (MK, OL, KS, VV), p. 32.

POPL-2018-Lee0A #automation #correctness #implementation #on the #proving

On automatically proving the correctness of math.h implementations (WL0, RS0, AA), p. 32.

POPL-2018-RadicekBG0Z #cost analysis #monad #relational

Monadic refinements for relational cost analysis (IR, GB, MG, DG0, FZ), p. 32.

POPL-2018-AminR

Collapsing towers of interpreters (NA, TR), p. 33.

POPL-2018-BowmanCRA #continuation

Type-preserving CPS translation of Σ and Π types is not not possible (WJB, YC, NR, AA), p. 33.

POPL-2018-KincaidCBR #invariant #reasoning #synthesis

Non-linear reasoning for invariant synthesis (ZK, JC, JB, TWR), p. 33.

POPL-2018-PadonHLPSS #first-order #liveness #logic #safety

Reducing liveness to safety in first-order logic (OP, JH, GL, AP, MS, SS), p. 33.

POPL-2018-ParreauxVSK #static typing

Unifying analytic and statically-typed quasiquotes (LP, AV, AS, CEK), p. 33.

POPL-2018-SantosMNWG #javascript #named #verification

JaVerT: JavaScript verification toolchain (JFS, PM, DN, TW0, PG), p. 33.

POPL-2018-0002JKD #named #programming language #rust

RustBelt: securing the foundations of the rust programming language (RJ0, JHJ, RK, DD), p. 34.

POPL-2018-ChandraB #named #reasoning #type system

Bonsai: synthesis-based reasoning for type systems (KC, RB), p. 34.

POPL-2018-KakiNNJ #composition #reasoning

Alone together: compositional reasoning and inference for weak isolation (GK, KN, MN, SJ), p. 34.

POPL-2018-PoulsenRTKV #imperative

Intrinsically-typed definitional interpreters for imperative languages (CBP, AR, AT, RK, EV), p. 34.