- Xueying Qin
, Liam O'Connor, Rob van Glabbeek, Peter Höfner, Ohad Kammar, Michel Steuwer:
Shoggoth: A Formal Foundation for Strategic Rewriting. Proc. ACM Program. Lang. 8(POPL): 61-89 (2024) - Itsaka Rakotonirina, Gilles Barthe, Clara Schneidewind:
Decision and Complexity of Dolev-Yao Hyperproperties. Proc. ACM Program. Lang. 8(POPL): 1913-1944 (2024) - Steven Ramsay, Charlie Walpole:
Ill-Typed Programs Don't Evaluate. Proc. ACM Program. Lang. 8(POPL): 2010-2040 (2024) - Francesca Randone, Luca Bortolussi, Emilio Incerto, Mirco Tribastone:
Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures. Proc. ACM Program. Lang. 8(POPL): 1882-1912 (2024) - Francis Rinaldi, june wunder, Arthur Azevedo de Amorim, Stefan K. Muller:
Pipelines and Beyond: Graph Types for ADTs with Futures. Proc. ACM Program. Lang. 8(POPL): 482-511 (2024) - Yanis Sellami, Guillaume Girol, Frédéric Recoules, Damien Couroussé, Sébastien Bardin:
Inference of Robust Reachability Constraints. Proc. ACM Program. Lang. 8(POPL): 2731-2760 (2024) - Filip Sieczkowski, Sergei Stepanenko, Jonathan Sterling, Lars Birkedal:
The Essence of Generalized Algebraic Data Types. Proc. ACM Program. Lang. 8(POPL): 695-723 (2024) - Tom Smeding, Matthijs Vákár:
Efficient CHAD. Proc. ACM Program. Lang. 8(POPL): 1060-1088 (2024) - Thodoris Sotiropoulos, Stefanos Chaliasos, Zhendong Su:
API-Driven Program Synthesis for Testing Static Typing Implementations. Proc. ACM Program. Lang. 8(POPL): 1850-1881 (2024) - Pu Sun, Fu Song, Yuqi Chen, Taolue Chen:
EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis. Proc. ACM Program. Lang. 8(POPL): 848-881 (2024) - Wenhao Tang, Daniel Hillerström, Sam Lindley, J. Garrett Morris:
Soundly Handling Linearity. Proc. ACM Program. Lang. 8(POPL): 1600-1628 (2024) - Amin Timany, Armaël Guéneau, Lars Birkedal:
The Logical Essence of Well-Bracketed Control Flow. Proc. ACM Program. Lang. 8(POPL): 575-603 (2024) - 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. Proc. ACM Program. Lang. 8(POPL): 241-272 (2024) - Takeshi Tsukada, Kazuyuki Asada:
Enriched Presheaf Model of Quantum FPC. Proc. ACM Program. Lang. 8(POPL): 362-392 (2024) - Guannan Wei, Oliver Bracevac, Songlin Jia, Yuyan Bao, Tiark Rompf:
Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs. Proc. ACM Program. Lang. 8(POPL): 393-424 (2024) - Sam Westrick, Matthew Fluet, Mike Rainey, Umut A. Acar:
Automatic Parallelism Management. Proc. ACM Program. Lang. 8(POPL): 1118-1149 (2024) - Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh:
Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions. Proc. ACM Program. Lang. 8(POPL): 1028-1059 (2024) - Ling Zhang, Yuting Wang, Jinhua Wu, Jérémie Koenig, Zhong Shao:
Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules. Proc. ACM Program. Lang. 8(POPL): 2160-2190 (2024) - Xing Zhang, Ruifeng Xie, Guanchen Guo, Xiao He, Tao Zan, Zhenjiang Hu:
Fusing Direct Manipulations into Functional Programs. Proc. ACM Program. Lang. 8(POPL): 1211-1238 (2024) - 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)
