Roberto Giacobazzi, Radhia Cousot
Proceedings of the 40th Annual Symposium on Principles of Programming Languages
POPL, 2013.

@proceedings{POPL-2013,
	acmid         = "2429069",
	address       = "Rome, Italy",
	editor        = "Roberto Giacobazzi and Radhia Cousot",
	isbn          = "978-1-4503-1832-7",
	publisher     = "{ACM}",
	title         = "{Proceedings of the 40th Annual Symposium on Principles of Programming Languages}",
	year          = 2013,
}

Contents (47 items)

5 ×#concurrent
4 ×#abstraction
4 ×#named
3 ×#automation
3 ×#data type
3 ×#logic
3 ×#programming
3 ×#proving
3 ×#semantics
3 ×#source code

POPL-2013-Gonthier #order #proving #theorem

Engineering mathematics: the odd order theorem proof (GG), pp. 1–2.

POPL-2013-LoschP #abstraction

Full abstraction for nominal Scott domains (SL, AMP), pp. 3–14.

POPL-2013-Tate #semantics

The sequential semantics of producer effect systems (RT), pp. 15–26.

POPL-2013-AbelPTS #infinity #named #pattern matching #programming

Copatterns: programming infinite structures by observations (AA, BP, DT, AS), pp. 27–38.

POPL-2013-BlellochH #algorithm #functional

Cache and I/O efficent functional algorithms (GEB, RH), pp. 39–50.

POPL-2013-Ben-AmramG #constraints #integer #linear #on the #problem #ranking

On the linear ranking problem for integer linear-constraint loops (AMBA, SG), pp. 51–62.

POPL-2013-MayrC #automaton

Advanced automata minimization (RM, LC), pp. 63–74.

POPL-2013-UnnoTK #automation #functional #higher-order #source code #verification

Automating relatively complete verification of higher-order functional programs (HU, TT, NK), pp. 75–86.

POPL-2013-AtkeyJK #abstraction #algebra

Abstraction and invariance for algebraically indexed types (RA, PJ, AK), pp. 87–100.

POPL-2013-BenzakenCNS #semantics

Static and dynamic semantics of NoSQL languages (VB, GC, KN, JS), pp. 101–114.

POPL-2013-CernyHR #abstraction #refinement

Quantitative abstraction refinement (PC, TAH, AR), pp. 115–128.

POPL-2013-FarzanKP #data flow #graph #induction

Inductive data flow graphs (AF, ZK, AP), pp. 129–142.

POPL-2013-DSilvaHK #learning

Abstract conflict driven learning (VD, LH, DK), pp. 143–154.

POPL-2013-Goyet #calculus

The λ λ-Bar calculus: a dual calculus for unconstrained strategies (AG), pp. 155–166.

POPL-2013-LagoP #geometry

The geometry of types (UDL, BP), pp. 167–178.

POPL-2013-StatonL #programming language

Universal properties of impure programming languages (SS, PBL), pp. 179–192.

POPL-2013-HurNDV #induction #power of #proving

The power of parameterization in coinductive proof (CKH, GN, DD, VV), pp. 193–206.

POPL-2013-DelawareOS

Meta-theory à la carte (BD, BCdSO, TS), pp. 207–218.

POPL-2013-ParkSP #proving #theorem proving

A theorem prover for Boolean BI (JP, JS, SP), pp. 219–232.

POPL-2013-Krishnamurthi #programming language

From principles to programming languages (and back) (SK), pp. 233–234.

POPL-2013-BattyDG #abstraction #c #c++ #concurrent #library

Library abstraction for C/C++ concurrency (MB, MD, AG), pp. 235–248.

POPL-2013-RamalingamV #fault tolerance

Fault tolerance via idempotence (GR, KV), pp. 249–262.

POPL-2013-CarboneM #multi #named #programming

Deadlock-freedom-by-design: multiparty asynchronous global programming (MC, FM), pp. 263–274.

POPL-2013-CairesS #behaviour

The type discipline of behavioral separation (LC, JCS), pp. 275–286.

POPL-2013-Dinsdale-YoungBGPY #composition #concurrent #named #reasoning #source code

Views: compositional reasoning for concurrent programs (TDY, LB, PG, MJP, HY), pp. 287–300.

POPL-2013-JensenBK #logic #low level

High-level separation logic for low-level code (JBJ, NB, AK), pp. 301–314.

POPL-2013-Myers #distributed #how

How languages can save distributed computing (ACM), pp. 315–316.

POPL-2013-HenzingerKPSS #concurrent #data type

Quantitative relaxation of concurrent data structures (TAH, CMK, HP, AS, AS), pp. 317–328.

POPL-2013-DemangeLZJPV #java #memory management

Plan B: a buffered memory model for Java (DD, VL, LZ, SJ, DP, JV), pp. 329–342.

POPL-2013-TuronTABD #concurrent #fine-grained #logic

Logical relations for fine-grained concurrency (AJT, JT, AA, LB, DD), pp. 343–356.

POPL-2013-GaboardiHHNP #dependent type #difference #linear #privacy

Linear dependent types for differential privacy (MG, AH, JH, AN, BCP), pp. 357–370.

POPL-2013-FournetSCDSL #compilation #javascript

Fully abstract compilation to JavaScript (CF, NS, JC, PÉD, PYS, BL), pp. 371–384.

POPL-2013-LivshitsC #automation #classification #security #towards

Towards fully automatic placement of security sanitizers and declassifiers (BL, SC), pp. 385–398.

POPL-2013-Goodman #probability #programming

The principles and practice of probabilistic programming (NDG), pp. 399–402.

POPL-2013-GordonABCGNRR #reasoning

A model-learner pattern for bayesian reasoning (ADG, MA, JB, GC, TG, AVN, SKR, CVR), pp. 403–416.

POPL-2013-SuenagaSH #modelling #standard

Hyperstream processing systems: nonstandard modeling of continuous-time signals (KS, HS, IH), pp. 417–430.

POPL-2013-VytiniotisJCR #haskell #logic #named #semantics

HALO: haskell to logic through denotational semantics (DV, SLPJ, KC, DR), pp. 431–442.

POPL-2013-BotincanB #learning #specification

Sigma*: symbolic learning of input-output specifications (MB, DB), pp. 443–456.

POPL-2013-BonchiP #automaton #bisimulation #congruence #equivalence #nondeterminism

Checking NFA equivalence with bisimulations up to congruence (FB, DP), pp. 457–468.

POPL-2013-KoksalPSBFP #biology #modelling #synthesis

Synthesis of biological models from mutation experiments (ASK, YP, SS, RB, JF, NP), pp. 469–482.

POPL-2013-UpadrastaC #scheduling #using

Sub-polyhedral scheduling using (unit-)two-variable-per-inequality polyhedra (RU, AC), pp. 483–496.

POPL-2013-RompfSABJLJOO #compilation #data type #optimisation #source code #staging

Optimizing data structures in high-level programs: new directions for extensible compilers based on staging (TR, AKS, NA, KJB, VJ, HL, MJ, KO, MO), pp. 497–510.

POPL-2013-Adams #parsing

Principled parsing for indentation-sensitive languages: revisiting landin’s offside rule (MDA), pp. 511–522.

POPL-2013-HoborV #data type

The ramifications of sharing in data structures (AH, JV), pp. 523–536.

POPL-2013-TotlaW

Complete instantiation-based interpolation (NT, TW), pp. 537–548.

POPL-2013-BarrVLS #automation #detection #exception #float

Automatic detection of floating-point exceptions (ETB, TV, VL, ZS), pp. 549–560.

POPL-2013-Ley-WildN #concurrent

Subjective auxiliary state for coarse-grained concurrency (RLW, AN), pp. 561–574.