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

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

PLT
no DBLP info
Scholar
Full names Links ISxN
@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.

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.