![](https://dblp1.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp1.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp1.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
default search action
44th POPL 2017: Paris, France
- Giuseppe Castagna
, Andrew D. Gordon:
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. ACM 2017, ISBN 978-1-4503-4660-3
Keynotes
- Stephanie Weirich:
The influence of dependent types (keynote). 1 - Aaron Turon:
Rust: from POPL to practice (keynote). 2
Abstract Interpretation
- Jade Alglave, Patrick Cousot:
Ogre and Pythia: an invariance proof method for weak consistency models. 3-18 - Kimball Germane
, Matthew Might:
A posteriori environment analysis with Pushdown Delta CFA. 19-31 - Huisong Li, Francois Berenger
, Bor-Yuh Evan Chang
, Xavier Rival:
Semantic-directed clumping of disjunctive abstract states. 32-45 - Gagandeep Singh
, Markus Püschel, Martin T. Vechev:
Fast polyhedra abstract domain. 46-59
Type Systems 1
- Stephen Dolan, Alan Mycroft
:
Polymorphism, subtyping, and type inference in MLsub. 60-72 - Radu Grigore:
Java generics are turing complete. 73-85 - Cyrus Omar, Ian Voysey
, Michael Hilton, Jonathan Aldrich
, Matthew A. Hammer:
Hazelnut: a bidirectionally typed structure editor calculus. 86-99 - Karl Crary:
Modules, abstraction, and parametric polymorphism. 100-113
Probabilistic Programming
- Leonidas Lampropoulos
, Diane Gallois-Wong, Catalin Hritcu, John Hughes, Benjamin C. Pierce, Li-yao Xia:
Beginner's luck: a language for property-based generators. 114-129 - Chung-chieh Shan, Norman Ramsey:
Exact Bayesian inference by symbolic disintegration. 130-144 - Krishnendu Chatterjee, Petr Novotný
, Dorde Zikelic:
Stochastic invariants for probabilistic termination. 145-160 - Gilles Barthe, Benjamin Grégoire, Justin Hsu
, Pierre-Yves Strub:
Coupling proofs are probabilistic product programs. 161-174
Concurrency 1
- Jeehoon Kang
, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis
, Derek Dreyer:
A promising semantics for relaxed-memory concurrency. 175-189 - John Wickerson
, Mark Batty, Tyler Sorensen
, George A. Constantinides:
Automatically comparing memory consistency models. 190-204 - Robbert Krebbers, Amin Timany
, Lars Birkedal:
Interactive proofs in higher-order concurrent separation logic. 205-217 - Morten Krogh-Jespersen, Kasper Svendsen, Lars Birkedal:
A relational model of types-and-effects in higher-order concurrent separation logic. 218-231
Logic
- Loris D'Antoni, Margus Veanes:
Monadic second-order logic on finite sequences. 232-245 - Naoki Kobayashi, Étienne Lozes, Florian Bruse:
On the relationship between higher-order recursion schemes and higher-order fixpoint logic. 246-259 - Laura Kovács
, Simon Robillard, Andrei Voronkov:
Coming to terms with quantified reasoning. 260-270
Compiler Optimisation
- Ziv Scully
, Adam Chlipala:
A program optimization for automatic database result caching. 271-284 - Oleg Kiselyov, Aggelos Biboudis, Nick Palladinos, Yannis Smaragdakis:
Stream fusion, to completeness. 285-299 - Wei-Fan Chiang, Mark Baranowski, Ian Briggs, Alexey Solovyev, Ganesh Gopalakrishnan, Zvonimir Rakamaric:
Rigorous floating-point mixed-precision tuning. 300-315
Program Analysis
- Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Jan Hoffmann:
Relational cost analysis. 316-329 - Ravichandhran Madhavan, Sumith Kulal, Viktor Kuncak:
Contract-based resource verification for higher-order functions with memoization. 330-343 - Qirun Zhang
, Zhendong Su
:
Context-sensitive data-dependence analysis via linear conjunctive language reachability. 344-358 - Jan Hoffmann, Ankush Das, Shu-Chun Weng:
Towards automatic resource bound analysis for OCaml. 359-373
Type Systems 2
- Gabriel Scherer:
Deciding equivalence with sums and the empty type. 374-386 - Danko Ilik
:
The exp-log normal form of types: decomposing extensional equality and representing terms compactly. 387-399 - Paul Blain Levy:
Contextual isomorphisms. 400-414 - Matt Brown, Jens Palsberg:
Typed self-evaluation via intensional type functions. 415-428
Concurrency 2
- Shaked Flur, Susmit Sarkar
, Christopher Pulte
, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, Peter Sewell
:
Mixed-size concurrency: ARM, POWER, C/C++11, and SC. 429-442 - Christopher Lidbury, Alastair F. Donaldson:
Dynamic race detection for C++11. 443-457 - Lucas Brutschy, Dimitar K. Dimitrov, Peter Müller, Martin T. Vechev:
Serializability for eventual consistency: criterion, analysis, and applications. 458-472 - Jochen Hoenicke
, Rupak Majumdar, Andreas Podelski:
Thread modularity at many levels: a pearl in compositional verification. 473-485
Functional Programming with Effects
- Daan Leijen:
Type directed compilation of row-typed algebraic effects. 486-499 - Sam Lindley
, Conor McBride
, Craig McLaughlin
:
Do be do be do. 500-514 - Danel Ahman
, Catalin Hritcu, Kenji Maillard
, Guido Martínez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy:
Dijkstra monads for free. 515-529 - Taro Sekiyama, Atsushi Igarashi
:
Stateful manifest contracts. 530-544
Semantic Foundations
- Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu
, Shin-ya Katsumata
, Ikram Cherigui:
A semantic account of metric preservation. 545-556 - Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, Alexandra Silva
:
Cantor meets scott: semantic foundations for probabilistic networks. 557-571
Logic and Programming
- Kausik Subramanian, Loris D'Antoni, Aditya Akella:
Genesis: synthesizing forwarding tables in multi-tenant networks. 572-585 - Eryk Kopczynski
, Szymon Torunczyk
:
LOIS: syntax and semantics. 586-598
Verification and Synthesis
- Yu Feng
, Ruben Martins, Yuepeng Wang, Isil Dillig, Thomas W. Reps:
Component-based synthesis for complex APIs. 599-612 - Joshua Moerman
, Matteo Sammartino
, Alexandra Silva
, Bartek Klin
, Michal Szynwelski:
Learning nominal automata. 613-625 - Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui
, Jad Hamza:
On verifying causal consistency. 626-638 - Akhilesh Srikanth, Burak Sahin, William R. Harris:
Complexity verification using guided theorem enumeration. 639-652
Type Systems 3
- Andrej Dudenhefner
, Jakob Rehof:
Intersection type calculi of bounded dimension. 653-665 - Nada Amin, Tiark Rompf:
Type soundness proofs with definitional interpreters. 666-679 - Carlo Angiuli
, Robert Harper, Todd Wilson:
Computational higher-dimensional type theory. 680-693 - Stephen Chang
, Alex Knauth
, Ben Greenman
:
Type systems as macros. 694-705
Concurrency 3
- Ananya Kumar, Guy E. Blelloch, Robert Harper:
Parallel functional arrays. 706-718 - Igor V. Konnov
, Marijana Lazic, Helmut Veith, Josef Widder
:
A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. 719-734 - Xinxin Liu, Tingting Yu, Wenhui Zhang:
Analyzing divergence in bisimulation semantics. 735-747 - Julien Lange
, Nicholas Ng, Bernardo Toninho
, Nobuko Yoshida
:
Fencing off go: liveness and safety for channel-based programming. 748-761
Gradual Typing and Contracts
- Michael M. Vitousek, Cameron Swords, Jeremy G. Siek
:
Big types in little runtime: open-world soundness and collaborative blame for gradual type systems. 762-774 - Nico Lehmann, Éric Tanter:
Gradual refinement types. 775-788 - Matteo Cimini, Jeremy G. Siek
:
Automatically generating the dynamic semantics of gradually typed languages. 789-803 - Khurram A. Jafery, Jana Dunfield:
Sums of uncertainty: refinements go gradual. 804-817
Quantum
- Mingsheng Ying
, Shenggang Ying, Xiaodi Wu:
Invariants of quantum programs: characterisations and generation. 818-832 - Ugo Dal Lago
, Claudia Faggian, Benoît Valiron
, Akira Yoshimizu:
The geometry of parallelism: classical, probabilistic, and quantum effects. 833-845 - Jennifer Paykin, Robert Rand
, Steve Zdancewic:
QWIRE: a core language for quantum circuits. 846-858
Security and Privacy
- Nada Amin, Tiark Rompf:
LMS-Verify: abstraction without regret for verified systems programming. 859-873 - Mounir Assaf, David A. Naumann
, Julien Signoles
, Eric Totel, Frédéric Tronel
:
Hypercollecting semantics and its application to static analysis of information flow. 874-887 - Danfeng Zhang
, Daniel Kifer:
LightDP: towards automating differential privacy proofs. 888-901
![](https://dblp1.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.