research-article

Open access

Effectful program distancing

Authors:

Francesco GavazzoAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 6, Issue POPL

Article No.: 19, Pages 1 - 30

https://doi.org/10.1145/3498680

Published: 12 January 2022 Publication History

Abstract

Semantics is traditionally concerned with program equivalence, in which all pairs of programs which are not equivalent are treated the same, and simply dubbed as incomparable. In recent years, various forms of program metrics have been introduced such that the distance between non-equivalent programs is measured as an element of an appropriate quantale. By letting the underlying quantale vary as the type of the compared programs become more complex, the recently introduced framework of differential logical relations allows for a new contextual form of reasoning. In this paper, we show that all this can be generalised to effectful higher-order programs, in which not only the values, but also the effects computations produce can be appropriately distanced in a principled way. We show that the resulting framework is flexible, allowing various forms of effects to be handled, and that it provides compact and informative judgments about program differences.

Supplementary Material

Auxiliary Presentation Video (popl22main-p94-p-video.mp4)

This is a short video presentation of the paper "Effectful Program Distancing" presented at POPL 2022.

Download
5.41 MB

References

[1]

Martín Abadi, Luca Cardelli, and Pierre-Louis Curien. 1993. Formal Parametric Polymorphism. Theor. Comput. Sci., 121, 1&2 (1993), 9–58. https://doi.org/10.1016/0304-3975(93)90082-5

Digital Library

[2]

Harold Abelson and Gerald J. Sussman. 1996. Structure and Interpretation of Computer Programs, Second Edition. MIT Press.

Digital Library

[3]

Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Pierre-Yves Strub. 2019. A relational logic for higher-order programs. J. Funct. Program., 29 (2019), e16. https://doi.org/10.1017/S0956796819000145

[4]

Mario Alvarez-Picallo and C.-H. Luke Ong. 2019. Change Actions: Models of Generalised Differentiation. In Proc. of FOSSACS 2019. 45–61. https://doi.org/10.1007/978-3-030-17127-8_3

Digital Library

[5]

Roland Carl Backhouse and Paul F. Hoogendijk. 1993. Elements of a Relational Theory of Datatypes. In Formal Program Development - IFIP TC2/WG 2.1 State-of-the-Art Report. 7–42.

[6]

Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. 2018. Coalgebraic Behavioral Metrics. Log. Methods Comput. Sci., 14, 3 (2018), https://doi.org/10.23638/LMCS-14(3:20)2018

[7]

M. Barr. 1970. Relational algebras. Lect. Notes Math., 137 (1970), 39–55.

[8]

Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2018. Proving expected sensitivity of probabilistic programs. Proc. ACM Program. Lang., 2, POPL (2018), 57:1–57:29. https://doi.org/10.1145/3158145

Digital Library

[9]

Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, and Pierre-Yves Strub. 2014. Proving Differential Privacy in Hoare Logic. In Proc. of CSF 2014. 411–424. https://doi.org/10.1109/CSF.2014.36

Digital Library

[10]

Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, and Pierre-Yves Strub. 2015. Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. In Proc. of POPL 2015. 55–68. https://doi.org/10.1145/2676726.2677000

Digital Library

[11]

Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2016. Proving Differential Privacy via Probabilistic Couplings. In Proc. of LICS 2016. 749–758. https://doi.org/10.1145/2933575.2934554

Digital Library

[12]

Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Béguelin. 2013. Probabilistic Relational Reasoning for Differential Privacy. ACM Trans. Program. Lang. Syst., 35, 3 (2013), 9:1–9:49. https://doi.org/10.1145/2492061

Digital Library

[13]

Nick Benton. 2004. Simple relational correctness proofs for static analyses and program transformations. In Proc. of POPL 2004. 14–25. https://doi.org/10.1145/964001.964003

Digital Library

[14]

Richard S. Bird and Oege de Moor. 1997. Algebra of programming. Prentice Hall.

[15]

Brett Boston, Adrian Sampson, Dan Grossman, and Luis Ceze. 2015. Probability type inference for flexible approximate programming. In Proc. of OOPSLA 2015. 470–487. https://doi.org/10.1145/2814270.2814301

Digital Library

[16]

Yufei Cai, Paolo G. Giarrusso, Tillmann Rendel, and Klaus Ostermann. 2014. A theory of changes for higher-order languages: incrementalizing λ -calculi by static differentiation. In Proc. of PLDI ’14. 145–155. https://doi.org/10.1145/2594291.2594304

Digital Library

[17]

Michael Carbin, Deokhwan Kim, Sasa Misailovic, and Martin C. Rinard. 2012. Proving acceptability properties of relaxed nondeterministic approximate programs. In Proc. of PLDI 2012. 169–180. https://doi.org/10.1145/2254064.2254086

Digital Library

[18]

Michael Carbin, Sasa Misailovic, and Martin C. Rinard. 2013. Verifying quantitative reliability for programs that execute on unreliable hardware. In Proc. of OOPSLA 2013. 33–52. https://doi.org/10.1145/2509136.2509546

Digital Library

[19]

Konstantinos Chatzikokolakis, Daniel Gebler, Catuscia Palamidessi, and Lili Xu. 2014. Generalized Bisimulation Metrics. In Proc. of CONCUR 2014. 32–46. https://doi.org/10.1007/978-3-662-44584-6_4

[20]

Swarat Chaudhuri, Sumit Gulwani, and Roberto Lublinerman. 2010. Continuity analysis of programs. In Proc. of POPL 2010. 57–70. https://doi.org/10.1145/1706299.1706308

Digital Library

[21]

Swarat Chaudhuri, Sumit Gulwani, Roberto Lublinerman, and Sara NavidPour. 2011. Proving programs robust. In Proc. of SIGSOFT/FSE’11. 102–112. https://doi.org/10.1145/2025113.2025131

Digital Library

[22]

Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Jan Hoffmann. 2017. Relational cost analysis. In Proc. of POPL 2017. 316–329. https://doi.org/10.1145/3009837.3009858

Digital Library

[23]

Maria Manuel Clementino, Dirk Hofmann, and Walter Tholen. 2004. One Setting for All: Metric, Topology, Uniformity, Approach Structure. Appl. Categorical Struct., 12, 2 (2004), 127–154. https://doi.org/10.1023/B:APCS.0000018144.87456.10

[24]

Raphaëlle Crubillé and Ugo Dal Lago. 2015. Metric Reasoning about λ -Terms: The Affine Case. In Proc. of LICS 2015. 633–644. https://doi.org/10.1109/LICS.2015.64

Digital Library

[25]

Raphaëlle Crubillé and Ugo Dal Lago. 2017. Metric Reasoning About λ -Terms: The General Case. In Proc. of ESOP 2017. 341–367. https://doi.org/10.1007/978-3-662-54434-1_13

Digital Library

[26]

Ugo Dal Lago and Francesco Gavazzo. 2019. Effectful Normal Form Bisimulation. In Proc. of ESOP 2019. 263–292. https://doi.org/10.1007/978-3-030-17184-1_10

[27]

Ugo Dal Lago and Francesco Gavazzo. 2019. On Bisimilarity in Lambda Calculi with Continuous Probabilistic Choice. In Proc. of MFPS 2019. 121–141. https://doi.org/10.1016/j.entcs.2019.09.007

Digital Library

[28]

Ugo Dal Lago and Francesco Gavazzo. 2020. Differential Logical Relations Part II: Increments and Derivatives. In Proc. of ICTCS 2020. 101–114.

[29]

Ugo Dal Lago and Francesco Gavazzo. 2021. Differential logical relations, part II increments and derivatives. Theoretical Computer Science, issn:0304-3975 https://doi.org/10.1016/j.tcs.2021.09.027

Digital Library

[30]

Ugo Dal Lago and Francesco Gavazzo. 2021. Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Programs. In Proc. of FSCD 2021 (LIPIcs, Vol. 195). 23:1–23:19. https://doi.org/10.4230/LIPIcs.FSCD.2021.23

[31]

Ugo Dal Lago and Francesco Gavazzo. 2022. A Relational Theory of Effects and Coeffects. Proc. ACM Program. Lang., 6, POPL (2022), 36:1–36:32. https://doi.org/10.1145/3498692

Digital Library

[32]

Ugo Dal Lago, Francesco Gavazzo, and Paul Blain Levy. 2017. Effectful applicative bisimilarity: Monads, relators, and Howe’s method. In Proc. of LICS 2017. 1–12. https://doi.org/10.1109/LICS.2017.8005117

[33]

Ugo Dal Lago, Francesco Gavazzo, and Ryo Tanaka. 2017. Effectful Applicative Similarity for Call-by-Name Lambda Calculi. In Proc. of ICTCS 2017. 87–98.

[34]

Ugo Dal Lago, Francesco Gavazzo, and Ryo Tanaka. 2020. Effectful applicative similarity for call-by-name lambda calculi. Theor. Comput. Sci., 813 (2020), 234–247. https://doi.org/10.1016/j.tcs.2019.12.025

Digital Library

[35]

Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu. 2019. Differential Logical Relations, Part I: The Simply-Typed Case. In Proc. of ICALP 2019. 111:1–111:14. https://doi.org/10.4230/LIPIcs.ICALP.2019.111

[36]

Ugo Dal Lago, Davide Sangiorgi, and Michele Alberti. 2014. On coinductive equivalences for higher-order probabilistic functional programs. In Proc. of POPL 2014. 297–308. https://doi.org/10.1145/2535838.2535872

Digital Library

[37]

Loris D’Antoni, Marco Gaboardi, Emilio Jesús Gallego Arias, Andreas Haeberlen, and Benjamin C. Pierce. 2013. Sensitivity analysis using type-based constraints. In Proc. of FPCDSL@ICFP 2013. 43–50. https://doi.org/10.1145/2505351.2505353

Digital Library

[38]

B.A. Davey and H.A. Priestley. 1990. Introduction to lattices and order. Cambridge University Press.

[39]

A.A. de Amorim, M. Gaboardi, J. Hsu, S. Katsumata, and I. Cherigui. 2017. A semantic account of metric preservation. In Proc. of POPL 2017. 545–556. https://doi.org/10.1145/3009837.3009890

Digital Library

[40]

Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, and Shin-ya Katsumata. 2019. Probabilistic Relational Reasoning via Metrics. In Proc. of LICS 2019. 1–19. https://doi.org/10.1109/LICS.2019.8785715

[41]

Y. Deng. 2015. Semantics of Probabilistic Processes: An Operational Approach. Springer Berlin Heidelberg.

[42]

Josee Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. 2004. Metrics for labelled Markov processes. Theor. Comput. Sci., 318, 3 (2004), 323–354. https://doi.org/10.1016/j.tcs.2003.09.013

Digital Library

[43]

W. Du, Y. Deng, and D. Gebler. 2016. Behavioural Pseudometrics for Nondeterministic Probabilistic Systems. In Proc. of SETTA 2016. 67–84. https://doi.org/10.1007/978-3-319-47677-3_5

[44]

Vladimir Estivill-Castro and Derick Wood. 1992. A Survey of Adaptive Sorting Algorithms. ACM Comput. Surv., 24, 4 (1992), 441–476. https://doi.org/10.1145/146370.146381

Digital Library

[45]

Bob Flagg and Ralph Kopperman. 1997. Continuity Spaces: Reconciling Domains and Metric Spaces. Theor. Comput. Sci., 177, 1 (1997), 111–138. https://doi.org/10.1016/S0304-3975(97)00236-3

Digital Library

[46]

Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce. 2013. Linear dependent types for differential privacy. In Proc. of POPL. 357–370. https://doi.org/10.1145/2429069.2429113

Digital Library

[47]

Francesco Gavazzo. 2018. Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances. In Proc. of LICS 2018. 452–461. https://doi.org/10.1145/3209108.3209149

Digital Library

[48]

Francesco Gavazzo. 2019. Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects. Ph. D. Dissertation. University of Bologna, Italy. http://amsdottorato.unibo.it/9075/

[49]

Daniel Gebler, Kim G. Larsen, and Simone Tini. 2016. Compositional bisimulation metric reasoning with Probabilistic Process Calculi. Log. Methods Comput. Sci., 12, 4 (2016), https://doi.org/10.2168/LMCS-12(4:12)2016

[50]

P.G. Giarrusso. 2018. Optimizing and incrementalizing higher-order collection queries by AST transformation. Ph. D. Dissertation. University of Tübingen.

[51]

Robert Harper. 2016. Practical Foundations for Programming Languages (2nd. Ed.). Cambridge University Press.

[52]

D. Hoffman. 2015. A cottage industry of lax extensions. Categories and General Algebraic Structures with Applications, 3, 1 (2015), 113–151.

[53]

D. Hofmann. 2007. Topological theories and closed objects. Adv. Math., 215 (2007), 789–824. https://doi.org/10.1016/j.aim.2007.04.013

[54]

2014. Monoidal Topology. A Categorical Approach to Order, Metric, and Topology, D. Hofmann, G.J. Seal, and W. Tholen (Eds.) (Encyclopedia of Mathematics and its Applications). Cambridge University Press.

[55]

Shin-ya Katsumata, Tetsuya Sato, and Tarmo Uustalu. 2018. Codensity Lifting of Monads and its Dual. Log. Methods Comput. Sci., 14, 4 (2018), https://doi.org/10.23638/LMCS-14(4:6)2018

[56]

A. Kurz and J. Velebil. 2016. Relation lifting, a survey. J. Log. Algebr. Meth. Program., 85, 4 (2016), 475–499. https://doi.org/10.1016/j.jlamp.2015.08.002

[57]

Kim Guldstrand Larsen and Arne Skou. 1989. Bisimulation Through Probabilistic Testing. In Proceedings of POPL 1989. 344–352. https://doi.org/10.1145/75277.75307

Digital Library

[58]

F.W. Lawvere. 1973. Metric spaces, generalized logic, and closed categories. Rend. Sem. Mat. Fis. Milano, 43 (1973), 135–166.

[59]

P.B. Levy, J. Power, and H. Thielecke. 2003. Modelling Environments in Call-by-Value Programming Languages. Inf. Comput., 185, 2 (2003), 182–210. https://doi.org/10.1016/S0890-5401(03)00088-9

Digital Library

[60]

S. MacLane. 1971. Categories for the Working Mathematician. Springer-Verlag.

[61]

Ernest G. Manes. 2002. Taut Monads and T0-spaces. Theor. Comput. Sci., 275, 1-2 (2002), 79–109. https://doi.org/10.1016/S0304-3975(00)00415-1

Digital Library

[62]

Sasa Misailovic, Daniel M. Roy, and Martin C. Rinard. 2011. Probabilistically Accurate Program Transformations. In Proc. of SAS. 316–333. https://doi.org/10.1007/978-3-642-23702-7_24

[63]

Sparsh Mittal. 2016. A Survey of Techniques for Approximate Computing. ACM Comput. Surv., 48, 4 (2016), Article 62, 33 pages. https://doi.org/10.1145/2893356

Digital Library

[64]

Eugenio Moggi. 1989. Computational Lambda-Calculus and Monads. In Proc. of LICS 1989. IEEE Computer Society, 14–23. https://doi.org/10.1109/LICS.1989.39155

[65]

Kobbi Nissim, Sofya Raskhodnikova, and Adam D. Smith. 2007. Smooth sensitivity and sampling in private data analysis. In Proc. of STOC 2007. 75–84. https://doi.org/10.1145/1250790.1250803

Digital Library

[66]

Paolo Pistone. 2021. On Generalized Metric Spaces for the Simply Typed Lambda-Calculus. In Proc. of LICS 2021. 1–14. https://doi.org/10.1109/LICS52264.2021.9470696

Digital Library

[67]

Gordon D. Plotkin. 1973. Lambda-Definability and Logical Relations. Memorandum SAI-RM-4, University of Edinburgh

[68]

Gordon D. Plotkin and John Power. 2001. Adequacy for Algebraic Effects. In Proc. of FOSSACS 2001. 1–24. https://doi.org/10.1007/3-540-45315-6_1

[69]

Weihao Qu, Marco Gaboardi, and Deepak Garg. 2019. Relational cost analysis for functional-imperative programs. Proc. ACM Program. Lang., 3, ICFP (2019), 92:1–92:29. https://doi.org/10.1145/3341696

Digital Library

[70]

Ivan Radicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Florian Zuleger. 2018. Monadic refinements for relational cost analysis. Proc. ACM Program. Lang., 2, POPL (2018), 36:1–36:32. https://doi.org/10.1145/3158124

Digital Library

[71]

Ganesan Ramalingam and Thomas W. Reps. 1993. A Categorized Bibliography on Incremental Computation. In Proc. of POPL 1993. 502–510. https://doi.org/10.1145/158511.158710

Digital Library

[72]

J. Reed and B.C. Pierce. 2010. Distance makes the types grow stronger: a calculus for differential privacy. In Proc. of ICFP 2010. 157–168. https://doi.org/10.1145/1863543.1863568

Digital Library

[73]

C.H. Richardson. 1954. An Introduction to the Calculus of Finite Differences. New York.

[74]

Martin C. Rinard. 2011. Probabilistic accuracy bounds for perforated programs: a new foundation for program analysis and transformation. In Proceedings of PEPM 2011. 79–80. https://doi.org/10.1145/1929501.1929517

Digital Library

[75]

Adrian Sampson, Werner Dietl, Emily Fortuna, Danushen Gnanapragasam, Luis Ceze, and Dan Grossman. 2011. EnerJ: approximate data types for safe and general low-power computation. In Proc. of PLDI 2011. 164–174. https://doi.org/10.1145/1993498.1993518

Digital Library

[76]

Adrian Sampson, Pavel Panchekha, Todd Mytkowicz, Kathryn S. McKinley, Dan Grossman, and Luis Ceze. 2014. Expressing and verifying probabilistic assertions. In Proc. of PLDI 2014. 112–122. https://doi.org/10.1145/2594291.2594294

Digital Library

[77]

D. Sands. 1998. Improvement Theory and Its Applications. In Higher Order Operational Techniques in Semantics, A. D. Gordon and A. M. Pitts (Eds.). Cambridge University Press, 275–306.

Digital Library

[78]

Tetsuya Sato, Gilles Barthe, Marco Gaboardi, Justin Hsu, and Shin-ya Katsumata. 2019. Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy. In Proc. of LICS 2019. 1–14. https://doi.org/10.1109/LICS.2019.8785668

[79]

R. Sedgewick and P. Flajolet. 2013. An Introduction to the Analysis of Algorithms. Pearson Education.

[80]

Stelios Sidiroglou-Douskos, Sasa Misailovic, Henry Hoffmann, and Martin C. Rinard. 2011. Managing performance vs. accuracy trade-offs with loop perforation. In Proc. of SIGSOFT/FSE’11. 124–134. https://doi.org/10.1145/2025113.2025133

Digital Library

[81]

V. Strassen. 1965. The existence of probability measures with given marginals. Ann. Math. Statist., 36, 2 (1965), 423–439.

[82]

A.M. Thijs. 1996. Simulation and fixpoint semantics. Rijksuniversiteit Groningen.

[83]

F. Van Breugel and J. Worrell. 2005. A behavioural pseudometric for probabilistic transition systems. Theor. Comput. Sci., 331, 1 (2005), 115–142. https://doi.org/10.1016/j.tcs.2004.09.035

Digital Library

[84]

C. Villani. 2008. Optimal Transport: Old and New. Springer Berlin Heidelberg.

[85]

Edwin M. Westbrook and Swarat Chaudhuri. 2013. A Semantics for Approximate Program Transformations. CoRR, abs/1304.5531 (2013), arxiv:1304.5531

[86]

Hang Zhang, Mateja Putic, and John Lach. 2014. Low Power GPGPU Computation with Imprecise Hardware. In The 51st Annual Design Automation Conference 2014, DAC ’14, San Francisco, CA, USA, June 1-5, 2014. 99:1–99:6. https://doi.org/10.1145/2593069.2593156

Digital Library

[87]

Hengchu Zhang, Edo Roth, Andreas Haeberlen, Benjamin C. Pierce, and Aaron Roth. 2019. Fuzzi: a three-level logic for differential privacy. Proc. ACM Program. Lang., 3, ICFP (2019), 93:1–93:28.

Digital Library

[88]

Zeyuan Allen Zhu, Sasa Misailovic, Jonathan A. Kelner, and Martin C. Rinard. 2012. Randomized accuracy-aware program transformations for efficient approximate computations. In Proc. of POPL 2012, John Field and Michael Hicks (Eds.). ACM, 441–454. https://doi.org/10.1007/978-3-642-35632-2_26

Cited By

Gregersen SAguirre AHaselwarter PTassarotti JBirkedal L(2024)Asynchronous Probabilistic Couplings in Higher-Order Separation LogicProceedings of the ACM on Programming Languages10.1145/36328688:POPL(753-784)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632868
Gavazzo FDi Florio C(2023)Elements of Quantitative RewritingProceedings of the ACM on Programming Languages10.1145/35712567:POPL(1832-1863)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571256
Dal Lago UGavazzo F(2022)A relational theory of effects and coeffectsProceedings of the ACM on Programming Languages10.1145/34986926:POPL(1-28)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498692

Index Terms

Effectful program distancing
1. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

Translating dependency into parametricity
ICFP '04: Proceedings of the ninth ACM SIGPLAN international conference on Functional programming

Abadi et al. introduced the dependency core calculus (DCC) as a unifying framework to study many important program analyses such as binding time, information flow, slicing, and function call tracking. DCC uses a lattice of monads and a nonstandard ...
Logical Relations for Monadic Types
CSL '02: Proceedings of the 16th International Workshop and 11th Annual Conference of the EACSL on Computer Science Logic

Logical relations andt heir generalizations are a fundamental tool in proving properties of lambda-calculi, e.g., yielding sound principles for observational equivalence. We propose a natural notion of logical relations able to deal with the monadic ...
Translating dependency into parametricity
ICFP '04

Abadi et al. introduced the dependency core calculus (DCC) as a unifying framework to study many important program analyses such as binding time, information flow, slicing, and function call tracking. DCC uses a lattice of monads and a nonstandard ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 6, Issue POPL

January 2022

1886 pages

EISSN:2475-1421

DOI:10.1145/3511309

Issue’s Table of Contents

Copyright © 2022 Owner/Author.

This work is licensed under a Creative Commons Attribution-ShareAlike International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 January 2022

Published in PACMPL Volume 6, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

European Research Council

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
713
Total Downloads

Downloads (Last 12 months)185
Downloads (Last 6 weeks)39

Reflects downloads up to 10 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Gregersen SAguirre AHaselwarter PTassarotti JBirkedal L(2024)Asynchronous Probabilistic Couplings in Higher-Order Separation LogicProceedings of the ACM on Programming Languages10.1145/36328688:POPL(753-784)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632868
Gavazzo FDi Florio C(2023)Elements of Quantitative RewritingProceedings of the ACM on Programming Languages10.1145/35712567:POPL(1832-1863)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571256
Dal Lago UGavazzo F(2022)A relational theory of effects and coeffectsProceedings of the ACM on Programming Languages10.1145/34986926:POPL(1-28)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498692

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents