Brigitte Pientka, Lars Birkedal
Proceedings of the 47th Symposium on Principles of Programming Languages
POPL, 2018.

@proceedings{POPL-2020,
	editor        = "Brigitte Pientka and Lars Birkedal",
	journal       = "{Proceedings of the ACM on Programming Languages}",
	publisher     = "{ACM}",
	title         = "{Proceedings of the 47th Symposium on Principles of Programming Languages}",
	year          = 2018,
}

Contents (68 items)

POPL-2020-BarbarossaM

Taylor subsumes Scott, Berry, Kahn and Plotkin (DB, GM), p. 23.

POPL-2020-ForsterKR #call-by #λ-calculus

The weak call-by-value λ-calculus is reasonable for both time and space (YF0, FK, MR), p. 23.

POPL-2020-AnSMS #relational #synthesis #using

Augmented example-based synthesis using relational perturbation properties (SA, RS, SM, RS), p. 24.

POPL-2020-ClochardMP #deduction #monitoring #verification

Deductive verification with ghost monitors (MC, CM, AP), p. 26.

POPL-2020-BansalNS #coordination #linear #source code #specification #synthesis

Synthesis of coordination programs from linear temporal specifications (SB, KSN, YS), p. 27.

POPL-2020-BeckettGMW #abstract interpretation #distributed #network

Abstract interpretation of distributed network control planes (RB, AG, RM, DW), p. 27.

POPL-2020-BrunelMP #linear #λ-calculus

Backpropagation in the simply typed lambda-calculus with linear negation (AB, DM, MP), p. 27.

POPL-2020-HandleyVH #haskell #reasoning #resource management

Liquidate your assets: reasoning about resource usage in liquid Haskell (MATH, NV, GH), p. 27.

POPL-2020-MackayPAG #decidability #dependent type #type system

Decidable subtyping for path dependent types (JM, AP, JA, LG), p. 27.

POPL-2020-RaghothamanMZNS #datalog #source code #synthesis

Provenance-guided synthesis of Datalog programs (MR, JM, DZ, MN, BS), p. 27.

POPL-2020-VandenbrouckeS #functional #named #probability

PλωNK: functional probabilistic NetKAT (AV, TS), p. 27.

POPL-2020-ZouZXFZS #detection #fault #float

Detecting floating-point errors via atomic conditions (DZ, MZ, YX, ZF, LZ0, ZS), p. 27.

POPL-2020-AbadiP #programming language

A simple differentiable programming language (MA, GDP), p. 28.

POPL-2020-ArntzeniusK #evaluation #functional #higher-order

Seminaïve evaluation for a higher-order functional language (MA, NK), p. 28.

POPL-2020-AschieriG #concurrent #functional #linear #logic #parallel #proving #source code

Par means parallel: multiplicative linear logic proofs as concurrent functional programs (FA, FAG), p. 28.

POPL-2020-BinderJSO #composition #symmetry

Decomposition diversity with symmetric data and codata (DB, JJ, IS, KO), p. 28.

POPL-2020-BruniGGGP #abstract interpretation

Abstract extensionality: on the properties of incomplete abstract interpretations (RB, RG, RG, IGC, DP), p. 28.

POPL-2020-ClairambaultV #abstraction #quantum #λ-calculus

Full abstraction for the quantum lambda-calculus (PC, MdV), p. 28.

POPL-2020-FarzanV #proving #reduction #safety

Reductions for safety proofs (AF, AV), p. 28.

POPL-2020-GuoJJZWJP #abstraction #refinement #synthesis

Program synthesis by type-guided abstraction refinement (ZG, MJ, DJ, JZ, ZW, RJ, NP), p. 28.

POPL-2020-HarkKGK #bound #induction #probability #verification

Aiming low is harder: induction for lower bounds in probabilistic program verification (MH, BLK, JG, JPK), p. 28.

POPL-2020-Jaber #automation #equivalence #higher-order #named #source code

SyTeCi: automating contextual equivalence for higher-order programs with references (GJ), p. 28.

POPL-2020-JonesME #ad hoc #data type

Partial type constructors: or, making ad hoc datatypes less ad hoc (MPJ, JGM, RAE), p. 28.

POPL-2020-PedrotT #how

The fire triangle: how to mix substitution, dependent elimination, and effects (PMP, NT), p. 28.

POPL-2020-SmolkaFHKKS #algebra #linear #source code #testing #verification

Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time (SS, NF, JH, TK, DK, AS0), p. 28.

POPL-2020-SozeauBFTW #coq #exclamation #type checking #verification

Coq Coq correct! verification of type checking and erasure for Coq, in Coq (MS, SB, YF0, NT, TW), p. 28.

POPL-2020-VilhenaPJ #game studies #verification

Spy game: verifying a local generic solver in Iris (PEdV, FP, JHJ), p. 28.

POPL-2020-WangFBCD #visualisation

Visualization by example (CW, YF, RB, AC, ID), p. 28.

POPL-2020-XieEO #data type

Kind inference for datatypes (NX, RAE, BCdSO), p. 28.

POPL-2020-AbdullaAR #verification

Parameterized verification under TSO is PSPACE-complete (PAA, MFA, RR), p. 29.

POPL-2020-AhrensHLM #monad #reduction

Reduction monads and their signatures (BA, AH, AL, MM), p. 29.

POPL-2020-BartheHYYZ #proving #quantum #relational #source code

Relational proofs for quantum programs (GB, JH, MY, NY, LZ), p. 29.

POPL-2020-BiernackiPPS

Binders by day, labels by night: effect instances via lexically scoped handlers (DB, MP, PP, FS), p. 29.

POPL-2020-BourkeBP #compilation #data flow #semantics

Mechanized semantics and verified compilation for a dataflow synchronous language with reset (TB, LB, MP), p. 29.

POPL-2020-ChangBTB #dependent type #metaprogramming #type system

Dependent type systems as macros (SC, MB, MT, WJB), p. 29.

POPL-2020-DahlqvistK #higher-order #probability #semantics #source code

Semantics of higher-order probabilistic programs with conditioning (FD, DK), p. 29.

POPL-2020-DangJKD #memory management

RustBelt meets relaxed memory (HHD, JHJ, JOK, DD), p. 29.

POPL-2020-FeldmanISS #complexity #invariant

Complexity and information in invariant inference (YMYF, NI, MS, SS), p. 29.

POPL-2020-LazarekKSFD #question

Does blame shifting work? (LL, AK, SS, RBF, CD), p. 29.

POPL-2020-MathurMKMV #memory management #safety #source code

Deciding memory safety for single-pass heap-manipulating programs (UM, AM, PK, PM, MV0), p. 29.

POPL-2020-MigeedP #decidability #question #what

What is decidable about gradual types? (ZM, JP), p. 29.

POPL-2020-Pavlogiannis #effectiveness #performance #predict

Fast, sound, and effectively complete dynamic race prediction (AP), p. 29.

POPL-2020-ThiemannV

Label-dependent session types (PT0, VTV), p. 29.

POPL-2020-BartheBGHLPT #c #compilation #verification

Formal verification of a constant-time preserving C compiler (GB, SB, BG, RH, VL, DP, AT), p. 30.

POPL-2020-BartheHL #logic #probability

A probabilistic separation logic (GB, JH, KL), p. 30.

POPL-2020-GreenbergB #execution #semantics

Executable formal semantics for the POSIX shell (MG0, AJB), p. 30.

POPL-2020-HinrichsenBK #logic #named #reasoning

Actris: session-type based reasoning in separation logic (JKH, JB, RK), p. 30.

POPL-2020-HuL #decidability

Undecidability of d<: and its decidable fragments (JZSH, OL), p. 30.

POPL-2020-WangFCDX #probability #proving #random #source code #termination

Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time (PW, HF0, KC, YD, MX), p. 30.

POPL-2020-DaraisSLH

A language for probabilistically oblivious computation (DD, IS, CL0, MH0), p. 31.

POPL-2020-KavvosMLD #call-by #functional #source code

Recurrence extraction for functional programs through call-by-push-value (GAK, EM, DRL, ND), p. 31.

POPL-2020-LiuRSGCKY #abstraction #timeline #verification

Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation (ML0, LR, ZS, RG, DC, JEK, MKY), p. 31.

POPL-2020-RaadWNV #architecture #semantics

Persistency semantics of the Intel-x86 architecture (AR, JW, GN, VV), p. 31.

POPL-2020-SaadFRM #approximate #probability

Optimal approximate sampling from discrete probability distributions (FAS, CEF, MCR, VKM), p. 31.

POPL-2020-SongCKKKH #composition #lightweight #named #verification

CompCertM: CompCert with C-assembly linking and lightweight modular verification (YS, MC, DK, YK, JK, CKH), p. 31.

POPL-2020-JungDKD #alias #rust

Stacked borrows: an aliasing model for Rust (RJ0, HHD, JK, DD), p. 32.

POPL-2020-JungLPRTDJ #logic

The future is ours: prophecy variables in separation logic (RJ0, RL, GP, MR, AT, DD, BJ0), p. 32.

POPL-2020-LewCSCM #probability #programmable #semantics

Trace types and denotational semantics for sound programmable inference in probabilistic languages (AKL, MFCT, BS, MC, VKM), p. 32.

POPL-2020-NewJA #parametricity

Graduality and parametricity: together again for the first time (MSN, DJ, AA), p. 32.

POPL-2020-OHearn #logic

Incorrectness logic (PWO), p. 32.

POPL-2020-SammlerGDL #low level

The high-level benefits of low-level sandboxing (MS, DG0, DD, TL), p. 32.

POPL-2020-WestrickYFA #source code

Disentanglement in nested-parallel programs (SW, RY, MF, UAA), p. 32.

POPL-2020-XiaZHHMPZ #coq #interactive #recursion #representation #source code

Interaction trees: representing recursive and impure programs in Coq (LyX, YZ, PH, CKH, GM, BCP, SZ), p. 32.

POPL-2020-KimVT #fixpoint #parallel

Deterministic parallel fixpoint computation (SKK, AJV, AVT), p. 33.

POPL-2020-LeeYRY #probability #source code #towards

Towards verified stochastic variational inference for probabilistic programs (WL0, HY, XR, HY), p. 33.

POPL-2020-MaillardHRM #logic #relational

The next 700 relational program logics (KM, CH, ER, AVM), p. 33.

POPL-2020-SamakKR

Synthesizing replacement classes (MS, DK, MCR), p. 33.

POPL-2020-MeyerW #data type #lifecycle #memory management #pointer

Pointer life cycle types for lock-free data structures with memory reclamation (RM0, SW), p. 36.