Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDProceedings of the ACM on Programming Languages, Volume 8
Volume 8, Number POPL, January 2024
- Pascal Bergsträßer
, Moses Ganardi, Anthony W. Lin, Georg Zetzsche:
Ramsey Quantifiers in Linear Arithmetics. 1-32 - Jens Oliver Gutsfeld, Markus Müller-Olm, Christoph Ohrem:
Deciding Asynchronous Hyperproperties for Recursive Programs. 33-60 - Xueying Qin, Liam O'Connor, Rob van Glabbeek, Peter Höfner, Ohad Kammar, Michel Steuwer:
Shoggoth: A Formal Foundation for Strategic Rewriting. 61-89 - A. R. Balasubramanian, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche:
Reachability in Continuous Pushdown VASS. 90-114 - Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi:
Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers. 115-147 - William Mansky, Ke Du:
An Iris Instance for Verifying CompCert C Programs. 148-174 - Patrick Cousot:
Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation. 175-208 - Antoine Van Muylder, Andreas Nuyts, Dominique Devriese:
Internal and Observational Parametricity for Cubical Agda. 209-240 - Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Jonas Kastberg Hinrichsen, Léon Gondelman, Abel Nieto, Lars Birkedal:
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement. 241-272 - Harrison Grodin, Yue Niu, Jonathan Sterling, Robert Harper:
Decalf: A Directed, Effectful Cost-Aware Logical Framework. 273-301 - Alexandre Moine, Sam Westrick, Stephanie Balzer:
DisLog: A Separation Logic for Disentanglement. 302-331 - Dan Frumin, Amin Timany, Lars Birkedal:
Modular Denotational Semantics for Effects with Guarded Interaction Trees. 332-361 - Takeshi Tsukada, Kazuyuki Asada:
Enriched Presheaf Model of Quantum FPC. 362-392 - Guannan Wei, Oliver Bracevac, Songlin Jia, Yuyan Bao, Tiark Rompf:
Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs. 393-424 - Andrei Popescu:
Nominal Recursors as Epi-Recursors. 425-456 - Stephen Mell, Steve Zdancewic, Osbert Bastani:
Optimal Program Synthesis via Abstract Interpretation. 457-481 - Francis Rinaldi, june wunder, Arthur Azevedo de Amorim, Stefan K. Muller:
Pipelines and Beyond: Graph Types for ADTs with Futures. 482-511 - Noah Patton, Kia Rahmani, Meghana Missula, Joydeep Biswas, Isil Dillig:
Programming-by-Demonstration for Long-Horizon Robot Tasks. 512-545 - Jacques Carette, Chris Heunen, Robin Kaarsgaard, Amr Sabry:
With a Few Square Roots, Quantum Computing Is as Easy as Pi. 546-574 - Amin Timany, Armaël Guéneau, Lars Birkedal:
The Logical Essence of Well-Bracketed Control Flow. 575-603 - Angus Hammond, Zongyuan Liu, Thibaut Pérami, Peter Sewell, Lars Birkedal, Jean Pichon-Pharabod:
An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic. 604-637 - Chih-Duo Hong, Anthony W. Lin:
Regular Abstractions for Array Systems. 638-666 - Will Crichton, Shriram Krishnamurthi:
A Core Calculus for Documents: Or, Lambda: The Ultimate Document. 667-694 - Filip Sieczkowski, Sergei Stepanenko, Jonathan Sterling, Lars Birkedal:
The Essence of Generalized Algebraic Data Types. 695-723 - John Cyphert, Zachary Kincaid:
Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis. 724-752 - Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal:
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. 753-784 - Brandon Hewer, Graham Hutton:
Quotient Haskell: Lightweight Quotient Types for All. 785-815 - Shankara Pailoor, Yuepeng Wang, Isil Dillig:
Semantic Code Refactoring for Abstract Data Types. 816-847 - Pu Sun, Fu Song, Yuqi Chen, Taolue Chen:
EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis. 848-881 - Julian Müllner, Marcel Moosbrugger, Laura Kovács:
Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs. 882-910 - Azadeh Farzan, Umang Mathur:
Coarser Equivalences for Causal Concurrency. 911-941 - Ian Briggs, Yash Lad, Pavel Panchekha:
Implementation and Synthesis of Math Library Functions. 942-969 - Neta Elad, Oded Padon, Sharon Shoham:
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification. 970-1000 - Alex Buna-Marginean, Vincent Cheval, Mahsa Shirmohammadi, James Worrell:
On Learning Polynomial Recursive Programs. 1001-1027 - Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh:
Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions. 1028-1059 - Tom Smeding, Matthijs Vákár:
Efficient CHAD. 1060-1088 - Rupak Majumdar, V. R. Sathiyanarayana:
Positive Almost-Sure Termination: Complexity and Proof Rules. 1089-1117 - Sam Westrick, Matthew Fluet, Mike Rainey, Umut A. Acar:
Automatic Parallelism Management. 1118-1149 - Simon Guilloud, Viktor Kuncak:
Orthologic with Axioms. 1150-1178 - Giuseppe Castagna, Mickaël Laurent, Kim Nguyen:
Polymorphic Type Inference for Dynamic Languages. 1179-1210 - Xing Zhang, Ruifeng Xie, Guanchen Guo, Xiao He, Tao Zan, Zhenjiang Hu:
Fusing Direct Manipulations into Functional Programs. 1211-1238 - Shankaranarayanan Krishna, Aniket Lal, Andreas Pavlogiannis, Omkar Tuppe:
On-the-Fly Static Analysis via Dynamic Bidirected Dyck Reachability. 1239-1268 - Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, Gabriele Tedeschi:
Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-deterministic Observers. 1269-1297 - Yiyun Liu, Jonathan Chan, Jessica Shi, Stephanie Weirich:
Internalizing Indistinguishability with Dependent Types. 1298-1325 - Mikolaj Bojanczyk, Bartek Klin:
Polyregular Functions on Unordered Trees of Bounded Height. 1326-1351 - Liron Cohen, Adham Jabarin, Andrei Popescu, Reuben N. S. Rowe:
The Complex(ity) Landscape of Checking Infinite Descent. 1352-1384 - Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers:
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing. 1385-1417 - Lionel Parreaux, Aleksander Boruch-Gruszecki, Andong Fan, Chun Yin Chau:
When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism. 1418-1450 - Lyes Attouche, Mohamed Amine Baazizi, Dario Colazzo, Giorgio Ghelli, Carlo Sartiani, Stefanie Scherzinger:
Validation of Modern JSON Schema: Formalization and Complexity. 1451-1481 - François Pottier, Armaël Guéneau, Jacques-Henri Jourdan, Glen Mével:
Thunks and Debits in Separation Logic with Time Credits. 1482-1508 - Nicolas Chataing, Stephen Dolan, Gabriel Scherer, Jeremy Yallop:
Unboxed Data Constructors: Or, How cpp Decides a Halting Problem. 1509-1539 - Xiang Li, Xiangyu Zhou, Rui Dong, Yihong Zhang, Xinyu Wang:
Efficient Bottom-Up Synthesis for Programs with Local Variables. 1540-1568 - Jatin Arora, Stefan K. Muller, Umut A. Acar:
Disentanglement with Futures, State, and Interaction. 1569-1599 - Wenhao Tang, Daniel Hillerström, Sam Lindley, J. Garrett Morris:
Soundly Handling Linearity. 1600-1628 - Marco Campion, Mila Dalla Preda, Roberto Giacobazzi, Caterina Urban:
Monotonicity and the Precision of Program Analysis. 1629-1662 - Donnacha Oisín Kidney, Zhixuan Yang, Nicolas Wu:
Algebraic Effects Meet Hoare Logic in Cubical Agda. 1663-1695 - Philippe Heim, Rayna Dimitrova:
Solving Infinite-State Games via Acceleration. 1696-1726 - Thomas Koehler, Andrés Goens, Siddharth Bhat, Tobias Grosser, Phil Trinder, Michel Steuwer:
Guided Equality Saturation. 1727-1758 - Haowei Deng, Runzhou Tao, Yuxiang Peng, Xiaodi Wu:
A Case for Synthesis of Recursive Quantum Unitary Programs. 1759-1788 - Joshua M. Cohen, Philip Johnson-Freyd:
A Formalization of Core Why3 in Coq. 1789-1818 - Nathanael L. Ackerman, Cameron E. Freer, Younesse Kaddar, Jacek Karwowski, Sean K. Moss, Daniel M. Roy, Sam Staton, Hongseok Yang:
Probabilistic Programming Interfaces for Random Graphs: Markov Categories, Graphons, and Nominal Sets. 1819-1849 - Thodoris Sotiropoulos, Stefanos Chaliasos, Zhendong Su:
API-Driven Program Synthesis for Testing Static Typing Implementations. 1850-1881 - Francesca Randone, Luca Bortolussi, Emilio Incerto, Mirco Tribastone:
Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures. 1882-1912 - Itsaka Rakotonirina, Gilles Barthe, Clara Schneidewind:
Decision and Complexity of Dolev-Yao Hyperproperties. 1913-1944 - Matthew Hague, Artur Jez, Anthony W. Lin:
Parikh's Theorem Made Symbolic. 1945-1977 - Soham Chakraborty, Shankara Narayanan Krishna, Umang Mathur, Andreas Pavlogiannis:
How Hard Is Weak-Memory Testing? 1978-2009 - Steven Ramsay, Charlie Walpole:
Ill-Typed Programs Don't Evaluate. 2010-2040 - Eric Zhao, Raef Maroof, Anand Dukkipati, Andrew Blinn, Zhiyi Pan, Cyrus Omar:
Total Type Error Localization and Recovery with Holes. 2041-2068 - Litao Zhou, Jianxing Qin, Qinshi Wang, Andrew W. Appel, Qinxiang Cao:
VST-A: A Foundationally Sound Annotation Verifier. 2069-2098 - Michael Borkowski, Niki Vazou, Ranjit Jhala:
Mechanizing Refinement Types. 2099-2128 - Yuantian Ding, Xiaokang Qiu:
Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations. 2129-2159 - Ling Zhang, Yuting Wang, Jinhua Wu, Jérémie Koenig, Zhong Shao:
Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules. 2160-2190 - Zhendong Ang, Umang Mathur:
Predictive Monitoring against Pattern Regular Languages. 2191-2225 - Cezar-Constantin Andrici, Stefan Ciobaca, Catalin Hritcu, Guido Martínez, Exequiel Rivas, Éric Tanter, Théo Winterhalter:
Securing Verified IO Programs Against Unverified Code in F. 2226-2259 - Zhongkui Ma, Jiaying Li, Guangdong Bai:
ReLU Hull Approximation. 2260-2287 - Robert Atkey:
Polynomial Time and Dependent Types. 2288-2317 - Justin Frank, Benjamin Quiring, Leonidas Lampropoulos:
Generating Well-Typed Terms That Are Not "Useless". 2318-2339 - Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, Michael Shulman:
Internal Parametricity, without an Interval. 2340-2369 - Martin Elsman:
Explicit Effects and Effect Constraints in ReML. 2370-2394 - Adam T. Geller, Justin Frank, William J. Bowman:
Indexed Types for a Statically Safe WebAssembly. 2395-2424 - Yuxiang Peng, Jacob Young, Pengyu Liu, Xiaodi Wu:
SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog Compilation. 2425-2455 - Prasad Jayanti, Siddhartha Jayanti, Ugur Y. Yavuz, Lizzie Hernandez:
A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability. 2456-2484 - Azadeh Farzan, Dominik Klumpp, Andreas Podelski:
Commutativity Simplifies Proofs of Parameterized Programs. 2485-2513 - Claudia Faggian, Daniele Pautasso, Gabriele Vanoni:
Higher Order Bayesian Networks, Exactly. 2514-2546 - Conrad Zimmerman, Jenna DiVincenzo, Jonathan Aldrich:
Sound Gradual Verification with Symbolic Execution. 2547-2576 - Supun Abeysinghe, Anxhelo Xhebraj, Tiark Rompf:
Flan: An Expressive and Efficient Datalog Compiler for Program Analysis. 2577-2609 - Ugo Dal Lago, Alexis Ghyselen:
On Model-Checking Higher-Order Effectful Programs. 2610-2638 - Cameron Moy, Christos Dimoulas, Matthias Felleisen:
Effectful Software Contracts. 2639-2666 - John Peter Campora III, Mohammad Wahiduzzaman Khan, Sheng Chen:
Type-Based Gradual Typing Performance Optimization. 2667-2699 - Henry DeYoung, Andreia Mordido, Frank Pfenning, Ankush Das:
Parametric Subtyping for Structural Parametric Polymorphism. 2700-2730 - Yanis Sellami, Guillaume Girol, Frédéric Recoules, Damien Couroussé, Sébastien Bardin:
Inference of Robust Reachability Constraints. 2731-2760 - Konstantinos Mamouras, Agnishom Chattopadhyay:
Efficient Matching of Regular Expressions with Lookaround Assertions. 2761-2791 - Kevin Batz, Tom Jannik Biskup, Joost-Pieter Katoen, Tobias Winkler:
Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs. 2792-2820
a service of 
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-04-26 18:21 CEST 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:
