- Eric Zhao
, Raef Maroof, Anand Dukkipati, Andrew Blinn, Zhiyi Pan, Cyrus Omar:
Total Type Error Localization and Recovery with Holes. Proc. ACM Program. Lang. 8(POPL): 2041-2068 (2024) - Litao Zhou, Jianxing Qin, Qinshi Wang, Andrew W. Appel, Qinxiang Cao:
VST-A: A Foundationally Sound Annotation Verifier. Proc. ACM Program. Lang. 8(POPL): 2069-2098 (2024) - Conrad Zimmerman, Jenna DiVincenzo, Jonathan Aldrich:
Sound Gradual Verification with Symbolic Execution. Proc. ACM Program. Lang. 8(POPL): 2547-2576 (2024) - 2023
- Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins, J. Garrett Morris, Aaron Stump:
A Type-Based Approach to Divide-and-Conquer Recursion in Coq. Proc. ACM Program. Lang. 7(POPL): 61-90 (2023) - Alejandro Aguirre, Lars Birkedal:
Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice. Proc. ACM Program. Lang. 7(POPL): 33-60 (2023) - Rajeev Alur, Caleb Stanford, Christopher Watson:
A Robust Theory of Series Parallel Graphs. Proc. ACM Program. Lang. 7(POPL): 1058-1088 (2023) - Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David A. Naumann, Minh Ngo:
An Algebra of Alignment for Relational Verification. Proc. ACM Program. Lang. 7(POPL): 573-603 (2023) - Victor Arrial, Giulio Guerrieri, Delia Kesner:
Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework. Proc. ACM Program. Lang. 7(POPL): 1483-1513 (2023) - Aurèle Barrière, Sandrine Blazy, David Pichardie:
Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler. Proc. ACM Program. Lang. 7(POPL): 249-277 (2023) - Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Lena Verscht:
A Calculus for Amortized Expected Runtimes. Proc. ACM Program. Lang. 7(POPL): 1957-1986 (2023) - Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche:
Context-Bounded Verification of Context-Free Specifications. Proc. ACM Program. Lang. 7(POPL): 2141-2170 (2023) - Aaron Bembenek, Michael Greenberg, Stephen Chong:
From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems. Proc. ACM Program. Lang. 7(POPL): 185-217 (2023) - Filippo Bonchi, Alessandro Di Giorgio, Alessio Santamaria:
Deconstructing the Calculus of Relations with Tape Diagrams. Proc. ACM Program. Lang. 7(POPL): 1864-1894 (2023) - Matthew Bowers, Theo X. Olausson, Lionel Wong, Gabriel Grand, Joshua B. Tenenbaum, Kevin Ellis, Armando Solar-Lezama:
Top-Down Synthesis for Library Learning. Proc. ACM Program. Lang. 7(POPL): 1182-1213 (2023) - José Cambronero, Sumit Gulwani, Vu Le, Daniel Perelman, Arjun Radhakrishna, Clint Simon, Ashish Tiwari:
FlashFill++: Scaling Programming by Example by Cutting to the Chase. Proc. ACM Program. Lang. 7(POPL): 952-981 (2023) - David Cao, Rose Kunkel, Chandrakana Nandi, Max Willsey, Zachary Tatlock, Nadia Polikarpova:
babble: Learning Better Abstractions with E-Graphs and Anti-unification. Proc. ACM Program. Lang. 7(POPL): 396-424 (2023) - Simon Castellan, Pierre Clairambault:
The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Unfolding. Proc. ACM Program. Lang. 7(POPL): 689-717 (2023) - Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, Steve Zdancewic:
Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq. Proc. ACM Program. Lang. 7(POPL): 1770-1800 (2023) - Zilin Chen, Ambroise Lafont, Liam O'Connor, Gabriele Keller, Craig McLaughlin, Vincent Jackson, Christine Rizkallah:
Dargent: A Silver Bullet for Verified Data Layout Refinement. Proc. ACM Program. Lang. 7(POPL): 1369-1395 (2023) - Emanuele D'Osualdo, Azalea Raad, Viktor Vafeiadis:
The Path to Durable Linearizability. Proc. ACM Program. Lang. 7(POPL): 748-774 (2023) - Ria Das, Joshua B. Tenenbaum, Armando Solar-Lezama, Zenna Tavares:
Combining Functional and Automata Synthesis to Discover Causal Reactive Programs. Proc. ACM Program. Lang. 7(POPL): 1628-1658 (2023) - Ankush Das, Di Wang, Jan Hoffmann:
Probabilistic Resource-Aware Session Types. Proc. ACM Program. Lang. 7(POPL): 1925-1956 (2023) - Swaraj Dash, Younesse Kaddar, Hugo Paquet, Sam Staton:
Affine Monads and Lazy Structures for Bayesian Programming. Proc. ACM Program. Lang. 7(POPL): 1338-1368 (2023) - Joel D. Day, Vijay Ganesh, Nathan Grewal, Florin Manea:
On the Expressive Power of String Constraints. Proc. ACM Program. Lang. 7(POPL): 278-308 (2023) - Shuo Ding, Qirun Zhang:
Witnessability of Undecidable Problems. Proc. ACM Program. Lang. 7(POPL): 982-1002 (2023) - Azadeh Farzan, Dominik Klumpp, Andreas Podelski:
Stratified Commutativity in Verification Algorithms for Concurrent Programs. Proc. ACM Program. Lang. 7(POPL): 1426-1453 (2023) - Kuen-Bang Hou (Favonia), Carlo Angiuli, Reed Mullanix:
An Order-Theoretic Analysis of Universe Polymorphism. Proc. ACM Program. Lang. 7(POPL): 1659-1685 (2023) - Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger:
Proto-Quipper with Dynamic Lifting. Proc. ACM Program. Lang. 7(POPL): 309-334 (2023) - Joshua Gancher, Kristina Sojakova, Xiong Fan, Elaine Shi, Greg Morrisett:
A Core Calculus for Equational Proofs of Cryptographic Protocols. Proc. ACM Program. Lang. 7(POPL): 866-892 (2023) - Francesco Gavazzo, Cecilia Di Florio:
Elements of Quantitative Rewriting. Proc. ACM Program. Lang. 7(POPL): 1832-1863 (2023)
