default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDProceedings of the ACM on Programming Languages, Volume 6
Volume 6, Number POPL, January 2022
- Toghrul Karimov
, Engel Lefaucheux, Joël Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, James Worrell:
What's decidable about linear loops? 1-25 - Roly Perera, Minh Nguyen, Tomas Petricek, Meng Wang:
Linked visualisations via Galois dependencies. 1-29 - Davide Sangiorgi:
From enhanced coinduction towards enhanced induction. 1-29 - Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer:
Simuliris: a separation logic framework for verifying concurrent program optimizations. 1-31 - Matthias Eichholz, Eric Hayden Campbell, Matthias Krebs, Nate Foster, Mira Mezini:
Dependently-typed data plane programming. 1-28 - Jialu Bao, Marco Gaboardi, Justin Hsu, Joseph Tassarotti:
A separation logic for negative dependence. 1-29 - Azalea Raad, Josh Berdine, Derek Dreyer, Peter W. O'Hearn:
Concurrent incorrectness separation logic. 1-29 - Devon Loehr, David Walker:
Safe, modular packet pipeline programming. 1-28 - Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, James R. Wilcox:
Property-directed reachability as abstract interpretation in the monotone theory. 1-31 - Ugo Dal Lago, Francesco Gavazzo:
Effectful program distancing. 1-30 - Faustyna Krawiec, Simon Peyton Jones, Neel Krishnaswami, Tom Ellis, Richard A. Eisenberg, Andrew W. Fitzgibbon:
Provably correct, asymptotically efficient, higher-order reverse-mode automatic differentiation. 1-30 - Vikraman Choudhury, Jacek Karwowski, Amr Sabry:
Symmetries in reversible programming: from symmetric rig groupoids to reversible programming languages. 1-32 - Jean-Marie Madiot, François Pottier:
A separation logic for heap space under garbage collection. 1-28 - Jules Jacobs, Stephanie Balzer, Robbert Krebbers:
Connectivity graphs: a method for proving deadlock freedom based on separation logic. 1-33 - Qianchuan Ye, Benjamin Delaware:
Oblivious algebraic data types. 1-29 - Loïc Pujet, Nicolas Tabareau:
Observational equality: now for good. 1-27 - Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, Peter Sewell:
VIP: verifying real-world C idioms with integer-pointer casts. 1-32 - Charles Yuan, Christopher McNally, Michael Carbin:
Twist: sound reasoning for purity and entanglement in Quantum programs. 1-32 - Xiaodong Jia, Andre Kornell, Bert Lindenhovius, Michael W. Mislove, Vladimir Zamdzhiev:
Semantics for variational Quantum programming. 1-31 - Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, Alex Aiken:
Induction duality: primal-dual search for invariants. 1-29 - Yue Niu, Jonathan Sterling, Harrison Grodin, Robert Harper:
A cost-aware logical framework. 1-31 - Alan Jeffrey, James Riely, Mark Batty, Simon Cooksey, Ilya Kaysin, Anton Podkopaev:
The leaky semicolon: compositional semantic dependencies for relaxed-memory concurrency. 1-30 - Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, Deian Stefan:
Isolation without taxation: near-zero-cost transitions for WebAssembly and SFI. 1-30 - Jay P. Lim, Santosh Nagarakatte:
One polynomial approximation to produce correctly rounded results of an elementary function for multiple representations and rounding modes. 1-28 - Luca Ciccone, Luca Padovani:
Fair termination of binary sessions. 1-30 - Arthur Oliveira Vale, Paul-André Melliès, Zhong Shao, Jérémie Koenig, Léo Stefanesco:
Layered and object-based game semantics. 1-32 - Delia Kesner:
A fine-grained computational interpretation of Girard's intuitionistic proof-nets. 1-28 - Marco Campion, Mila Dalla Preda, Roberto Giacobazzi:
Partial (In)Completeness in abstract interpretation: limiting the imprecision in program analysis. 1-31 - Dmitry Chistikov, Rupak Majumdar, Philipp Schepper:
Subcubic certificates for CFL reachability. 1-29 - Junyoung Jang, Samuel Gélineau, Stefan Monnier, Brigitte Pientka:
Mœbius: metaprogramming using contextual types: the stage where system f can pattern match on itself. 1-27 - Anders Miltner, Adrian Trejo Nuñez, Ana Brendel, Swarat Chaudhuri, Isil Dillig:
Bottom-up synthesis of recursive functional programs using angelic execution. 1-29 - Joakim Öhman, Aleksandar Nanevski:
Visibility reasoning for concurrent snapshot algorithms. 1-30 - Yizhou Zhang, Nada Amin:
Reasoning about "reasoning about reasoning": semantics and contextual equivalence for probabilistic programs with nested queries and recursion. 1-28 - Stefan K. Muller:
Static prediction of parallel computation graphs. 1-31 - Yuting Wang, Ling Zhang, Zhong Shao, Jérémie Koenig:
Verified compilation of C programs with a nominal memory model. 1-31 - Yuanbo Li, Kris Satya, Qirun Zhang:
Efficient algorithms for dynamic bidirected Dyck-reachability. 1-29 - Ningning Xie, Matthew Pickering, Andres Löh, Nicolas Wu, Jeremy Yallop, Meng Wang:
Staging with class: a specification for typed template Haskell. 1-30 - Xuan-Bach Le, Shang-Wei Lin, Jun Sun, David Sanán:
A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic. 1-27 - Mirai Ikebuchi, Andres Erbsen, Adam Chlipala:
Certifying derivation of state machines from coroutines. 1-31 - Yihong Zhang, Yisu Remy Wang, Max Willsey, Zachary Tatlock:
Relational e-matching. 1-22 - Cheng Zhang, Arthur Azevedo de Amorim, Marco Gaboardi:
On incorrectness logic and Kleene algebra with top and tests. 1-30 - Chris Heunen, Robin Kaarsgaard:
Quantum information effects. 1-27 - Giuseppe Castagna, Mickaël Laurent, Kim Nguyen, Matthew Lutze:
On type-cases, union elimination, and occurrence typing. 1-31 - Hari Govind V. K., Sharon Shoham, Arie Gurfinkel:
Solving constrained Horn clauses modulo algebraic data types and recursive functions. 1-29 - Amanda Liu, Gilbert Louis Bernstein, Adam Chlipala, Jonathan Ragan-Kelley:
Verified tensor-program optimization via high-level scheduling rewrites. 1-28 - Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, Viktor Vafeiadis:
Truly stateless, optimal dynamic partial order reduction. 1-28 - Adam Husted Kjelstrøm, Andreas Pavlogiannis:
The decidability and complexity of interleaved bidirected Dyck reachability. 1-26 - Zi Wang, Aws Albarghouthi, Gautam Prakriya, Somesh Jha:
Interval universal approximation for neural networks. 1-29 - Olivier Blanvillain, Jonathan Immanuel Brachthäuser, Maxime Kjaer, Martin Odersky:
Type-level programming with match types. 1-24 - Ugo Dal Lago, Francesco Gavazzo:
A relational theory of effects and coeffects. 1-28 - Andrew K. Hirsch, Deepak Garg:
Pirouette: higher-order typed functional choreographies. 1-27 - Azalea Raad, Luc Maranget, Viktor Vafeiadis:
Extending Intel-x86 consistency and persistency: formalising the semantics of Intel-x86 memory types and non-temporal stores. 1-31 - Jacob Laurel, Rem Yang, Gagandeep Singh, Sasa Misailovic:
A dual number abstraction for static analysis of Clarke Jacobians. 1-30 - Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche:
Context-bounded verification of thread pools. 1-28 - Ohad Kammar, Shin-ya Katsumata, Philip Saville:
Fully abstract models for effectful λ-calculi via category-theoretic logical relations. 1-28 - Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, Martin T. Vechev:
PRIMA: general and precise neural network certification via scalable convex hull approximations. 1-33 - Kuen-Bang Hou (Favonia), Zhuyang Wang:
Logarithm and program testing. 1-26 - Minseok Jeon, Hakjoo Oh:
Return of CFA: call-site sensitivity can be superior to object sensitivity even for object-oriented programs. 1-29 - Paul Krogmeier, P. Madhusudan:
Learning formulas in finite variable logics. 1-28 - Takeshi Tsukada, Hiroshi Unno:
Software model-checking as cyclic-proof search. 1-29 - Bryan Tan, Benjamin Mariano, Shuvendu K. Lahiri, Isil Dillig, Yu Feng:
SolType: refinement types for arithmetic overflow in solidity. 1-29 - Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, Zhilin Wu:
Solving string constraints with Regex-dependent functions through transducers with priorities and variables. 1-31 - Wenlei He, Julián Mestre, Sergey Pupyrev, Lei Wang, Hongtao Yu:
Profile inference revisited. 1-24 - Sorawee Porncharoenwase, Luke Nelson, Xi Wang, Emina Torlak:
A formal foundation for symbolic evaluation with merging. 1-28 - Marcelo Fiore, Dmitrij Szamozvancev:
Formal metatheory of second-order abstract syntax. 1-29
Volume 6, Number OOPSLA1, April 2022
- Kostas Ferles, Benjamin Sepanski, Rahul Krishnan, James Bornholt, Isil Dillig:
Synthesizing fine-grained synchronization protocols for implicit monitors. 1-26 - Koen Jacobs, Dominique Devriese, Amin Timany:
Purity of an ST monad: full abstraction by semantically typed back-translation. 1-27 - Basile Clément, Albert Cohen:
End-to-end translation validation for the halide language. 1-30 - Jonathan Immanuel Brachthäuser, Philipp Schuster, Edward Lee, Aleksander Boruch-Gruszecki:
Effects, capabilities, and boxes: from scope-based reasoning to type-based reasoning and back. 1-30 - Elizabeth Labrada, Matías Toro, Éric Tanter, Dominique Devriese:
Plausible sealing for gradual parametricity. 1-28 - Matteo Paltenghi, Michael Pradel:
Bugs in Quantum computing platforms: an empirical study. 1-27 - Aïna Linn Georges, Alix Trieu, Lars Birkedal:
Le temps des cerises: efficient temporal stack safety on capability machines using directed capabilities. 1-30 - Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, Chris Hawblitzel:
Linear types for large-scale systems verification. 1-28 - Peng Yan, Hanru Jiang, Nengkun Yu:
On incorrectness logic for Quantum programs. 1-28 - Jiawei Liu, Yuxiang Wei, Sen Yang, Yinlin Deng, Lingming Zhang:
Coverage-guided tensor compiler fuzzing with joint IR-pass mutation. 1-26 - Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, Steve Zdancewic:
C4: verified transactional objects. 1-31 - Benjamin Mariano, Yanju Chen, Yu Feng, Greg Durrett, Isil Dillig:
Automated transpilation of imperative to functional code using neural-guided program synthesis. 1-27 - Linpeng Zhang, Benjamin Lucien Kaminski:
Quantitative strongest post: a calculus for reasoning about the flow of quantitative information. 1-29 - Daniël A. A. Pelsmaeker, Hendrik van Antwerpen, Casper Bach Poulsen, Eelco Visser:
Language-parametric static semantic code completion. 1-30 - Bozhen Liu, Jeff Huang:
SHARP: fast incremental context-sensitive pointer analysis for Java. 1-28 - Aravind Machiry, John H. Kastner, Matt McCutchen, Aaron Eline, Kyle Headley, Michael Hicks:
C to checked C by 3c. 1-29 - Neville Grech, Sifis Lagouvardos, Ilias Tsatiris, Yannis Smaragdakis:
Elipmoc: advanced decompilation of Ethereum smart contracts. 1-27 - Shubham Ugare, Gagandeep Singh, Sasa Misailovic:
Proof transfer for fast certification of multiple approximate neural networks. 1-29 - Amir Shaikhha, Mathieu Huot, Jaclyn Smith, Dan Olteanu:
Functional collection programming with semi-ring dictionaries. 1-33 - Chengpeng Wang, Peisen Yao, Wensheng Tang, Qingkai Shi, Charles Zhang:
Complexity-guided container replacement synthesis. 1-31 - Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, Peter W. O'Hearn:
Finding real bugs in big programs with incorrectness logic. 1-27 - Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Tobias Winkler:
Weighted programming: a programming paradigm for specifying mathematical models. 1-30 - Véronique Benzaken, Evelyne Contejean, Mohammed Houssem Hachmaoui, Chantal Keller, Louis Mandel, Avraham Shinnar, Jérôme Siméon:
Translating canonical SQL to imperative code in Coq. 1-27 - Tristan Dyer, Tim Nelson, Kathi Fisler, Shriram Krishnamurthi:
Applying cognitive principles to model-finding output: the positive value of negative information. 1-29
Volume 6, Number ICFP, August 2022
- Norman Ramsey:
Beyond Relooper: recursive translation of unstructured control flow to structured control flow (functional pearl). 1-22 - James Koppel, Zheng Guo, Edsko de Vries, Armando Solar-Lezama, Nadia Polikarpova:
Searching entangled program spaces. 23-51 - Marek Materzok:
Generating circuits with generators. 52-79 - Patrick Bahr, Graham Hutton:
Monadic compiler calculation (functional pearl). 80-108 - Malgorzata Biernacka, Witold Charatonik, Tomasz Drab:
A simple and efficient implementation of strong call by need by an abstract machine. 109-136 - Arnaud Spiwack, Csongor Kiss, Jean-Philippe Bernardy, Nicolas Wu, Richard A. Eisenberg:
Linearly qualified types: generic inference for capabilities and uniqueness. 137-164 - Joseph Eremondi, Ronald Garcia, Éric Tanter:
Propositional equality for gradual dependently typed programming. 165-193 - Steven Keuchel, Sander Huyghebaert, Georgy Lukyanov, Dominique Devriese:
Verified symbolic execution with Kripke specification monads (and no meta-programming). 194-224 - Hsiang-Shang Ko, Liang-Ting Chen, Tzu-Chi Lin:
Datatype-generic programming meets elaborator reflection. 225-253 - Irene Yoon, Yannick Zakowski, Steve Zdancewic:
Formal reasoning about layered monadic interpreters. 254-282 - Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer:
Later credits: resourceful reasoning for the later modality. 283-311 - Yao Li, Stephanie Weirich:
Program adverbs and Tlön embeddings. 312-342 - Elijah Rivera, Shriram Krishnamurthi:
Structural versus pipeline composition of higher-order functions (experience report). 343-356 - Anton Lorenzen, Daan Leijen:
Reference counting with frame limited reuse. 357-380 - Minh Nguyen, Roly Perera, Meng Wang, Nicolas Wu:
Modular probabilistic models via algebraic effects. 381-410 - Cas van der Rest, Wouter Swierstra:
A completely unique account of enumeration. 411-437 - Klaus Ostermann, David Binder, Ingo Skupin, Tim Süberkrüb, Paul Downen:
Introduction and elimination, left and right. 438-465 - Jules Jacobs, Stephanie Balzer, Robbert Krebbers:
Multiparty GV: functional multiparty session types with certified deadlock freedom. 466-495 - Patrick Thomson, Rob Rix, Nicolas Wu, Tom Schrijvers:
Fusing industry and academia at GitHub (experience report). 496-511 - Sebastian Ullrich, Leonardo de Moura:
'do' unchained: embracing local imperativity in a purely functional language (functional pearl). 512-539 - András Kovács:
Staged compilation with two-level type theory. 540-569 - Frank Emrich, Jan Stolarek, James Cheney, Sam Lindley:
Constraint-based type inference for FreezeML. 570-595 - Elizaveta Vasilenko, Niki Vazou, Gilles Barthe:
Safe couplings: coupled refinement types. 596-624 - Lucas Escot, Jesper Cockx:
Practical generic programming over a universe of native datatypes. 625-649 - Benjamin Quiring, John H. Reppy, Olin Shivers:
Analyzing binding extent in 3CPS. 650-678 - Sam Westrick, Jatin Arora, Umut A. Acar:
Entanglement detection with near-zero cost. 679-710 - Son Ho, Jonathan Protzenko:
Aeneas: Rust verification by functional translation. 711-741 - James Koppel, Jackson Kearl, Armando Solar-Lezama:
Automatically deriving control-flow graph generators from operational semantics. 742-771 - Nachiappan Valliappan, Fabian Ruch, Carlos Tomé Cortiñas:
Normalization for fitch-style modal calculi. 772-798 - Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni:
Multi types and reasonable space. 799-825 - Gilles Barthe,