Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID44th 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
a service of 
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-04-22 20:00 CEST 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:
