default search action
Proceedings of the ACM on Programming Languages, Volume 2
Volume 2, Number POPL, January 2018
- Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic:
Synthesizing bijective lenses. 1:1-1:30 - Jeevana Priya Inala, Rishabh Singh:
WebRelate: integrating web data with spreadsheets using examples. 2:1-2:28 - Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, Zhilin Wu:
What is decidable about string constraints with the ReplaceAll function. 3:1-3:29 - Lukás Holík, Petr Janku, Anthony W. Lin, Philipp Rümmer, Tomás Vojnar:
String constraints with concatenation and transducers solved efficiently. 4:1-4:32
- Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, Arnaud Spiwack:
Linear Haskell: practical linearity in a higher-order polymorphic language. 5:1-5:29 - Damiano Mazza, Luc Pellissier, Pierre Vial:
Polyadic approximations, fibrations and intersection types. 6:1-6:28 - Danel Ahman:
Handling fibred algebraic effects. 7:1-7:29 - Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, Filip Sieczkowski:
Handle with care: relational interpretation of algebraic effects and handlers. 8:1-8:30
- Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, Wei-Ngan Chin:
Automated lemma synthesis in symbolic-heap separation logic. 9:1-9:29 - Christof Löding, P. Madhusudan, Lucas Peña:
Foundations for natural proofs and quantifier instantiation. 10:1-10:30 - Toby Cathcart Burn, C.-H. Luke Ong, Steven J. Ramsay:
Higher-order constrained horn clauses for verification. 11:1-11:28 - Hiroshi Unno, Yuki Satake, Tachio Terauchi:
Relatively complete refinement type system for verification of higher-order non-deterministic programs. 12:1-12:29
- Lionel Parreaux, Antoine Voizard, Amir Shaikhha, Christoph E. Koch:
Unifying analytic and statically-typed quasiquotes. 13:1-13:33 - Matt Brown, Jens Palsberg:
Jones-optimal partial evaluation by specialization-safe normalization. 14:1-14:28 - John Peter Campora III, Sheng Chen, Martin Erwig, Eric Walkingshaw:
Migrating gradual types. 15:1-15:29 - Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, Eelco Visser:
Intrinsically-typed definitional interpreters for imperative languages. 16:1-16:34
- Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, Viktor Vafeiadis:
Effective stateless model checking for C/C++ concurrency. 17:1-17:32 - Brijesh Dongol, Radha Jagadeesan, James Riely:
Transactions in relaxed memory architectures. 18:1-18:29 - Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, Peter Sewell:
Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8. 19:1-19:29 - Hongjin Liang, Xinyu Feng:
Progress of concurrent objects with partial methods. 20:1-20:31
- Thomas Williams, Didier Rémy:
A principled approach to ornamentation in ML. 21:1-21:30 - William J. Bowman, Youyou Cong, Nick Rioux, Amal Ahmed:
Type-preserving CPS translation of Σ and Π types is not not possible. 22:1-22:33 - Andreas Abel, Joakim Öhman, Andrea Vezzosi:
Decidability of conversion for type theory in type theory. 23:1-23:29 - Ondrej Kuncar, Andrei Popescu:
Safety and conservativity of definitions in HOL and Isabelle/HOL. 24:1-24:26
- Michael Emmi, Constantin Enea:
Sound, complete, and tractable linearizability monitoring for concurrent collections. 25:1-25:27 - Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, Sharon Shoham:
Reducing liveness to safety in first-order logic. 26:1-26:33 - Gowtham Kaki, Kartik Nagar, Mahsa Najafzadeh, Suresh Jagannathan:
Alone together: compositional reasoning and inference for weak isolation. 27:1-27:34 - Ilya Sergey, James R. Wilcox, Zachary Tatlock:
Programming and proving with distributed protocols. 28:1-28:30
- Leandro T. C. Melo, Rodrigo Geraldo Ribeiro, Marcus R. de Araújo, Fernando Magno Quintão Pereira:
Inference of static semantics for incomplete C programs. 29:1-29:28 - Krishnendu Chatterjee, Bhavya Choudhary, Andreas Pavlogiannis:
Optimal Dyck reachability for data-dependence and alias analysis. 30:1-30:30 - Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, Kapil Vaidya:
Data-centric dynamic partial order reduction. 31:1-31:30 - Wenlei Bao, Sriram Krishnamoorthy, Louis-Noël Pouchet, P. Sadayappan:
Analytical modeling of cache behavior for affine programs. 32:1-32:26
- Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, Joost-Pieter Katoen:
A new proof rule for almost-sure termination. 33:1-33:28 - Sheshansh Agrawal, Krishnendu Chatterjee, Petr Novotný:
Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. 34:1-34:32 - Yangjia Li, Mingsheng Ying:
Algorithmic analysis of termination problems for quantum programs. 35:1-35:29 - Ivan Radicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Florian Zuleger:
Monadic refinements for relational cost analysis. 36:1-36:32
- Siddharth Krishna, Dennis E. Shasha, Thomas Wies:
Go with the flow: compositional abstractions for concurrent data structures. 37:1-37:31 - Dominique Devriese, Marco Patrignani, Frank Piessens:
Parametricity versus the universal type. 38:1-38:23 - Pierre Clairambault, Charles Grellois, Andrzej S. Murawski:
Linearity in higher-order recursion schemes. 39:1-39:29 - Stephen Chang, Alex Knauth, Emina Torlak:
Symbolic types for lenient symbolic execution. 40:1-40:29
- Hsiang-Shang Ko, Zhenjiang Hu:
An axiomatic basis for bidirectional programming. 41:1-41:29 - Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, Sandro Stucki:
Simplicitly: foundations and applications of implicit function types. 42:1-42:29
- Nils Anders Danielsson:
Up-to techniques using sized types. 43:1-43:28 - Paolo Capriotti, Nicolai Kraus:
Univalent higher categories via complete Semi-Segal types. 44:1-44:29
- Leonidas Lampropoulos, Zoe Paraskevopoulou, Benjamin C. Pierce:
Generating good generators for inductive relations. 45:1-45:30 - Rupak Majumdar, Filip Niksic:
Why is random testing effective for partition tolerance bugs? 46:1-46:24 - Wonyeol Lee, Rahul Sharma, Alex Aiken:
On automatically proving the correctness of math.h implementations. 47:1-47:32 - Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, Yoni Zohar:
Online detection of effectively callback free objects with applications to smart contracts. 48:1-48:28
- Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, Jan Vitek:
Correctness of speculative optimizations with dynamic deoptimization. 49:1-49:28 - José Fragoso Santos, Petar Maksimovic, Daiva Naudziuniene, Thomas Wood, Philippa Gardner:
JaVerT: JavaScript verification toolchain. 50:1-50:33 - Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, David Van Horn:
Soft contract verification for higher-order stateful programs. 51:1-51:30 - Nada Amin, Tiark Rompf:
Collapsing towers of interpreters. 52:1-52:33
- Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, Ranjit Jhala:
Refinement reflection: complete verification with SMT. 53:1-53:31 - Zachary Kincaid, John Cyphert, Jason Breck, Thomas W. Reps:
Non-linear reasoning for invariant synthesis. 54:1-54:33 - Gagandeep Singh, Markus Püschel, Martin T. Vechev:
A practical construction for decomposing numerical abstract domains. 55:1-55:28 - Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, William R. Cook:
Verifying equivalence of database-driven applications. 56:1-56:29
- Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving expected sensitivity of probabilistic programs. 57:1-57:29 - Aws Albarghouthi, Justin Hsu:
Synthesizing coupling proofs of differential privacy. 58:1-58:30 - Thomas Ehrhard, Michele Pagani, Christine Tasson:
Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming. 59:1-59:28 - Adam Scibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, Zoubin Ghahramani:
Denotational validation of higher-order Bayesian inference. 60:1-60:29
- Azadeh Farzan, Zachary Kincaid:
Strategy synthesis for linear arithmetic games. 61:1-61:30 - Kartik Chandra, Rastislav Bodík:
Bonsai: synthesis-based reasoning for type systems. 62:1-62:34 - Xinyu Wang, Isil Dillig, Rishabh Singh:
Program synthesis using abstraction refinement. 63:1-63:30
- Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, Lars Birkedal:
A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST. 64:1-64:28 - Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy:
Recalling a witness: foundations and applications of monotonic state. 65:1-65:30 - Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer:
RustBelt: securing the foundations of the rust programming language. 66:1-66:34
Volume 2, Number ICFP, September 2018
- Oliver Bracevac, Nada Amin, Guido Salvaneschi, Sebastian Erdweg, Patrick Eugster, Mira Mezini:
Versatile event correlation with algebraic effects. 67:1-67:31 - Jennifer Hackett, Graham Hutton:
Parametric polymorphism and operational improvement. 68:1-68:24 - Youyou Cong, Kenichi Asai:
Handling delimited continuations with dependent types. 69:1-69:31 - Conal Elliott:
The simple essence of automatic differentiation. 70:1-70:29 - Ben Greenman, Matthias Felleisen:
A spectrum of type soundness and performance. 71:1-71:32 - Sven Keidel, Casper Bach Poulsen, Sebastian Erdweg:
Compositional soundness proofs of abstract interpreters. 72:1-72:26 - Max S. New, Amal Ahmed:
Graduality from embedding-projection pairs. 73:1-73:30 - Rudi Horn, Roly Perera, James Cheney:
Incremental relational lenses. 74:1-74:30 - Jesper Cockx, Andreas Abel:
Elaborating dependent (co)pattern matching. 75:1-75:30 - James Koppel, Gabriel Scherer, Armando Solar-Lezama:
Capturing the future by replaying the past (functional pearl). 76:1-76:29 - Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer:
MoSeL: a general, extensible modal framework for interactive proofs in separation logic. 77:1-77:30 - Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas, Derek Dreyer:
Mtac2: typed tactics for backward reasoning in Coq. 78:1-78:31 - Andrey Mokhov, Neil Mitchell, Simon Peyton Jones:
Build systems à la carte. 79:1-79:29 - Solomon Maina, Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic:
Synthesizing quotient lenses. 80:1-80:29 - Atsushi Ohori, Katsuhiro Ueno, Hisayuki Mima:
Finitary polymorphism for optimizing type-directed compilation. 81:1-81:29 - José Bacelar Almeida, Alcino Cunha, Nuno Macedo, Hugo Pacheco, José Proença:
Teaching how to program using automated assessment and functional glossy games (experience report). 82:1-82:17 - Adam Scibior, Ohad Kammar, Zoubin Ghahramani:
Functional programming for modular Bayesian inference. 83:1-83:29 - Guillaume Boisseau, Jeremy Gibbons:
What you needa know about Yoneda: profunctor optics and the Yoneda lemma (functional pearl). 84:1-84:27 - Csongor Kiss, Matthew Pickering, Nicolas Wu:
Generic deriving of generic traversals. 85:1-85:30 - Jeremy Gibbons, Fritz Henglein, Ralf Hinze, Nicolas Wu:
Relational algebra by way of adjunctions. 86:1-86:28 - Mitchell Wand, Ryan Culpepper, Theophilos Giannakopoulos, Andrew Cobb:
Contextual equivalence for a probabilistic language with continuous random variables and recursion. 87:1-87:30 - Andrew K. Hirsch, Ross Tate:
Strict and lazy semantics for effects: layering monads and comonads. 88:1-88:30 - Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Stephanie Weirich:
Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report). 89:1-89:16 - Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna:
A type and scope safe universe of syntaxes with binding: their semantics and proofs. 90:1-90:30 - Ankush Das, Jan Hoffmann, Frank Pfenning:
Parallel complexity analysis with temporal session types. 91:1-91:30 - Nicolas Tabareau, Éric Tanter, Matthieu Sozeau:
Equivalences for free: univalent parametricity for effective transport. 92:1-92:29 - Antonis Stampoulis, Adam Chlipala:
Prototyping a functional language using higher-order logic programming: a functional pearl on learning the ways of λProlog/Makam. 93:1-93:30 - Beniamino Accattoli, Stéphane Graham-Lengrand, Delia Kesner:
Tight typings and split bounds. 94:1-94:30 - Stefan K. Muller, Umut A. Acar, Robert Harper:
Competitive parallelism: getting your priorities right. 95:1-95:30 - Ivan Perez:
Fault tolerant functional reactive programming (functional pearl). 96:1-96:30 - Martin Elsman, Troels Henriksen, Danil Annenkov, Cosmin E. Oancea:
Static interpretation of higher-order modules in Futhark: functional GPU programming in the large. 97:1-97:30 - John Peter Campora III, Sheng Chen, Eric Walkingshaw:
Casts and costs: harmonizing safety and performance in gradual typing. 98:1-98:30 - Chandrakana Nandi, James R. Wilcox, Pavel Panchekha, Taylor Blau, Dan Grossman, Zachary Tatlock:
Functional programming for compiling and decompiling computer-aided design. 99:1-99:31 - Jeremy Yallop, Tamara von Glehn, Ohad Kammar:
Partially-static data as free extension of algebras. 100:1-100:30 - Brent A. Yorgey, Kenneth Foner:
What's the difference? a functional pearl on subtracting bijections. 101:1-101:21 - Kenneth Foner, Hengchu Zhang, Leonidas Lampropoulos:
Keep your laziness in check. 102:1-102:30 - Frédéric Bour, Thomas Refis, Gabriel Scherer:
Merlin: a language server for OCaml (experience report). 103:1-103:15 - Larry Diehl, Denis Firsov, Aaron Stump:
Generic zero-cost reuse for dependent types. 104:1-104:30 - Guannan Wei, James M. Decker, Tiark Rompf:
Refunctionalization of abstract abstract machines: bridging the gap between abstract abstract machines and abstract definitional interpreters (functional pearl). 105:1-105:28 - Cyrus Omar, Jonathan Aldrich:
Reasonably programmable literal notation. 106:1-106:32
Volume 2, Number OOPSLA, November 2018
- Joscha Drechsler, Ragnar Mogk, Guido Salvaneschi, Mira Mezini:
Thread-safe reactive programming. 107:1-107:30 - Benoit Daloze, Arie Tal, Stefan Marr, Hanspeter Mössenböck, Erez Petrank:
Parallelization of dynamic languages: synchronizing built-in collections. 108:1-108:30 - Remigius Meier, Armin Rigo, Thomas R. Gross:
Virtual machine design for parallel dynamic programming languages. 109:1-109:25 - Charith Mendis, Saman P. Amarasinghe:
goSLP: globally optimized superword level parallelism framework. 110:1-110:28 - Jonathan Immanuel Brachthäuser, Philipp Schuster, Klaus Ostermann:
Effect handlers for the masses. 111:1-111:27 - Fabian Muehlboeck, Ross Tate:
Empowering union and intersection types with integrated subtyping. 112:1-112:29 - Francesco Zappa Nardelli, Julia Belyakova, Artem Pelenitsyn, Benjamin Chung, Jeff Bezanson, Jan Vitek:
Julia subtyping: a rational reconstruction. 113:1-113:27 - Hendrik van Antwerpen, Casper Bach Poulsen, Arjen Rouvoet, Eelco Visser:
Scopes as types. 114:1-114:30 - Peixuan Li, Danfeng Zhang:
A derivation framework for dependent security label inference. 115:1-115:26 - Neville Grech, Michael Kong, Anton Jurisevic, Lexi Brent, Bernhard Scholz, Yannis Smaragdakis:
MadMax: surviving out-of-gas conditions in Ethereum smart contracts. 116:1-116:27 - Chu-Pan Wong, Jens Meinicke, Lukas Lazarek, Christian Kästner:
Faster variational execution with transparent bytecode transformation. 117:1-117:30 - Kalev Alpernas, Cormac Flanagan, Sadjad Fouladi, Leonid Ryzhyk, Mooly Sagiv, Thomas Schmitz, Keith Winstein:
Secure serverless computing using dynamic information flow control. 118:1-118:26 - Roland Leißa, Klaas Boesche, Sebastian Hack, Arsène Pérard-Gayot, Richard Membarth, Philipp Slusallek, André Müller, Bertil Schmidt:
AnyDSL: a partial evaluation framework for programming high-performance libraries. 119:1-119:30 - Jeff Bezanson, Jiahao Chen, Benjamin Chung, Stefan Karpinski, Viral B. Shah, Jan Vitek, Lionel Zoubritzky:
Julia: dynamism and performance reconciled by design. 120:1-120:23 - Yunming Zhang, Mengjiao Yang, Riyadh Baghdadi, Shoaib Kamil, Julian Shun, Saman P. Amarasinghe:
GraphIt: a high-performance graph DSL. 121:1-121:30 - James Koppel, Varot Premtoon, Armando Solar-Lezama:
One tool, many languages: language-parametric transformation with incremental parametric syntax. 122:1-122:28 - Stephen Chou, Fredrik Kjolstad, Saman P. Amarasinghe:
Format abstraction for sparse tensor algebra compilers. 123:1-123:30