Proceedings of the 44th 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

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

PLT
DBLP
Scholar
DOI
Full names Links ISxN
@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 (, 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.

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.