Next paper 15 September

data/desc.txt

@@ -1,3 +1,3 @@
-Mostly Automated Proof Repair for Verified Libraries
-Gopinathan, Kiran, et al. “Mostly Automated Proof Repair for Verified Libraries.” Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, June 2023, pp. 25–49. Crossref, https://doi.org/10.1145/3591221.
-The cost of maintaining formally specified and verified software is widely considered prohibitively high due to the need to constantly keep code and the proofs of its correctness in sync—the problem known as proof repair . One of the main challenges in automated proof repair for evolving code is to infer invariants for a new version of a once verified program that are strong enough to establish its full functional correctness. In this work, we present the first proof repair methodology for higher-order imperative functions, whose initial versions were verified in the Coq proof assistant and whose specifications remained unchanged. Our proof repair procedure is based on the combination of dynamic program alignment, enumerative invariant synthesis, and a novel technique for efficiently pruning the space of invariant candidates, dubbed proof-driven testing , enabled by the constructive nature of Coq’s proof certificates. We have implemented our approach in a mostly-automated proof repair tool called Sisyphus. Given an OCaml function verified in Coq and its unverified new version, Sisyphus produces a Coq proof for the new version, discharging most of the new proof goals automatically and suggesting high-confidence obligations for the programmer to prove for the cases when automation fails. We have evaluated Sisyphus on 10 OCaml programs taken from popular libraries, that manipulate arrays and mutable data structures, considering their verified original and unverified evolved versions. Sisyphus has managed to repair proofs for all those functions, suggesting correct invariants and generating a small number of easy-to-prove residual obligations.
+Collecting Cyclic Garbage across Foreign Function Interfaces: Who Takes the Last Piece of Cake?
+Yamazaki, Tetsuro, et al. “Collecting Cyclic Garbage across Foreign Function Interfaces: Who Takes the Last Piece of Cake?” Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, June 2023, pp. 591–614. Crossref, https://doi.org/10.1145/3591244.
+A growing number of libraries written in managed languages, such as Python and JavaScript, are bringing about new demand for a foreign language interface (FFI) between two managed languages. Such an FFI allows a host-language program to seamlessly call a library function written in a foreign language and exchange objects. It is often implemented by a user-level library but such implementation cannot reclaim cyclic garbage, or a group of objects with circular references, across the language boundary. This paper proposes Refgraph GC , which enables FFI implementation that can reclaim cyclic garbage. Refgraph GC coordinates the garbage collectors of two languages and it needs to modify the managed runtime of one language only. It does not modify that of the other language. This paper discusses the soundness and completeness of the proposed algorithm and also shows the results of the experiments with our implementation of FFI with Refgraph GC. This FFI allows a Ruby program to access a JavaScript library.

data/history.txt

@@ -10,4 +10,5 @@ https://doi.org/10.1145/3547652
 https://doi.org/10.1145/3314221.3314607
 https://doi.org/10.1145/3591264
 https://doi.org/10.1145/3563333
-https://doi.org/10.1145/3591221
+https://doi.org/10.1145/3591221
+https://doi.org/10.1145/3591244

data/next.txt

@@ -1 +1 @@
-https://doi.org/10.1145/3591221
+https://doi.org/10.1145/3591244

data/past.txt

@@ -2,4 +2,5 @@
 https://doi.org/10.1145/3314221.3314607
 https://doi.org/10.1145/3591264
 https://doi.org/10.1145/3563333
-https://doi.org/10.1145/3591221
+https://doi.org/10.1145/3591221
+https://doi.org/10.1145/3591244

docs/next.md

@@ -1 +1 @@
-Gopinathan, Kiran, et al. “Mostly Automated Proof Repair for Verified Libraries.” Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, June 2023, pp. 25–49. Crossref, <a href='https://doi.org/10.1145/3591221' target='_blank'>https://doi.org/10.1145/3591221</a>.
+Yamazaki, Tetsuro, et al. “Collecting Cyclic Garbage across Foreign Function Interfaces: Who Takes the Last Piece of Cake?” Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, June 2023, pp. 591–614. Crossref, <a href='https://doi.org/10.1145/3591244' target='_blank'>https://doi.org/10.1145/3591244</a>.

docs/papers.md

@@ -1,4 +1,5 @@
-1. Gopinathan, Kiran, et al. “Mostly Automated Proof Repair for Verified Libraries.” Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, June 2023, pp. 25–49. Crossref, <a href='https://doi.org/10.1145/3591221' target='_blank'>https://doi.org/10.1145/3591221</a>.
-2. Sundararajah, Kirshanthan, et al. “UniRec: A Unimodular-like Framework for Nested Recursions and Loops.” Proceedings of the ACM on Programming Languages, vol. 6, no. OOPSLA2, Oct. 2022, pp. 1264–90. Crossref, <a href='https://doi.org/10.1145/3563333' target='_blank'>https://doi.org/10.1145/3563333</a>.
-3. Zhang, Jialun, et al. “Interval Parsing Grammars for File Format Parsing.” Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, June 2023, pp. 1073–95. Crossref, <a href='https://doi.org/10.1145/3591264' target='_blank'>https://doi.org/10.1145/3591264</a>.
-4. Liao, Kevin, et al. “ILC: A Calculus for Composable, Computational Cryptography.” Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2019. Crossref, <a href='https://doi.org/10.1145/3314221.3314607' target='_blank'>https://doi.org/10.1145/3314221.3314607</a>.
+1. Yamazaki, Tetsuro, et al. “Collecting Cyclic Garbage across Foreign Function Interfaces: Who Takes the Last Piece of Cake?” Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, June 2023, pp. 591–614. Crossref, <a href='https://doi.org/10.1145/3591244' target='_blank'>https://doi.org/10.1145/3591244</a>.
+2. Gopinathan, Kiran, et al. “Mostly Automated Proof Repair for Verified Libraries.” Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, June 2023, pp. 25–49. Crossref, <a href='https://doi.org/10.1145/3591221' target='_blank'>https://doi.org/10.1145/3591221</a>.
+3. Sundararajah, Kirshanthan, et al. “UniRec: A Unimodular-like Framework for Nested Recursions and Loops.” Proceedings of the ACM on Programming Languages, vol. 6, no. OOPSLA2, Oct. 2022, pp. 1264–90. Crossref, <a href='https://doi.org/10.1145/3563333' target='_blank'>https://doi.org/10.1145/3563333</a>.
+4. Zhang, Jialun, et al. “Interval Parsing Grammars for File Format Parsing.” Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, June 2023, pp. 1073–95. Crossref, <a href='https://doi.org/10.1145/3591264' target='_blank'>https://doi.org/10.1145/3591264</a>.
+5. Liao, Kevin, et al. “ILC: A Calculus for Composable, Computational Cryptography.” Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2019. Crossref, <a href='https://doi.org/10.1145/3314221.3314607' target='_blank'>https://doi.org/10.1145/3314221.3314607</a>.