Next paper option 03 September

data/desc.txt

@@ -1,3 +1,3 @@
-A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized
-Abel, Andreas, et al. “A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized.” Proceedings of the ACM on Programming Languages, vol. 7, no. ICFP, Aug. 2023, pp. 920–54. Crossref, https://doi.org/10.1145/3607862.
-We present a graded modal type theory, a dependent type theory with grades that can be used to enforce various properties of the code. The theory has Π-types, weak and strong Σ-types, natural numbers, an empty type, and a universe, and we also extend the theory with a unit type and graded Σ-types. The theory is parameterized by a modality, a kind of partially ordered semiring, whose elements (grades) are used to track the usage of variables in terms and types. Different modalities are possible. We focus mainly on quantitative properties, in particular erasure: with the erasure modality one can mark function arguments as erasable. The theory is fully formalized in Agda. The formalization, which uses a syntactic Kripke logical relation at its core and is based on earlier work, establishes major meta-theoretic properties such as subject reduction, consistency, normalization, and decidability of definitional equality. We also prove a substitution theorem for grade assignment, and preservation of grades under reduction. Furthermore we study an extraction function that translates terms to an untyped λ-calculus and removes erasable content, in particular function arguments with the “erasable” grade. For a certain class of modalities we prove that extraction is sound, in the sense that programs of natural number type have the same value before and after extraction. Soundness of extraction holds also for open programs, as long as all variables in the context are erasable, the context is consistent, and erased matches are not allowed for weak Σ-types.
+A Gradual Probabilistic Lambda Calculus
+Ye, Wenjia, et al. “A Gradual Probabilistic Lambda Calculus.” Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA1, Apr. 2023, pp. 256–85. Crossref, https://doi.org/10.1145/3586036.
+Probabilistic programming languages have recently gained a lot of attention, in particular due to their applications in domains such as machine learning and differential privacy. To establish invariants of interest, many such languages include some form of static checking in the form of type systems. However, adopting such a type discipline can be cumbersome or overly conservative. Gradual typing addresses this problem by supporting a smooth transition between static and dynamic checking, and has been successfully applied for languages with different constructs and type abstractions. Nevertheless, its benefits have never been explored in the context of probabilistic languages. In this work, we present and formalize GPLC, a gradual source probabilistic lambda calculus. GPLC includes a binary probabilistic choice operator and allows programmers to gradually introduce/remove static type–and probability–annotations. The static semantics of GPLC heavily relies on the notion of probabilistic couplings, as required for defining several relations, such as consistency, precision, and consistent transitivity. The dynamic semantics of GPLC is given via elaboration to the target language TPLC, which features a distribution-based semantics interpreting programs as probability distributions over final values. Regarding the language metatheory, we establish that TPLC–and therefore also GPLC–is type safe and satisfies two of the so-called refined criteria for gradual languages, namely, that it is a conservative extension of a fully static variant and that it satisfies the gradual guarantee, behaving smoothly with respect to type precision.

data/history.txt

@@ -31,4 +31,5 @@ https://doi.org/10.1145/3622870
 https://doi.org/10.1145/3656456
 https://doi.org/10.1145/3622828
 https://doi.org/10.1145/3632882
-https://doi.org/10.1145/3607862
+https://doi.org/10.1145/3607862
+https://doi.org/10.1145/3586036

data/next.txt

@@ -1 +1 @@
-https://doi.org/10.1145/3607862
+https://doi.org/10.1145/3586036

data/past.txt

@@ -3,4 +3,5 @@
 https://doi.org/10.1145/3656456
 https://doi.org/10.1145/3622828
 https://doi.org/10.1145/3632882
-https://doi.org/10.1145/3607862
+https://doi.org/10.1145/3607862
+https://doi.org/10.1145/3586036

docs/index.md

@@ -27,7 +27,7 @@ Our tools for paper selection: [plgroup on Github](https://github.com/the-au-for
 | 2.  | September 6  | Simple Reference Immutability for System F <:             | 
 | 3.  | September 13 | Polymorphic Type Inference for Dynamic Languages                                                    |
 | 4.  | September 20 | A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized                                                    |
-| 5.  | September 27 | Paper 5 discussion                                                    |
+| 5.  | September 27 | A Gradual Probabilistic Lambda Calculus                                                    |
 | 6.  | October 4    | Paper 6 discussion                                                    |
 | 7.  | October 11   | Paper 7 discussion                                                    |
 | 8.  | October 18   | Paper 8 discussion                                                    |

docs/papers.md

@@ -1,4 +1,5 @@
 1. Kellison, Ariel E., and Justin Hsu. “Numerical Fuzz: A Type System for Rounding Error Analysis.” Proceedings of the ACM on Programming Languages, vol. 8, no. PLDI, June 2024, pp. 1954–78. Crossref, <a href='https://doi.org/10.1145/3656456' target='_blank'>https://doi.org/10.1145/3656456</a>.
 2. Lee, Edward, and Ondřej Lhoták. “Simple Reference Immutability for System F &lt;:” Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA2, Oct. 2023, pp. 857–81. Crossref, <a href='https://doi.org/10.1145/3622828' target='_blank'>https://doi.org/10.1145/3622828</a>.
 3. Castagna, Giuseppe, et al. “Polymorphic Type Inference for Dynamic Languages.” Proceedings of the ACM on Programming Languages, vol. 8, no. POPL, Jan. 2024, pp. 1179–210. Crossref, <a href='https://doi.org/10.1145/3632882' target='_blank'>https://doi.org/10.1145/3632882</a>.
-4. Abel, Andreas, et al. “A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized.” Proceedings of the ACM on Programming Languages, vol. 7, no. ICFP, Aug. 2023, pp. 920–54. Crossref, <a href='https://doi.org/10.1145/3607862' target='_blank'>https://doi.org/10.1145/3607862</a>.
+4. Abel, Andreas, et al. “A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized.” Proceedings of the ACM on Programming Languages, vol. 7, no. ICFP, Aug. 2023, pp. 920–54. Crossref, <a href='https://doi.org/10.1145/3607862' target='_blank'>https://doi.org/10.1145/3607862</a>.
+5. Ye, Wenjia, et al. “A Gradual Probabilistic Lambda Calculus.” Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA1, Apr. 2023, pp. 256–85. Crossref, <a href='https://doi.org/10.1145/3586036' target='_blank'>https://doi.org/10.1145/3586036</a>.