Proceedings of the 41st 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

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

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

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.

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.