Table of Contents

• Modular reasoning about concurrent higher-order imperative programsLars Birkedal. 1-2 [doi]
• A galois connection calculus for abstract interpretationPatrick Cousot, Radhia Cousot. 3-4 [doi]
• Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluationGiuseppe Castagna, Kim Nguyen 0001, Zhiwu Xu, Hyeonseung Im, Sergueï Lenglet, Luca Padovani. 5-18 [doi]
• Backpack: retrofitting Haskell with interfacesScott Kilpatrick, Derek Dreyer, Simon L. Peyton Jones, Simon Marlow. 19-32 [doi]
• Combining proofs and programs in a dependently typed languageChris Casinghino, Vilhelm Sjöberg, Stephanie Weirich. 33-46 [doi]
• Tracing compilation by abstract interpretationStefano Dissegna, Francesco Logozzo, Francesco Ranzato. 47-60 [doi]
• A type-directed abstraction refinement approach to higher-order model checkingSteven James Ramsay, Robin P. Neatherway, C.-H. Luke Ong. 61-72 [doi]
• Fissile type analysis: modular checking of almost everywhere invariantsDevin Coughlin, Bor-Yuh Evan Chang. 73-86 [doi]
• A trusted mechanised JavaSript specificationMartin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt, Gareth Smith. 87-100 [doi]
• An operational and axiomatic semantics for non-determinism and sequence points in CRobbert Krebbers. 101-112 [doi]
• NetkAT: semantic foundations for networksCarolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, David Walker. 113-126 [doi]
• Bias-variance tradeoffs in program analysisRahul Sharma 0001, Aditya V. Nori, Alex Aiken. 127-138 [doi]
• Abstract satisfactionVijay D'Silva, Leopold Haller, Daniel Kroening. 139-150 [doi]
• Proofs that countAzadeh Farzan, Zachary Kincaid, Andreas Podelski. 151-164 [doi]
• A verified information-flow architectureArthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew P. Tolmach. 165-178 [doi]
• CakeML: a verified implementation of MLRamana Kumar, Magnus O. Myreen, Michael Norrish, Scott Owens. 179-192 [doi]
• Probabilistic relational verification for cryptographic implementationsGilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella Béguelin. 193-206 [doi]
• Bridging boolean and quantitative synthesis using smoothed proof searchSwarat Chaudhuri, Martin Clochard, Armando Solar-Lezama. 207-220 [doi]
• A constraint-based approach to solving games on infinite graphsTewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, Andrey Rybalchenko. 221-234 [doi]
• Sound compilation of realsEva Darulova, Viktor Kuncak. 235-248 [doi]
• 30 years of research and development around CoqGérard Huet, Hugo Herbelin. 249-250 [doi]
• The essence of ReynoldsStephen Brookes, Peter W. O'Hearn, Uday S. Reddy. 251-256 [doi]
• Freeze after writing: quasi-deterministic parallel programming with LVarsLindsey Kuper, Aaron Turon, Neelakantan R. Krishnaswami, Ryan R. Newton. 257-270 [doi]
• Replicated data types: specification, verification, optimalitySebastian Burckhardt, Alexey Gotsman, Hongseok Yang, Marek Zawirski. 271-284 [doi]
• Verifying eventual consistency of optimistic replication systemsAhmed Bouajjani, Constantin Enea, Jad Hamza. 285-296 [doi]
• On coinductive equivalences for higher-order probabilistic functional programsUgo Dal Lago, Davide Sangiorgi, Michele Alberti. 297-308 [doi]
• Probabilistic coherence spaces are fully abstract for probabilistic PCFThomas Ehrhard, Christine Tasson, Michele Pagani. 309-320 [doi]
• Tabular: a schema-driven probabilistic programming languageAndrew D. Gordon, Thore Graepel, Nicolas Rolland, Claudio V. Russo, Johannes Borgström, John Guiver. 321-334 [doi]
• Modular, higher-order cardinality analysis in theory and practiceIlya Sergey, Dimitrios Vytiniotis, Simon L. Peyton Jones. 335-348 [doi]
• Profiling for lazinessStephen Chang, Matthias Felleisen. 349-360 [doi]
• Fair reactive programmingAndrew Cave, Francisco Ferreira, Prakash Panangaden, Brigitte Pientka. 361-372 [doi]
• Optimal dynamic partial order reductionParosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, Konstantinos F. Sagonas. 373-384 [doi]
• Modular reasoning about heap paths via effectively propositional formulasShachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv. 385-396 [doi]
• A sound and complete abstraction for reasoning about parallel prefix sumsNathan Chong, Alastair F. Donaldson, Jeroen Ketema. 397-410 [doi]
• Authenticated data structures, genericallyAndrew Miller, Michael Hicks, Jonathan Katz, Elaine Shi. 411-424 [doi]
• Gradual typing embedded securely in JavaScriptNikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin M. Bierman. 425-438 [doi]
• Sound input filter generation for integer overflow errorsFan Long, Stelios Sidiroglou-Douskos, Deokhwan Kim, Martin C. Rinard. 439-452 [doi]
• Parametric completeness for separation theoriesJames Brotherston, Jules Villard. 453-464 [doi]
• Proof search for propositional abstract separation logics via labelled sequentsZhe Hou, Ranald Clouston, Rajeev Goré, Alwen Tiu. 465-476 [doi]
• A proof system for separation logic with magic wandWonyeol Lee, Sungwoo Park. 477-490 [doi]
• From parametricity to conservation laws, via Noether's theoremRobert Atkey. 491-502 [doi]
• A relationally parametric model of dependent type theoryRobert Atkey, Neil Ghani, Patricia Johann. 503-516 [doi]
• Game semantics for interface middleweight JavaAndrzej S. Murawski, Nikos Tzevelekos. 517-528 [doi]
• Abstract acceleration of general linear loopsBertrand Jeannet, Peter Schrammel, Sriram Sankaranarayanan. 529-540 [doi]
• Minimization of symbolic automataLoris D'Antoni, Margus Veanes. 541-554 [doi]
• Consistency analysis of decision-making programsSwarat Chaudhuri, Azadeh Farzan, Zachary Kincaid. 555-568 [doi]
• Toward general diagnosis of static errorsDanfeng Zhang, Andrew C. Myers. 569-582 [doi]
• Counter-factual typing for debugging type errorsSheng Chen 0008, Martin Erwig. 583-594 [doi]
• Battery transition systemsUdi Boker, Thomas A. Henzinger, Arjun Radhakrishna. 595-606 [doi]
• Symbolic optimization with SMT solversYi Li, Aws Albarghouthi, Zachary Kincaid, Arie Gurfinkel, Marsha Chechik. 607-618 [doi]
• Abstract effects and proof-relevant logical relationsNick Benton, Martin Hofmann 0001, Vivek Nigam. 619-632 [doi]
• Parametric effect monads and semantics of effect systemsShin-ya Katsumata. 633-646 [doi]
• Applying quantitative semantics to higher-order quantum computingMichele Pagani, Peter Selinger, Benoît Valiron. 647-658 [doi]
• A nonstandard standardization theoremBeniamino Accattoli, Eduardo Bonelli, Delia Kesner, Carlos Lombardi. 659-670 [doi]
• Closed type families with overlapping equationsRichard A. Eisenberg, Dimitrios Vytiniotis, Simon L. Peyton Jones, Stephanie Weirich. 671-684 [doi]