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
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
What is decidable about string constraints with the ReplaceAll function. 3:1-3:29 - Lukás Holík, Petr Janku, Anthony W. Lin
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
Polyadic approximations, fibrations and intersection types. 6:1-6:28 - Danel Ahman
Handling fibred algebraic effects. 7:1-7:29 - Dariusz Biernacki
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
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
Migrating gradual types. 15:1-15:29 - Casper Bach Poulsen
Intrinsically-typed definitional interpreters for imperative languages. 16:1-16:34
- Michalis Kokologiannakis
Effective stateless model checking for C/C++ concurrency. 17:1-17:32 - Brijesh Dongol
Transactions in relaxed memory architectures. 18:1-18:29 - Christopher Pulte
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
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
Reducing liveness to safety in first-order logic. 26:1-26:33 - Gowtham Kaki
Alone together: compositional reasoning and inference for weak isolation. 27:1-27:34 - Ilya Sergey
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
Optimal Dyck reachability for data-dependence and alias analysis. 30:1-30:30 - Marek Chalupa
Data-centric dynamic partial order reduction. 31:1-31:30 - Wenlei Bao, Sriram Krishnamoorthy
Analytical modeling of cache behavior for affine programs. 32:1-32:26
- Annabelle McIver
A new proof rule for almost-sure termination. 33:1-33:28 - Sheshansh Agrawal, Krishnendu Chatterjee
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
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
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
Symbolic types for lenient symbolic execution. 40:1-40:29
- Hsiang-Shang Ko
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
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
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
Correctness of speculative optimizations with dynamic deoptimization. 49:1-49:28 - José Fragoso Santos
JaVerT: JavaScript verification toolchain. 50:1-50:33 - Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt
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
Refinement reflection: complete verification with SMT. 53:1-53:31 - Zachary Kincaid
Non-linear reasoning for invariant synthesis. 54:1-54:33 - Gagandeep Singh
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
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
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
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
Program synthesis using abstraction refinement. 63:1-63:30
- Amin Timany
A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST. 64:1-64:28 - Danel Ahman
Recalling a witness: foundations and applications of monotonic state. 65:1-65:30 - Ralf Jung
RustBelt: securing the foundations of the rust programming language. 66:1-66:34
Volume 2, Number ICFP, September 2018
- Oliver Bracevac
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
A spectrum of type soundness and performance. 71:1-71:32 - Sven Keidel
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
Capturing the future by replaying the past (functional pearl). 76:1-76:29 - Robbert Krebbers, Jacques-Henri Jourdan
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
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
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
Strict and lazy semantics for effects: layering monads and comonads. 88:1-88:30 - Joachim Breitner, Antal Spector-Zabusky, Yao Li
Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report). 89:1-89:16 - Guillaume Allais
A type and scope safe universe of syntaxes with binding: their semantics and proofs. 90:1-90:30 - Ankush Das
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
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
Generic zero-cost reuse for dependent types. 104:1-104:30 - Guannan Wei
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
Thread-safe reactive programming. 107:1-107:30 - Benoit Daloze, Arie Tal, Stefan Marr
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
Effect handlers for the masses. 111:1-111:27 - Fabian Muehlboeck
Empowering union and intersection types with integrated subtyping. 112:1-112:29 - Francesco Zappa Nardelli, Julia Belyakova, Artem Pelenitsyn
Julia subtyping: a rational reconstruction. 113:1-113:27 - Hendrik van Antwerpen
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
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
AnyDSL: a partial evaluation framework for programming high-performance libraries. 119:1-119:30 - Jeff Bezanson, Jiahao Chen, Benjamin Chung
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
Format abstraction for sparse tensor algebra compilers. 123:1-123:30 - Xiaoran Xu, Keith D. Cooper, Jacob Brock, Yan Zhang, Handong Ye:
ShareJIT: JIT code cache sharing across processes and its practical implementation. 124:1-124:23 - Juneyoung Lee, Chung-Kil Hur, Ralf Jung
Reconciling high-level optimizations and low-level code in LLVM. 125:1-125:28 - Zhangxiaowen Gong, Zhi Chen, Justin Josef Szaday, David C. Wong, Zehra Sura, Neftali Watkinson, Saeed Maleki, David A. Padua, Alexander V. Veidenbaum, Alexandru Nicolau, Josep Torrellas:
An empirical study of the effect of source-level loop transformations on compiler stability. 126:1-126:29 - Mikaël Mayer, Viktor Kuncak, Ravi Chugh:
Bidirectional evaluation with direct manipulation. 127:1-127:28 - Jason Ott, Tyson Loveless
BioScript: programming safe chemistry on laboratories-on-a-chip. 128:1-128:31 - Pascal Weisenburger
Distributed system development with ScalaLoci. 129:1-129:30 - Michael Faes
Concurrency-aware object-oriented programming with roles. 130:1-130:30 - P. Ezudheen
Horn-ICE learning for synthesizing invariants and contracts. 131:1-131:25 - Niki Vazou, Éric Tanter, David Van Horn
Gradual liquid type inference. 132:1-132:25 - Daniel Feltey, Ben Greenman
Collapsible contracts: fixing a pathology of gradual typing. 133:1-133:27 - Jack Williams
The root cause of blame: contracts for intersection and union types. 134:1-134:29 - Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, Tuan Phong Ngo:
Optimal stateless model checking under the release-acquire semantics. 135:1-135:29 - Peizhao Ou, Brian Demsky:
Towards understanding the costs of avoiding out-of-thin-air results. 136:1-136:29 - Azalea Raad, Viktor Vafeiadis
Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model. 137:1-137:27 - Jyothi Vedurada
Identifying refactoring opportunities for replacing type code with subclass and state. 138:1-138:28 - Tamás Szabó, Gábor Bergmann, Sebastian Erdweg, Markus Voelter:
Incrementalizing lattice-based program analyses in Datalog. 139:1-139:29 - Minseok Jeon
Precise and scalable points-to analysis via data-driven context tunneling. 140:1-140:29 - Yue Li, Tian Tan, Anders Møller, Yannis Smaragdakis:
Precision-guided context sensitivity for pointer analysis. 141:1-141:29 - Girish Maskeri Rama, Raghavan Komondoor, Himanshu Sharma:
Refinement in object-sensitivity points-to analysis via slicing. 142:1-142:27 - Nachshon Cohen:
Every data structure deserves lock-free memory reclamation. 143:1-143:24 - Sam Blackshear, Nikos Gorogiannis, Peter W. O'Hearn, Ilya Sergey
RacerD: compositional static race detection. 144:1-144:28 - Umang Mathur
What happens-after the first race? enhancing the predictive power of happens-before based dynamic race detection. 145:1-145:29 - Christian Gram Kalhauge
Sound deadlock prediction. 146:1-146:29 - Michael Pradel, Koushik Sen:
DeepBugs: a learning approach to name-based bug detection. 147:1-147:25 - Daniel W. Barowy, Emery D. Berger
ExceLint: automatically finding spreadsheet formula errors. 148:1-148:26 - James Bornholt, Emina Torlak:
Finding code that explodes under symbolic evaluation. 149:1-149:26 - Saswat Padhi, Prateek Jain, Daniel Perelman
FlashProfile: a framework for synthesizing data profiles. 150:1-150:28 - Ulan Degenbaev, Jochen Eisinger, Kentaro Hara, Marcel Hlopko, Michael Lippautz, Hannes Payer:
Cross-component garbage collection. 151:1-151:24 - Sebastian Burckhardt, Tim Coppieters:
Reactive caching for composed services: polling at the speed of push. 152:1-152:28 - Nachshon Cohen, David T. Aksun, James R. Larus:
Object-oriented recovery for non-volatile memory. 153:1-153:22 - Will Dietz, Vikram S. Adve:
Software multiplexing: share your libraries and statically link them too. 154:1-154:26 - Yuepeng Wang, Xinyu Wang
Relational program synthesis. 155:1-155:27 - Pavol Bielik, Marc Fischer, Martin T. Vechev:
Robust relational layout synthesis from examples for Android. 156:1-156:29 - Chenglong Wang, Alvin Cheung
Speeding up symbolic reasoning for relational queries. 157:1-157:25 - Junho Lee, Dowon Song, Sunbeom So
Automatic diagnosis and correction of logical errors for functional programming assignments. 158:1-158:30 - Ankush Desai, Amar Phanishayee, Shaz Qadeer, Sanjit A. Seshia:
Compositional programming and testing of dynamic distributed systems. 159:1-159:30 - Burcu Kulahcioglu Ozkan
Randomized testing of distributed systems with probabilistic guarantees. 160:1-160:28 - Marija Selakovic, Michael Pradel, Rezwana Karim, Frank Tip:
Test generation for higher-order functions in dynamic languages. 161:1-161:27 - Saba Alimadadi, Di Zhong, Magnus Madsen, Frank Tip:
Finding broken promises in asynchronous JavaScript programs. 162:1-162:26 - Brett Boston, Zoe Gong, Michael Carbin:
Leto: verifying application-specific hardware fault tolerance with programmable execution models. 163:1-163:30 - Gowtham Kaki
Safe replication through bounded concurrency verification. 164:1-164:27 - Marcelo Sousa, Isil Dillig, Shuvendu K. Lahiri:
Verified three-way program merge. 165:1-165:29 - Fengmin Zhu
Conflict resolution for structured merge via version space algebra. 166:1-166:25
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-11-19 20:34 CET 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: