![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
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
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
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.