Giuseppe Castagna, Andrew D. Gordon
Proceedings of the 44th Symposium on Principles of Programming Languages
POPL, 2017.

@proceedings{POPL-2017,
	doi           = "10.1145/3009837",
	editor        = "Giuseppe Castagna and Andrew D. Gordon",
	isbn          = "978-1-4503-4660-3",
	publisher     = "{ACM}",
	title         = "{Proceedings of the 44th Symposium on Principles of Programming Languages}",
	year          = 2017,
}

Contents (66 items)

POPL-2017-Weirich #dependent type

The influence of dependent types (keynote) (SW), p. 1.

POPL-2017-Turon #named #rust

Rust: from POPL to practice (keynote) (AT), p. 2.

POPL-2017-AlglaveC #consistency #modelling #proving

Ogre and Pythia: an invariance proof method for weak consistency models (JA, PC), pp. 3–18.

POPL-2017-GermaneM #analysis #automaton

A posteriori environment analysis with Pushdown Delta CFA (KG, MM), pp. 19–31.

POPL-2017-LiBCR #semantics

Semantic-directed clumping of disjunctive abstract states (HL, FB, BYEC, XR), pp. 32–45.

POPL-2017-SinghPV #abstract domain #performance

Fast polyhedra abstract domain (GS, MP, MTV), pp. 46–59.

POPL-2017-DolanM #morphism #polymorphism #type inference #type system

Polymorphism, subtyping, and type inference in MLsub (SD, AM), pp. 60–72.

POPL-2017-Grigore #java

Java generics are turing complete (RG), pp. 73–85.

POPL-2017-OmarVHAH #bidirectional #calculus #editing #named

Hazelnut: a bidirectionally typed structure editor calculus (CO, IV, MH, JA, MAH), pp. 86–99.

POPL-2017-Crary #abstraction #morphism #parametricity #polymorphism

Modules, abstraction, and parametric polymorphism (KC), pp. 100–113.

POPL-2017-LampropoulosGHH #generative

Beginner's luck: a language for property-based generators (LL, DGW, CH, JH, BCP, LyX), pp. 114–129.

POPL-2017-ShanR

Exact Bayesian inference by symbolic disintegration (CcS, NR), pp. 130–144.

POPL-2017-ChatterjeeNZ #invariant #probability #termination

Stochastic invariants for probabilistic termination (KC, PN0, DZ), pp. 145–160.

POPL-2017-BartheGHS #probability #proving #source code

Coupling proofs are probabilistic product programs (GB, BG, JH, PYS), pp. 161–174.

POPL-2017-KangHLVD #concurrent #semantics

A promising semantics for relaxed-memory concurrency (JK, CKH, OL, VV, DD), pp. 175–189.

POPL-2017-WickersonBSC #automation #consistency #memory management #modelling

Automatically comparing memory consistency models (JW, MB, TS0, GAC), pp. 190–204.

POPL-2017-KrebbersTB #concurrent #higher-order #interactive #logic #proving

Interactive proofs in higher-order concurrent separation logic (RK, AT, LB), pp. 205–217.

POPL-2017-Krogh-Jespersen #concurrent #higher-order #logic #relational

A relational model of types-and-effects in higher-order concurrent separation logic (MKJ, KS, LB), pp. 218–231.

POPL-2017-DAntoniV #finite #higher-order #logic #monad #sequence

Monadic second-order logic on finite sequences (LD, MV), pp. 232–245.

POPL-2017-KobayashiLB #fixpoint #higher-order #logic #on the #recursion

On the relationship between higher-order recursion schemes and higher-order fixpoint logic (NK0, ÉL, FB), pp. 246–259.

POPL-2017-KovacsRV #quantifier #reasoning

Coming to terms with quantified reasoning (LK, SR, AV), pp. 260–270.

POPL-2017-ScullyC #automation #database #optimisation

A program optimization for automatic database result caching (ZS, AC), pp. 271–284.

POPL-2017-KiselyovBPS

Stream fusion, to completeness (OK, AB, NP, YS), pp. 285–299.

POPL-2017-ChiangBBSGR #float

Rigorous floating-point mixed-precision tuning (WFC, MB, IB, AS, GG, ZR), pp. 300–315.

POPL-2017-CicekBG0H #cost analysis #relational

Relational cost analysis (EÇ, GB, MG, DG0, JH0), pp. 316–329.

POPL-2017-MadhavanKK #contract #higher-order #verification

Contract-based resource verification for higher-order functions with memoization (RM, SK, VK), pp. 330–343.

POPL-2017-ZhangS #analysis #data flow #linear #reachability

Context-sensitive data-dependence analysis via linear conjunctive language reachability (QZ, ZS), pp. 344–358.

POPL-2017-HoffmannDW #analysis #automation #bound #ml #towards

Towards automatic resource bound analysis for OCaml (JH0, AD, SCW), pp. 359–373.

POPL-2017-Scherer #equivalence

Deciding equivalence with sums and the empty type (GS), pp. 374–386.

POPL-2017-Ilik #normalisation #representation #similarity

The exp-log normal form of types: decomposing extensional equality and representing terms compactly (DI), pp. 387–399.

POPL-2017-Levy #morphism

Contextual isomorphisms (PBL), pp. 400–414.

POPL-2017-BrownP #self

Typed self-evaluation via intensional type functions (MB, JP), pp. 415–428.

POPL-2017-FlurSPNMGSBS #concurrent

Mixed-size concurrency: ARM, POWER, C/C++11, and SC (SF, SS, CP, KN, LM, KEG, AS, MB, PS), pp. 429–442.

POPL-2017-LidburyD #concurrent #detection

Dynamic race detection for C++11 (CL, AFD), pp. 443–457.

POPL-2017-BrutschyD0V #analysis #consistency

Serializability for eventual consistency: criterion, analysis, and applications (LB, DD, PM0, MTV), pp. 458–472.

POPL-2017-HoenickeMP #composition #concurrent #thread #verification

Thread modularity at many levels: a pearl in compositional verification (JH, RM, AP), pp. 473–485.

POPL-2017-Leijen #algebra #compilation

Type directed compilation of row-typed algebraic effects (DL), pp. 486–499.

POPL-2017-LindleyMM

Do be do be do (SL, CM, CM), pp. 500–514.

POPL-2017-AhmanHMMPPRS #for free #monad

Dijkstra monads for free (DA, CH, KM, GM, GDP, JP, AR, NS), pp. 515–529.

POPL-2017-SekiyamaI #contract

Stateful manifest contracts (TS, AI), pp. 530–544.

POPL-2017-AmorimGHKC #metric #semantics

A semantic account of metric preservation (AAdA, MG, JH, SyK, IC), pp. 545–556.

POPL-2017-SmolkaKFK0 #network #probability #semantics

Cantor meets scott: semantic foundations for probabilistic networks (SS, PK0, NF, DK, AS0), pp. 557–571.

POPL-2017-SubramanianDA #multitenancy #named #network #overview

Genesis: synthesizing forwarding tables in multi-tenant networks (KS, LD, AA), pp. 572–585.

POPL-2017-KopczynskiT #named #semantics #syntax

LOIS: syntax and semantics (EK, ST), pp. 586–598.

POPL-2017-FengM0DR #api #component #synthesis

Component-based synthesis for complex APIs (YF, RM, YW0, ID, TWR), pp. 599–612.

POPL-2017-MoermanS0KS #automaton #learning

Learning nominal automata (JM, MS, AS0, BK, MS), pp. 613–625.

POPL-2017-BouajjaniEGH #consistency #on the #verification

On verifying causal consistency (AB, CE, RG, JH), pp. 626–638.

POPL-2017-SrikanthSH #complexity #theorem #using #verification

Complexity verification using guided theorem enumeration (AS, BS, WRH), pp. 639–652.

POPL-2017-DudenhefnerR #bound #calculus

Intersection type calculi of bounded dimension (AD, JR), pp. 653–665.

POPL-2017-AminR #proving

Type soundness proofs with definitional interpreters (NA, TR), pp. 666–679.

POPL-2017-AngiuliHW #type system

Computational higher-dimensional type theory (CA, RH0, TW), pp. 680–693.

POPL-2017-ChangKG #metaprogramming #type system

Type systems as macros (SC, AK, BG), pp. 694–705.

POPL-2017-KumarBH #array #functional #parallel

Parallel functional arrays (AK, GEB, RH0), pp. 706–718.

POPL-2017-KonnovLVW #algorithm #distributed #fault tolerance #liveness #safety #verification

A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms (IVK0, ML, HV, JW), pp. 719–734.

POPL-2017-LiuYZ #bisimulation #semantics

Analyzing divergence in bisimulation semantics (XL0, TY, WZ), pp. 735–747.

POPL-2017-LangeNTY #liveness #programming #safety

Fencing off go: liveness and safety for channel-based programming (JL, NN, BT, NY), pp. 748–761.

POPL-2017-VitousekSS #collaboration #runtime #type system

Big types in little runtime: open-world soundness and collaborative blame for gradual type systems (MMV, CS, JGS), pp. 762–774.

POPL-2017-LehmannT #refinement

Gradual refinement types (NL, ÉT), pp. 775–788.

POPL-2017-CiminiS #automation #generative #semantics

Automatically generating the dynamic semantics of gradually typed languages (MC, JGS), pp. 789–803.

POPL-2017-JaferyD #nondeterminism

Sums of uncertainty: refinements go gradual (KAJ, JD), pp. 804–817.

POPL-2017-YingYW #generative #invariant #quantum #source code

Invariants of quantum programs: characterisations and generation (MY, SY, XW), pp. 818–832.

POPL-2017-LagoFVY #geometry #parallel #probability #quantum

The geometry of parallelism: classical, probabilistic, and quantum effects (UDL, CF, BV, AY), pp. 833–845.

POPL-2017-Paykin0Z #named #quantum

QWIRE: a core language for quantum circuits (JP, RR0, SZ), pp. 846–858.

POPL-2017-AminR17a #abstraction #named #programming

LMS-Verify: abstraction without regret for verified systems programming (NA, TR), pp. 859–873.

POPL-2017-AssafNSTT #data flow #semantics #static analysis

Hypercollecting semantics and its application to static analysis of information flow (MA, DAN, JS, ET, FT), pp. 874–887.

POPL-2017-ZhangK #automation #difference #named #privacy #proving #towards

LightDP: towards automating differential privacy proofs (DZ, DK), pp. 888–901.