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
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
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
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
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
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
CakeML: a verified implementation of ML. 179-192 - Gilles Barthe
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
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
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
On coinductive equivalences for higher-order probabilistic functional programs. 297-308 - Thomas Ehrhard, Christine Tasson
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
Modular, higher-order cardinality analysis in theory and practice. 335-348 - Stephen Chang
Profiling for laziness. 349-360 - Andrew Cave, Francisco Ferreira, Prakash Panangaden, Brigitte Pientka:
Fair reactive programming. 361-372
Reasoning
- Parosh Aziz Abdulla, Stavros Aronis
Optimal dynamic partial order reduction. 373-384 - Shachar Itzhaky, Anindya Banerjee
Modular reasoning about heap paths via effectively propositional formulas. 385-396 - Nathan Chong
A sound and complete abstraction for reasoning about parallel prefix sums. 397-410
Security
- Andrew Miller, Michael Hicks
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
Proof search for propositional abstract separation logics via labelled sequents. 465-476 - Wonyeol Lee
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
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
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
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
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
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
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.
last updated on 2024-12-19 22:00 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: