Fritz Henglein, Stephanie Weirich
Proceedings of the 46th Symposium on Principles of Programming Languages
POPL, 2018.

@proceedings{POPL-2019,
	editor        = "Fritz Henglein and Stephanie Weirich",
	journal       = "{Proceedings of the ACM on Programming Languages}",
	publisher     = "{ACM}",
	title         = "{Proceedings of the 46th Symposium on Principles of Programming Languages}",
	year          = 2018,
}

Contents (77 items)

POPL-2019-KaposiKA #induction

Constructing quotient inductive-inductive types (AK, AK, TA), p. 24.

POPL-2019-CavalloH #induction #type system

Higher inductive types in cubical computational type theory (EC, RH0), p. 27.

POPL-2019-BiernackiPPS #algebra

Abstracting algebraic effects (DB, MP, PP, FS), p. 28.

POPL-2019-BonchiHPSZ #algebra #concurrent #diagrams #linear

Diagrammatic algebra: from linear to concurrent systems (FB, JH, RP, PS, FZ), p. 28.

POPL-2019-ChakrabortyV

Grounding thin-air reads with event structures (SC, VV), p. 28.

POPL-2019-ChatterjeeGOP #algorithm #performance

Efficient parameterized algorithms for data packing (KC, AKG, NO, AP), p. 28.

POPL-2019-DunfieldK #bidirectional #morphism #polymorphism #rank

Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types (JD, NRK), p. 28.

POPL-2019-EmmiE #specification

Weak-consistency specification via visibility relaxation (ME, CE), p. 28.

POPL-2019-GilbertCST

Definitional proof-irrelevance without K (GG, JC, MS, NT), p. 28.

POPL-2019-Hirschowitz #monad #semantics

Familial monads and structural operational semantics (TH), p. 28.

POPL-2019-MorrisM #data type

Abstracting extensible data types: or, rows by any other name (JGM, JM), p. 28.

POPL-2019-ParkHSR #multi #polymorphism #symmetry

Polymorphic symmetric multiple dispatch with variance (GP, JH, GLSJ, SR), p. 28.

POPL-2019-SkorstengaardDB #control flow #encapsulation #linear #named #stack #using

StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities (LS, DD, LB), p. 28.

POPL-2019-AcetoAFIL #branch #linear

Adventures in monitorability: from branching to linear time and back again (LA, AA, AF, AI, KL), p. 29.

POPL-2019-AlonZLY #distributed #learning #named

code2vec: learning distributed representations of code (UA0, MZ, OL, EY), p. 29.

POPL-2019-AndreescuJLM #analysis #correlation

Inferring frame conditions with static correlation analysis (OFA, TPJ, SL, BM), p. 29.

POPL-2019-BaldanKMP #fixpoint #game studies

Fixpoint games on continuous lattices (PB, BK0, CMM, TP), p. 29.

POPL-2019-BatzKKMN #logic #pointer #probability #reasoning #source code

Quantitative separation logic: a logic for reasoning about probabilistic pointer programs (KB, BLK, JPK, CM, TN0), p. 29.

POPL-2019-CastellanY #game studies #semantics

Two sides of the same coin: session types and game semantics: a synchronous side and an asynchronous side (SC, NY), p. 29.

POPL-2019-ClairambaultVW #game studies #programming #quantum #semantics

Game semantics for quantum programming (PC, MdV, GW), p. 29.

POPL-2019-Crary #compilation

Fully abstract module compilation (KC), p. 29.

POPL-2019-CyphertBKR #refinement #static analysis

Refinement of path expressions for static analysis (JC, JB, ZK, TWR), p. 29.

POPL-2019-DudenhefnerR #approximate #bound

Principality and approximation under dimensional bound (AD, JR), p. 29.

POPL-2019-FlorenceYTF #calculus

A calculus for Esterel: if can, can. if no can, no can (SPF, SHY, JAT, RBF), p. 29.

POPL-2019-FowlerLMD

Exceptional asynchronous session types: session types without tiers (SF0, SL, JGM, SD), p. 29.

POPL-2019-GorogiannisOS #detection #theorem

A true positives theorem for a static race detector (NG, PWO, IS), p. 29.

POPL-2019-HungHZYHW #analysis #quantum #robust #source code

Quantitative robustness analysis of quantum programs (SHH, KH, SZ, MY, MH0, XW), p. 29.

POPL-2019-Kavvos #data flow

Modalities, cohesion, and information flow (GAK), p. 29.

POPL-2019-KincaidBCR

Closed forms for numerical loops (ZK, JB, JC, TWR), p. 29.

POPL-2019-KokkeMP #process #semantics

Better late than never: a fully-abstract semantics for classical processes (WK, FM, MP), p. 29.

POPL-2019-LagoVMY #fault #runtime #π-calculus

Intersection types and runtime errors in the pi-calculus (UDL, MdV, DM, AY), p. 29.

POPL-2019-MathurMV #decidability #source code #verification

Decidable verification of uninterpreted programs (UM, PM, MV0), p. 29.

POPL-2019-MiyazakiSI #type inference #type system

Dynamic type inference for gradual Hindley-Milner typing (YM0, TS, AI), p. 29.

POPL-2019-MogelbergV #bisimulation #recursion

Bisimulation as path type for guarded recursive types (REM, NV), p. 29.

POPL-2019-ScalasY #less is more #multi #revisited

Less is more: multiparty session types revisited (AS, NY), p. 29.

POPL-2019-ShiSL #component #named #synthesis

FrAngel: component-based synthesis with control structures (KS, JS, PL), p. 29.

POPL-2019-SpathAB #analysis #automaton #data flow #using

Context-, flow-, and field-sensitive data-flow analysis using synchronized Pushdown systems (JS, KA0, EB), p. 29.

POPL-2019-TomanG #abstract interpretation #framework #named

Concerto: a framework for combined concrete and abstract interpretation (JT, DG), p. 29.

POPL-2019-TouzeauMMR #analysis #performance

Fast and exact analysis for LRU caches (VT, CM, DM, JR), p. 29.

POPL-2019-VakarKS #probability #programming #statistics

A domain theory for statistical probabilistic programming (MV, OK, SS), p. 29.

POPL-2019-WattRPCS #ecosystem #encryption #named #web

CT-wasm: type-driven secure cryptography for the web ecosystem (CW, JR, NP, SC, DS), p. 29.

POPL-2019-YiCMJ #automation #fault #float #library #performance

Efficient automated repair of high floating-point errors in numerical libraries (XY, LC, XM, TJ), p. 29.

POPL-2019-ZhangM

Abstraction-safe effect handlers via tunneling (YZ, ACM), p. 29.

POPL-2019-BaeL #bound #logic #model checking #using

Bounded model checking of signal temporal logic properties using syntactic separation (KB, JL), p. 30.

POPL-2019-BizjakGKB #concurrent #higher-order #logic #named

Iron: managing obligations in higher-order concurrent separation logic (AB, DG, RK, LB), p. 30.

POPL-2019-CastroHJNY #api #communication #distributed #parametricity #programming #static typing #using

Distributed programming using role-parametric session types in go: statically-typed endpoint APIs for dynamically-instantiated communication structures (DCP, RH, SSJ, NN, NY), p. 30.

POPL-2019-ChenHLRW #source code #string

Decision procedures for path feasibility of string-manipulating programs with complex operations (TC, MH, AWL, PR, ZW), p. 30.

POPL-2019-FromherzGHPRS #assembly #performance

A verified, efficient embedding of a verifiable assembly language (AF, NG, CH, BP, AR, NS), p. 30.

POPL-2019-GleissenthallKB #distributed #source code #verification

Pretend synchrony: synchronous verification of asynchronous distributed programs (KvG, RGK, AB, DS, RJ), p. 30.

POPL-2019-GorinovaGS #flexibility #performance #probability #programming

Probabilistic programming with densities in SlicStan: efficient, flexible, and deterministic (MIG, ADG, CAS), p. 30.

POPL-2019-Mellies #category theory #combinator #game studies #scheduling #semantics

Categorical combinatorics of scheduling and synchronization in game semantics (PAM), p. 30.

POPL-2019-ParkerVH #data flow #multi #named #security #web

LWeb: information flow security for multi-tier web applications (JP, NV, MH0), p. 30.

POPL-2019-PolikarpovaS #source code #synthesis

Structuring the synthesis of heap-manipulating programs (NP, IS), p. 30.

POPL-2019-SatoABGGH #approximate #convergence #higher-order #optimisation #probability #reasoning #source code #verification

Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization (TS, AA0, GB, MG, DG0, JH), p. 30.

POPL-2019-SinghGPV #abstract domain #network

An abstract domain for certifying neural networks (GS, TG, MP, MTV), p. 30.

POPL-2019-TassarottiH #concurrent #logic #random #source code

A separation logic for concurrent randomized programs (JT, RH0), p. 30.

POPL-2019-ToroLT #parametricity #revisited

Gradual parametricity, revisited (MT, EL, ÉT), p. 30.

POPL-2019-WangH #generative #worst-case

Type-guided worst-case input generation (DW, JH0), p. 30.

POPL-2019-WangWS #approach #compilation #composition #stack

An abstract stack based approach to verified compositional compilation to machine code (YW, PW, ZS), p. 30.

POPL-2019-AlurMS #composition #monitoring

Modular quantitative monitoring (RA, KM, CS), p. 31.

POPL-2019-ArmstrongBCRGNM #semantics

ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS (AA, TB, BC0, AR, KEG, RMN, PM, MW, JF, CP, SF, IS, NK, PS), p. 31.

POPL-2019-BodinGJS #semantics

Skeletal semantics and their interpretations (MB, PG, TPJ, AS), p. 31.

POPL-2019-CousotGR #named

A²I: abstract² interpretation (PC, RG, FR), p. 31.

POPL-2019-MeyerW #data type #memory management #static analysis

Decoupling lock-free data structures from memory reclamation for static analysis (RM0, SW), p. 31.

POPL-2019-NewLA #type system

Gradual type theory (MSN, DRL, AA), p. 31.

POPL-2019-PodkopaevLV #hardware #memory management #modelling #programming language

Bridging the gap between programming languages and hardware weak memory models (AP, OL, VV), p. 31.

POPL-2019-RaadDRLV #concurrent #consistency #correctness #declarative #library #memory management #modelling #on the #specification #verification

On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models (AR, MD, LR, OL, VV), p. 31.

POPL-2019-SantosMSG #composition #execution #javascript #symbolic computation

JaVerT 2.0: compositional symbolic execution for JavaScript (JFS, PM, GS, PG), p. 31.

POPL-2019-SmithHA #abstraction #probability

Trace abstraction modulo probability (CS, JH, AA), p. 31.

POPL-2019-Unruh #hoare #logic #quantum #relational

Quantum relational Hoare logic (DU), p. 31.

POPL-2019-VassenaRGRS #data flow #information management

From fine- to coarse-grained dynamic information flow control and back (MV, AR, DG0, VR, DS), p. 31.

POPL-2019-CastagnaLPS #perspective #type system

Gradual typing: a new perspective (GC, VL, TP, JGS), p. 32.

POPL-2019-HoushmandL #analysis #coordination #named #replication #synthesis

Hamsaz: replication coordination analysis and synthesis (FH, ML), p. 32.

POPL-2019-MemarianGDKRWS #c #pointer #semantics

Exploring C semantics and pointer provenance (KM, VBFG, BD, SK, AR, RNMW, PS), p. 32.

POPL-2019-OmarVCH #functional #programming

Live functional programming with typed holes (CO, IV, RC, MAH), p. 32.

POPL-2019-SaadCSRM #automation #modelling #probability #source code #synthesis

Bayesian synthesis of probabilistic programs for automatic data modeling (FAS, MFCT, US, MCR, VKM), p. 32.

POPL-2019-BlanchetteGPT #bound

Bindings as bounded natural functors (JCB, LG, AP0, DT), p. 34.