Abstract is missing.
- Programming the world of uncertain things (keynote)Kathryn S. McKinley. 1-2 [doi]
- Synthesis of reactive controllers for hybrid systems (keynote)Richard M. Murray. 3 [doi]
- Confluences in programming languages research (keynote)David Walker. 4 [doi]
- Breaking through the normalization barrier: a self-interpreter for f-omegaMatt Brown, Jens Palsberg. 5-17 [doi]
- Type theory in type theory using quotient inductive typesThorsten Altenkirch, Ambrus Kaposi. 18-29 [doi]
- System f-omega with equirecursive types for datatype-generic programmingYufei Cai, Paolo G. Giarrusso, Klaus Ostermann. 30-43 [doi]
- A theory of effects and resources: adjunction models and polarised calculiPierre-Louis Curien, Marcelo P. Fiore, Guillaume Munch-Maccagnoni. 44-56 [doi]
- Temporal verification of higher-order functional programsAkihiro Murase, Tachio Terauchi, Naoki Kobayashi 0001, Ryosuke Sato, Hiroshi Unno. 57-68 [doi]
- Scaling network verification using symmetry and surgeryGordon D. Plotkin, Nikolaj Bjørner, Nuno P. Lopes, Andrey Rybalchenko, George Varghese. 69-83 [doi]
- Model checking for symbolic-heap separation logic with inductive predicatesJames Brotherston, Nikos Gorogiannis, Max I. Kanovich, Reuben Rowe. 84-96 [doi]
- Reducing crash recoverability to reachabilityEric Koskinen, Junfeng Yang. 97-108 [doi]
- Query-guided maximum satisfiabilityXin Zhang, Ravi Mangal, Aditya V. Nori, Mayur Naik. 109-122 [doi]
- String solving with word equations and transducers: towards a logic for analysing mutation XSSAnthony Widjaja Lin, Pablo Barceló. 123-136 [doi]
- Symbolic computation of differential equivalencesLuca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin. 137-150 [doi]
- Unboundedness and downward closures of higher-order pushdown automataMatthew Hague, Jonathan Kochems, C.-H. Luke Ong. 151-163 [doi]
- Fully-abstract compilation by approximate back-translationDominique Devriese, Marco Patrignani, Frank Piessens. 164-177 [doi]
- Lightweight verification of separate compilationJeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis. 178-190 [doi]
- From MinX to MinC: semantics-driven decompilation of recursive datatypesEdward Robbins, Andy King, Tom Schrijvers. 191-203 [doi]
- Sound type-dependent syntactic language extensionFlorian Lorenzen, Sebastian Erdweg. 204-216 [doi]
- Decidability of inferring inductive invariantsOded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, Mooly Sagiv. 217-231 [doi]
- The hardness of data packingRahman Lavaee. 232-242 [doi]
- The complexity of interactionStéphane Gimenez, Georg Moser. 243-255 [doi]
- Dependent types and multi-monadic effects in F*Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, Santiago Zanella Béguelin. 256-270 [doi]
- Fabular: regression formulas as probabilistic programmingJohannes Borgström, Andrew D. Gordon, Long Ouyang, Claudio V. Russo, Adam Scibior, Marcin Szymczak. 271-283 [doi]
- Kleenex: compiling nondeterministic transducers to deterministic streaming transducersNiels Bjørn Bugge Grathwohl, Fritz Henglein, Ulrik Terp Rasmussen, Kristoffer Aalund Søholm, Sebastian Paaske Tørholm. 284-297 [doi]
- Automatic patch generation by learning correct codeFan Long, Martin Rinard. 298-312 [doi]
- Estimating types in binaries using predictive modelingOmer Katz, Ran El-Yaniv, Eran Yahav. 313-326 [doi]
- Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programsKrishnendu Chatterjee, Hongfei Fu, Petr Novotný, Rouzbeh Hasheminezhad. 327-342 [doi]
- Transforming spreadsheet data types using examplesRishabh Singh, Sumit Gulwani. 343-356 [doi]
- Chapar: certified causally consistent distributed key-value storesMohsen Lesani, Christian J. Bell, Adam Chlipala. 357-370 [doi]
- 'Cause i'm strong enough: reasoning about consistency choices in distributed systemsAlexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, Marc Shapiro. 371-384 [doi]
- A program logic for concurrent objects under fair schedulingHongjin Liang, Xinyu Feng. 385-399 [doi]
- PSync: a partially synchronous language for fault-tolerant distributed algorithmsCezara Dragoi, Thomas A. Henzinger, Damien Zufferey. 400-415 [doi]
- Principal type inference for GADTsSheng Chen 0008, Martin Erwig. 416-428 [doi]
- Abstracting gradual typingRonald Garcia, Alison M. Clark, Éric Tanter. 429-442 [doi]
- The gradualizer: a methodology and algorithm for generating gradual type systemsMatteo Cimini, Jeremy G. Siek. 443-455 [doi]
- Is sound gradual typing dead?Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, Matthias Felleisen. 456-468 [doi]
- Combining static analysis with probabilistic models to enable market-scale Android inter-component analysisDamien Octeau, Somesh Jha, Matthew Dering, Patrick Drew McDaniel, Alexandre Bartel, Li Li 0029, Jacques Klein, Yves Le Traon. 469-484 [doi]
- Abstraction refinement guided by a learnt probabilistic modelRadu Grigore, Hongseok Yang. 485-498 [doi]
- Learning invariants using decision trees and implication counterexamplesPranav Garg 0001, Daniel Neider, P. Madhusudan, Dan Roth. 499-512 [doi]
- Symbolic abstract data type inferenceMichael Emmi, Constantin Enea. 513-525 [doi]
- SMO: an integrated approach to intra-array and inter-array storage optimizationSomashekaracharya G. Bhaskaracharya, Uday Bondhugula, Albert Cohen 0001. 526-538 [doi]
- PolyCheck: dynamic verification of iteration space transformations on affine programsWenlei Bao, Sriram Krishnamoorthy, Louis-Noël Pouchet, Fabrice Rastello, P. Sadayappan. 539-554 [doi]
- Printing floating-point numbers: a faster, always correct methodMarc Andrysco, Ranjit Jhala, Sorin Lerner. 555-567 [doi]
- Effects as sessions, sessions as effectsDominic A. Orchard, Nobuko Yoshida. 568-581 [doi]
- Monitors and blame assignment for higher-order session typesLimin Jia, Hannah Gommerstadt, Frank Pfenning. 582-594 [doi]
- Environmental bisimulations for probabilistic higher-order languagesDavide Sangiorgi, Valeria Vignudelli. 595-607 [doi]
- Modelling the ARMv8 architecture, operationally: concurrency and ISAShaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, Peter Sewell. 608-621 [doi]
- A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executionsJean Pichon-Pharabod, Peter Sewell. 622-633 [doi]
- Overhauling SC atomics in c11 and OpenCLMark Batty, Alastair F. Donaldson, John Wickerson. 634-648 [doi]
- Taming release-acquire consistencyOri Lahav, Nick Giannarakis, Viktor Vafeiadis. 649-662 [doi]
- Newtonian program analysis via tensor productThomas W. Reps, Emma Turetsky, Prathmesh Prabhu. 663-677 [doi]
- Casper: an efficient approach to call trace collectionRongxin Wu, Xiao Xiao, Shing-Chi Cheung, Hongyu Zhang, Charles Zhang. 678-690 [doi]
- Pushdown control-flow analysis for freeThomas Gilray, Steven Lyde, Michael D. Adams 0001, Matthew Might, David Van Horn. 691-704 [doi]
- Binding as sets of scopesMatthew Flatt. 705-717 [doi]
- Lattice-theoretic progress measures and coalgebraic model checkingIchiro Hasuo, Shunsuke Shimizu, Corina Cîrstea. 718-732 [doi]
- Algorithms for algebraic path properties in concurrent systems of constant treewidth componentsKrishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, Andreas Pavlogiannis. 733-747 [doi]
- Memoryful geometry of interaction II: recursion and adequacyKoko Muroya, Naohiko Hoshino, Ichiro Hasuo. 748-760 [doi]
- Learning programs from noisy dataVeselin Raychev, Pavol Bielik, Martin T. Vechev, Andreas Krause. 761-774 [doi]
- Optimizing synthesis with metasketchesJames Bornholt, Emina Torlak, Dan Grossman, Luis Ceze. 775-788 [doi]
- Maximal specification synthesisAws Albarghouthi, Isil Dillig, Arie Gurfinkel. 789-801 [doi]
- Example-directed synthesis: a type-theoretic interpretationJonathan Frankle, Peter-Michael Osera, David Walker, Steve Zdancewic. 802-815 [doi]