Abstract is missing.
- The influence of dependent types (keynote)Stephanie Weirich. 1 [doi]
- Rust: from POPL to practice (keynote)Aaron Turon. 2 [doi]
- Ogre and Pythia: an invariance proof method for weak consistency modelsJade Alglave, Patrick Cousot. 3-18 [doi]
- A posteriori environment analysis with Pushdown Delta CFAKimball Germane, Matthew Might. 19-31 [doi]
- Semantic-directed clumping of disjunctive abstract statesHuisong Li, Francois Berenger, Bor-Yuh Evan Chang, Xavier Rival. 32-45 [doi]
- Fast polyhedra abstract domainGagandeep Singh, Markus Püschel, Martin T. Vechev. 46-59 [doi]
- Polymorphism, subtyping, and type inference in MLsubStephen Dolan, Alan Mycroft. 60-72 [doi]
- Java generics are turing completeRadu Grigore. 73-85 [doi]
- Hazelnut: a bidirectionally typed structure editor calculusCyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, Matthew A. Hammer. 86-99 [doi]
- Modules, abstraction, and parametric polymorphismKarl Crary. 100-113 [doi]
- Beginner's luck: a language for property-based generatorsLeonidas Lampropoulos, Diane Gallois-Wong, Catalin Hritcu, John Hughes, Benjamin C. Pierce, Li-yao Xia. 114-129 [doi]
- Exact Bayesian inference by symbolic disintegrationChung-chieh Shan, Norman Ramsey. 130-144 [doi]
- Stochastic invariants for probabilistic terminationKrishnendu Chatterjee, Petr Novotný, Dorde Zikelic. 145-160 [doi]
- Coupling proofs are probabilistic product programsGilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub. 161-174 [doi]
- A promising semantics for relaxed-memory concurrencyJeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer. 175-189 [doi]
- Automatically comparing memory consistency modelsJohn Wickerson, Mark Batty, Tyler Sorensen, George A. Constantinides. 190-204 [doi]
- Interactive proofs in higher-order concurrent separation logicRobbert Krebbers, Amin Timany, Lars Birkedal. 205-217 [doi]
- A relational model of types-and-effects in higher-order concurrent separation logicMorten Krogh-Jespersen, Kasper Svendsen, Lars Birkedal. 218-231 [doi]
- Monadic second-order logic on finite sequencesLoris D'Antoni, Margus Veanes. 232-245 [doi]
- On the relationship between higher-order recursion schemes and higher-order fixpoint logicNaoki Kobayashi, Étienne Lozes, Florian Bruse. 246-259 [doi]
- Coming to terms with quantified reasoningLaura Kovács, Simon Robillard, Andrei Voronkov. 260-270 [doi]
- A program optimization for automatic database result cachingZiv Scully, Adam Chlipala. 271-284 [doi]
- Stream fusion, to completenessOleg Kiselyov, Aggelos Biboudis, Nick Palladinos, Yannis Smaragdakis. 285-299 [doi]
- Rigorous floating-point mixed-precision tuningWei-Fan Chiang, Mark Baranowski, Ian Briggs, Alexey Solovyev, Ganesh Gopalakrishnan, Zvonimir Rakamaric. 300-315 [doi]
- Relational cost analysisEzgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg 0001, Jan Hoffmann. 316-329 [doi]
- Contract-based resource verification for higher-order functions with memoizationRavichandhran Madhavan, Sumith Kulal, Viktor Kuncak. 330-343 [doi]
- Context-sensitive data-dependence analysis via linear conjunctive language reachabilityQirun Zhang, Zhendong Su. 344-358 [doi]
- Towards automatic resource bound analysis for OCamlJan Hoffmann, Ankush Das, Shu-Chun Weng. 359-373 [doi]
- Deciding equivalence with sums and the empty typeGabriel Scherer. 374-386 [doi]
- The exp-log normal form of types: decomposing extensional equality and representing terms compactlyDanko Ilik. 387-399 [doi]
- Contextual isomorphismsPaul Blain Levy. 400-414 [doi]
- Typed self-evaluation via intensional type functionsMatt Brown, Jens Palsberg. 415-428 [doi]
- Mixed-size concurrency: ARM, POWER, C/C++11, and SCShaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, Peter Sewell. 429-442 [doi]
- Dynamic race detection for C++11Christopher Lidbury, Alastair F. Donaldson. 443-457 [doi]
- Serializability for eventual consistency: criterion, analysis, and applicationsLucas Brutschy, Dimitar Dimitrov, Peter Müller 0001, Martin T. Vechev. 458-472 [doi]
- Thread modularity at many levels: a pearl in compositional verificationJochen Hoenicke, Rupak Majumdar, Andreas Podelski. 473-485 [doi]
- Type directed compilation of row-typed algebraic effectsDaan Leijen. 486-499 [doi]
- Do be do be doSam Lindley, Conor McBride, Craig McLaughlin. 500-514 [doi]
- Dijkstra monads for freeDanel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martinez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy. 515-529 [doi]
- Stateful manifest contractsTaro Sekiyama, Atsushi Igarashi. 530-544 [doi]
- A semantic account of metric preservationArthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, Ikram Cherigui. 545-556 [doi]
- Cantor meets scott: semantic foundations for probabilistic networksSteffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, Alexandra Silva 0001. 557-571 [doi]
- Genesis: synthesizing forwarding tables in multi-tenant networksKausik Subramanian, Loris D'Antoni, Aditya Akella. 572-585 [doi]
- LOIS: syntax and semanticsEryk Kopczynski, Szymon Torunczyk. 586-598 [doi]
- Component-based synthesis for complex APIsYu Feng, Ruben Martins, Yuepeng Wang 0001, Isil Dillig, Thomas W. Reps. 599-612 [doi]
- Learning nominal automataJoshua Moerman, Matteo Sammartino, Alexandra Silva 0001, Bartek Klin, Michal Szynwelski. 613-625 [doi]
- On verifying causal consistencyAhmed Bouajjani, Constantin Enea, Rachid Guerraoui, Jad Hamza. 626-638 [doi]
- Complexity verification using guided theorem enumerationAkhilesh Srikanth, Burak Sahin, William R. Harris. 639-652 [doi]
- Intersection type calculi of bounded dimensionAndrej Dudenhefner, Jakob Rehof. 653-665 [doi]
- Type soundness proofs with definitional interpreters Nada Amin, Tiark Rompf. 666-679 [doi]
- Computational higher-dimensional type theoryCarlo Angiuli, Robert Harper, Todd Wilson. 680-693 [doi]
- Type systems as macrosStephen Chang, Alex Knauth, Ben Greenman. 694-705 [doi]
- Parallel functional arraysAnanya Kumar, Guy E. Blelloch, Robert Harper. 706-718 [doi]
- A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithmsIgor V. Konnov, Marijana Lazic, Helmut Veith, Josef Widder. 719-734 [doi]
- Analyzing divergence in bisimulation semanticsXinxin Liu, Tingting Yu, Wenhui Zhang. 735-747 [doi]
- Fencing off go: liveness and safety for channel-based programmingJulien Lange, Nicholas Ng, Bernardo Toninho, Nobuko Yoshida. 748-761 [doi]
- Big types in little runtime: open-world soundness and collaborative blame for gradual type systems Michael M. Vitousek, Cameron Swords, Jeremy G. Siek. 762-774 [doi]
- Gradual refinement typesNico Lehmann, Éric Tanter. 775-788 [doi]
- Automatically generating the dynamic semantics of gradually typed languagesMatteo Cimini, Jeremy G. Siek. 789-803 [doi]
- Sums of uncertainty: refinements go gradualKhurram A. Jafery, Joshua Dunfield. 804-817 [doi]
- Invariants of quantum programs: characterisations and generationMingsheng Ying, Shenggang Ying, Xiaodi Wu. 818-832 [doi]
- The geometry of parallelism: classical, probabilistic, and quantum effectsUgo Dal Lago, Claudia Faggian, Benoît Valiron, Akira Yoshimizu. 833-845 [doi]
- QWIRE: a core language for quantum circuitsJennifer Paykin, Robert Rand 0001, Steve Zdancewic. 846-858 [doi]
- LMS-Verify: abstraction without regret for verified systems programming Nada Amin, Tiark Rompf. 859-873 [doi]
- Hypercollecting semantics and its application to static analysis of information flowMounir Assaf, David A. Naumann, Julien Signoles, Eric Totel, Frédéric Tronel. 874-887 [doi]
- LightDP: towards automating differential privacy proofsDanfeng Zhang, Daniel Kifer. 888-901 [doi]