


default search action
41st POPL 2014: San Diego, CA, USA
- Suresh Jagannathan, Peter Sewell

:
The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014. ACM 2014, ISBN 978-1-4503-2544-8
Milner award
- Lars Birkedal

:
Modular reasoning about concurrent higher-order imperative programs. 1-2
SIGPLAN achievement award
- Patrick Cousot, Radhia Cousot:

A Galois connection calculus for abstract interpretation. 3-4
Type system design
- Giuseppe Castagna

, Kim Nguyen, Zhiwu Xu, Hyeonseung Im
, Sergueï Lenglet, Luca Padovani
:
Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation. 5-18 - Scott Kilpatrick, Derek Dreyer, Simon L. Peyton Jones, Simon Marlow:

Backpack: retrofitting Haskell with interfaces. 19-32 - Chris Casinghino, Vilhelm Sjöberg, Stephanie Weirich

:
Combining proofs and programs in a dependently typed language. 33-46
Program analysis 1
- Stefano Dissegna, Francesco Logozzo, Francesco Ranzato:

Tracing compilation by abstract interpretation. 47-60 - Steven J. Ramsay

, Robin P. Neatherway, C.-H. Luke Ong
:
A type-directed abstraction refinement approach to higher-order model checking. 61-72 - Devin Coughlin, Bor-Yuh Evan Chang

:
Fissile type analysis: modular checking of almost everywhere invariants. 73-86
Semantics of systems
- Martin Bodin

, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis
, Daiva Naudziuniene, Alan Schmitt, Gareth Smith:
A trusted mechanised JavaScript specification. 87-100 - Robbert Krebbers:

An operational and axiomatic semantics for non-determinism and sequence points in C. 101-112 - Carolyn Jane Anderson, Nate Foster, Arjun Guha

, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, David Walker
:
NetkAT: semantic foundations for networks. 113-126
Program analysis 2
- Rahul Sharma, Aditya V. Nori, Alex Aiken

:
Bias-variance tradeoffs in program analysis. 127-138 - Vijay Victor D'Silva, Leopold Haller, Daniel Kroening

:
Abstract satisfaction. 139-150 - Azadeh Farzan, Zachary Kincaid

, Andreas Podelski:
Proofs that count. 151-164
Verified systems
- Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange

, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach:
A verified information-flow architecture. 165-178 - Ramana Kumar, Magnus O. Myreen, Michael Norrish

, Scott Owens
:
CakeML: a verified implementation of ML. 179-192 - Gilles Barthe

, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella-Béguelin
:
Probabilistic relational verification for cryptographic implementations. 193-206
Synthesis
- Swarat Chaudhuri, Martin Clochard, Armando Solar-Lezama

:
Bridging boolean and quantitative synthesis using smoothed proof search. 207-220 - Tewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, Andrey Rybalchenko:

A constraint-based approach to solving games on infinite graphs. 221-234 - Eva Darulova

, Viktor Kuncak
:
Sound compilation of reals. 235-248
SIGPLAN software systems award
- Gérard P. Huet, Hugo Herbelin:

30 years of research and development around Coq. 249-250
In memory of John Reynolds
- Stephen Brookes, Peter W. O'Hearn, Uday S. Reddy:

The essence of Reynolds. 251-256
Concurrent programming models
- Lindsey Kuper

, Aaron Turon, Neelakantan R. Krishnaswami, Ryan R. Newton:
Freeze after writing: quasi-deterministic parallel programming with LVars. 257-270 - Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, Marek Zawirski:

Replicated data types: specification, verification, optimality. 271-284 - Ahmed Bouajjani, Constantin Enea, Jad Hamza:

Verifying eventual consistency of optimistic replication systems. 285-296
Probability
- Ugo Dal Lago

, Davide Sangiorgi, Michele Alberti:
On coinductive equivalences for higher-order probabilistic functional programs. 297-308 - Thomas Ehrhard, Christine Tasson

, Michele Pagani:
Probabilistic coherence spaces are fully abstract for probabilistic PCF. 309-320 - Andrew D. Gordon, Thore Graepel, Nicolas Rolland, Claudio V. Russo, Johannes Borgström, John Guiver:

Tabular: a schema-driven probabilistic programming language. 321-334
Functional programming 1
- Ilya Sergey

, Dimitrios Vytiniotis, Simon L. Peyton Jones:
Modular, higher-order cardinality analysis in theory and practice. 335-348 - Stephen Chang

, Matthias Felleisen:
Profiling for laziness. 349-360 - Andrew Cave, Francisco Ferreira, Prakash Panangaden, Brigitte Pientka:

Fair reactive programming. 361-372
Reasoning
- Parosh Aziz Abdulla, Stavros Aronis

, Bengt Jonsson, Konstantinos Sagonas
:
Optimal dynamic partial order reduction. 373-384 - Shachar Itzhaky, Anindya Banerjee

, Neil Immerman, Ori Lahav
, Aleksandar Nanevski, Mooly Sagiv:
Modular reasoning about heap paths via effectively propositional formulas. 385-396 - Nathan Chong

, Alastair F. Donaldson
, Jeroen Ketema:
A sound and complete abstraction for reasoning about parallel prefix sums. 397-410
Security
- Andrew Miller, Michael Hicks

, Jonathan Katz, Elaine Shi:
Authenticated data structures, generically. 411-424 - Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin M. Bierman:

Gradual typing embedded securely in JavaScript. 425-438 - Fan Long, Stelios Sidiroglou-Douskos, Deokhwan Kim, Martin C. Rinard:

Sound input filter generation for integer overflow errors. 439-452
Separation logic
- James Brotherston, Jules Villard

:
Parametric completeness for separation theories. 453-464 - Zhe Hou

, Ranald Clouston, Rajeev Goré, Alwen Tiu:
Proof search for propositional abstract separation logics via labelled sequents. 465-476 - Wonyeol Lee

, Sungwoo Park:
A proof system for separation logic with magic wand. 477-490
Semantic models 1
- Robert Atkey

:
From parametricity to conservation laws, via Noether's theorem. 491-502 - Robert Atkey

, Neil Ghani, Patricia Johann:
A relationally parametric model of dependent type theory. 503-516 - Andrzej S. Murawski

, Nikos Tzevelekos:
Game semantics for interface middleweight Java. 517-528
Program analysis 3
- Bertrand Jeannet, Peter Schrammel

, Sriram Sankaranarayanan:
Abstract acceleration of general linear loops. 529-540 - Loris D'Antoni, Margus Veanes:

Minimization of symbolic automata. 541-554 - Swarat Chaudhuri, Azadeh Farzan, Zachary Kincaid

:
Consistency analysis of decision-making programs. 555-568
Static errors
- Danfeng Zhang

, Andrew C. Myers:
Toward general diagnosis of static errors. 569-582 - Sheng Chen, Martin Erwig

:
Counter-factual typing for debugging type errors. 583-594
Model checking and SMT
- Udi Boker, Thomas A. Henzinger, Arjun Radhakrishna

:
Battery transition systems. 595-606 - Yi Li

, Aws Albarghouthi, Zachary Kincaid
, Arie Gurfinkel
, Marsha Chechik:
Symbolic optimization with SMT solvers. 607-618
Semantic models 2
- Nick Benton, Martin Hofmann, Vivek Nigam:

Abstract effects and proof-relevant logical relations. 619-632 - Shin-ya Katsumata

:
Parametric effect monads and semantics of effect systems. 633-646 - Michele Pagani, Peter Selinger

, Benoît Valiron
:
Applying quantitative semantics to higher-order quantum computing. 647-658
Functional programming 2
- Beniamino Accattoli, Eduardo Bonelli, Delia Kesner, Carlos Lombardi:

A nonstandard standardization theorem. 659-670 - Richard A. Eisenberg

, Dimitrios Vytiniotis, Simon L. Peyton Jones, Stephanie Weirich
:
Closed type families with overlapping equations. 671-684

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














