Suresh Jagannathan, Peter Sewell
Proceedings of the 41st Symposium on Principles of Programming Languages
POPL, 2014.

@proceedings{POPL-2014,
	acmid         = "2535838",
	address       = "San Diego, California, USA",
	editor        = "Suresh Jagannathan and Peter Sewell",
	isbn          = "978-1-4503-2544-8",
	publisher     = "{ACM}",
	title         = "{Proceedings of the 41st Symposium on Principles of Programming Languages}",
	year          = 2014,
}

Contents (55 items)

6 ×#semantics
5 ×#higher-order
5 ×#proving
4 ×#composition
4 ×#named
4 ×#parametricity
4 ×#probability
4 ×#source code
3 ×#analysis
3 ×#fault

POPL-2014-Birkedal #composition #concurrent #higher-order #imperative #reasoning #source code

Modular reasoning about concurrent higher-order imperative programs (LB), pp. 1–2.

POPL-2014-CousotC #abstract interpretation #calculus

A galois connection calculus for abstract interpretation (PC, RC), pp. 3–4.

POPL-2014-Castagna0XILP #evaluation #polymorphism #semantics #syntax

Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation (GC, KN, ZX, HI, SL, LP), pp. 5–18.

POPL-2014-KilpatrickDJM #haskell #interface #named

Backpack: retrofitting Haskell with interfaces (SK, DD, SLPJ, SM), pp. 19–32.

POPL-2014-CasinghinoSW #proving #source code

Combining proofs and programs in a dependently typed language (CC, VS, SW), pp. 33–46.

POPL-2014-DissegnaLR #abstract interpretation #compilation

Tracing compilation by abstract interpretation (SD, FL, FR), pp. 47–60.

POPL-2014-RamsayNO #abstraction #approach #higher-order #model checking #refinement

A type-directed abstraction refinement approach to higher-order model checking (SJR, RPN, CHLO), pp. 61–72.

POPL-2014-CoughlinC #analysis #composition #invariant

Fissile type analysis: modular checking of almost everywhere invariants (DC, BYEC), pp. 73–86.

POPL-2014-BodinCFGMNSS #specification

A trusted mechanised JavaSript specification (MB, AC, DF, PG, SM, DN, AS, GS), pp. 87–100.

POPL-2014-Krebbers #axiom #c #nondeterminism #semantics #sequence

An operational and axiomatic semantics for non-determinism and sequence points in C (RK), pp. 101–112.

POPL-2014-AndersonFGJKSW #named #network #semantics

NetkAT: semantic foundations for networks (CJA, NF, AG, JBJ, DK, CS, DW), pp. 113–126.

POPL-2014-SharmaNA #program analysis #trade-off

Bias-variance tradeoffs in program analysis (RS, AVN, AA), pp. 127–138.

POPL-2014-DSilvaHK #satisfiability

Abstract satisfaction (VD, LH, DK), pp. 139–150.

POPL-2014-FarzanKP #proving

Proofs that count (AF, ZK, AP), pp. 151–164.

POPL-2014-AmorimCDDHPPPT #architecture #data flow

A verified information-flow architecture (AAdA, NC, AD, DD, CH, DP, BCP, RP, AT), pp. 165–178.

POPL-2014-KumarMNO #implementation #ml #named

CakeML: a verified implementation of ML (RK, MOM, MN, SO), pp. 179–192.

POPL-2014-BartheFGSSB #encryption #implementation #probability #relational #verification

Probabilistic relational verification for cryptographic implementations (GB, CF, BG, PYS, NS, SZB), pp. 193–206.

POPL-2014-ChaudhuriCS #proving #synthesis #using

Bridging boolean and quantitative synthesis using smoothed proof search (SC, MC, ASL), pp. 207–220.

POPL-2014-BeyeneCPR #approach #constraints #game studies #graph #infinity

A constraint-based approach to solving games on infinite graphs (TAB, SC, CP, AR), pp. 221–234.

POPL-2014-DarulovaK #compilation

Sound compilation of reals (ED, VK), pp. 235–248.

POPL-2014-HuetH #coq #development #research

30 years of research and development around Coq (GH, HH), pp. 249–250.

POPL-2014-BrookesOR

The essence of Reynolds (SB, PWO, USR), pp. 251–256.

POPL-2014-KuperTKN #parallel #programming

Freeze after writing: quasi-deterministic parallel programming with LVars (LK, AT, NRK, RRN), pp. 257–270.

POPL-2014-BurckhardtGYZ #data type #specification #verification

Replicated data types: specification, verification, optimality (SB, AG, HY, MZ), pp. 271–284.

POPL-2014-BouajjaniEH #consistency #replication #verification

Verifying eventual consistency of optimistic replication systems (AB, CE, JH), pp. 285–296.

POPL-2014-LagoSA #functional #higher-order #induction #on the #probability #source code

On coinductive equivalences for higher-order probabilistic functional programs (UDL, DS, MA), pp. 297–308.

POPL-2014-EhrhardTP #probability

Probabilistic coherence spaces are fully abstract for probabilistic PCF (TE, CT, MP), pp. 309–320.

POPL-2014-GordonGRRBG #named #probability #programming language

Tabular: a schema-driven probabilistic programming language (ADG, TG, NR, CVR, JB, JG), pp. 321–334.

POPL-2014-SergeyVJ #analysis #composition #higher-order #theory and practice

Modular, higher-order cardinality analysis in theory and practice (IS, DV, SLPJ), pp. 335–348.

POPL-2014-ChangF #lazy evaluation #profiling

Profiling for laziness (SC, MF), pp. 349–360.

POPL-2014-CaveFPP #programming

Fair reactive programming (AC, FF, PP, BP), pp. 361–372.

POPL-2014-AbdullaAJS #partial order #reduction

Optimal dynamic partial order reduction (PAA, SA, BJ, KFS), pp. 373–384.

POPL-2014-ItzhakyBILNS #composition #effectiveness #reasoning

Modular reasoning about heap paths via effectively propositional formulas (SI, AB, NI, OL, AN, MS), pp. 385–396.

POPL-2014-ChongDK #abstraction #parallel #reasoning

A sound and complete abstraction for reasoning about parallel prefix sums (NC, AFD, JK), pp. 397–410.

POPL-2014-MillerHKS #authentication #data type

Authenticated data structures, generically (AM, MH, JK, ES), pp. 411–424.

POPL-2014-SwamyFRBCSB #embedded #javascript #type system

Gradual typing embedded securely in JavaScript (NS, CF, AR, KB, JC, PYS, GMB), pp. 425–438.

POPL-2014-LongSKR #fault #generative #integer

Sound input filter generation for integer overflow errors (FL, SSD, DK, MCR), pp. 439–452.

POPL-2014-BrotherstonV #parametricity

Parametric completeness for separation theories (JB, JV), pp. 453–464.

POPL-2014-HouCGT #logic #proving

Proof search for propositional abstract separation logics via labelled sequents (ZH, RC, RG, AT), pp. 465–476.

POPL-2014-LeeP #logic #proving

A proof system for separation logic with magic wand (WL, SP), pp. 477–490.

POPL-2014-Atkey #parametricity #theorem

From parametricity to conservation laws, via Noether’s theorem (RA), pp. 491–502.

POPL-2014-AtkeyGJ #dependent type #parametricity #type system

A relationally parametric model of dependent type theory (RA, NG, PJ), pp. 503–516.

POPL-2014-MurawskiT #game studies #interface #java #semantics

Game semantics for interface middleweight Java (ASM, NT), pp. 517–528.

POPL-2014-JeannetSS #linear

Abstract acceleration of general linear loops (BJ, PS, SS), pp. 529–540.

POPL-2014-DAntoniV #automaton

Minimization of symbolic automata (LD, MV), pp. 541–554.

POPL-2014-ChaudhuriFK #analysis #consistency #source code

Consistency analysis of decision-making programs (SC, AF, ZK), pp. 555–568.

POPL-2014-ZhangM #fault #towards

Toward general diagnosis of static errors (DZ, ACM), pp. 569–582.

POPL-2014-ChenE #debugging #fault #type system

Counter-factual typing for debugging type errors (SC, ME), pp. 583–594.

POPL-2014-BokerHR

Battery transition systems (UB, TAH, AR), pp. 595–606.

POPL-2014-LiAKGC #optimisation #smt

Symbolic optimization with SMT solvers (YL, AA, ZK, AG, MC), pp. 607–618.

POPL-2014-Benton0N #logic

Abstract effects and proof-relevant logical relations (NB, MH, VN), pp. 619–632.

POPL-2014-Katsumata #monad #parametricity #semantics

Parametric effect monads and semantics of effect systems (SyK), pp. 633–646.

POPL-2014-PaganiSV #higher-order #quantum #semantics

Applying quantitative semantics to higher-order quantum computing (MP, PS, BV), pp. 647–658.

POPL-2014-AccattoliBKL #standard #theorem

A nonstandard standardization theorem (BA, EB, DK, CL), pp. 659–670.

POPL-2014-EisenbergVJW #equation #product line

Closed type families with overlapping equations (RAE, DV, SLPJ, SW), pp. 671–684.