• Marshall D and Orchard D. (2024). Non-Linear Communication via Graded Modal Session Types. Information and Computation. 10.1016/j.ic.2024.105234. (105234). Online publication date: 1-Nov-2024.

    https://linkinghub.elsevier.com/retrieve/pii/S0890540124000993

  • Torczon C, Suárez Acevedo E, Agrawal S, Velez-Ginorio J and Weirich S. (2024). Effects and Coeffects in Call-by-Push-Value. Proceedings of the ACM on Programming Languages. 8:OOPSLA2. (1108-1134). Online publication date: 8-Oct-2024.

    https://doi.org/10.1145/3689750

  • Giannini P and Duso G. Coeffects for MiniJava: Cf-Mj. Proceedings of the 26th ACM International Workshop on Formal Techniques for Java-like Programs. (30-36).

    https://doi.org/10.1145/3678721.3686232

  • Lorenzen A, White L, Dolan S, Eisenberg R and Lindley S. (2024). Oxidizing OCaml with Modal Memory Management. Proceedings of the ACM on Programming Languages. 8:ICFP. (485-514). Online publication date: 15-Aug-2024.

    https://doi.org/10.1145/3674642

  • Marshall D and Orchard D. (2024). Functional Ownership through Fractional Uniqueness. Proceedings of the ACM on Programming Languages. 8:OOPSLA1. (1040-1070). Online publication date: 29-Apr-2024.

    https://doi.org/10.1145/3649848

  • Lee E, Zhao Y, Lhoták O, You J, Satheeskumar K and Brachthäuser J. (2024). Qualifying System F<:: Some Terms and Conditions May Apply. Proceedings of the ACM on Programming Languages. 8:OOPSLA1. (583-612). Online publication date: 29-Apr-2024.

    https://doi.org/10.1145/3649832

  • Boruch-Gruszecki A, Odersky M, Lee E, Lhoták O and Brachthäuser J. (2023). Capturing Types. ACM Transactions on Programming Languages and Systems. 45:4. (1-52). Online publication date: 31-Dec-2024.

    https://doi.org/10.1145/3618003

  • Bianchini R, Dagnino F, Giannini P and Zucca E. (2023). Resource-Aware Soundness for Big-Step Semantics. Proceedings of the ACM on Programming Languages. 7:OOPSLA2. (1281-1309). Online publication date: 16-Oct-2023.

    https://doi.org/10.1145/3622843

  • Abel A, Danielsson N and Eriksson O. (2023). A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized. Proceedings of the ACM on Programming Languages. 7:ICFP. (920-954). Online publication date: 30-Aug-2023.

    https://doi.org/10.1145/3607862

  • Bianchini R. Monitoring for Resource-Awareness. Proceedings of the 6th International Workshop on Verification and Monitoring at Runtime Execution. (13-16).

    https://doi.org/10.1145/3605159.3605856

  • Toro M, Darais D, Abuah C, Near J, Árquez D, Olmedo F and Tanter É. (2023). Contextual Linear Types for Differential Privacy. ACM Transactions on Programming Languages and Systems. 45:2. (1-69). Online publication date: 30-Jun-2023.

    https://doi.org/10.1145/3589207

  • Grove J and Bernardy J. (2022). Algebraic Effects for Extensible Dynamic Semantics. Journal of Logic, Language and Information. 10.1007/s10849-022-09378-7. 32:2. (219-245). Online publication date: 1-May-2023.

    https://link.springer.com/10.1007/s10849-022-09378-7

  • Gavazzo F and Di Florio C. (2023). Elements of Quantitative Rewriting. Proceedings of the ACM on Programming Languages. 7:POPL. (1832-1863). Online publication date: 9-Jan-2023.

    https://doi.org/10.1145/3571256

  • Ahman D. (2023). When Programs Have to Watch Paint Dry. Foundations of Software Science and Computation Structures. 10.1007/978-3-031-30829-1_1. (1-23).

    https://link.springer.com/10.1007/978-3-031-30829-1_1

  • Zhu F, Sammler M, Lepigre R, Dreyer D and Garg D. (2022). BFF: foundational and automated verification of bitfield-manipulating programs. Proceedings of the ACM on Programming Languages. 6:OOPSLA2. (1613-1638). Online publication date: 31-Oct-2022.

    https://doi.org/10.1145/3563345

  • Susag Z, Lahiri S, Hsu J and Roy S. (2022). Symbolic execution for randomized programs. Proceedings of the ACM on Programming Languages. 6:OOPSLA2. (1583-1612). Online publication date: 31-Oct-2022.

    https://doi.org/10.1145/3563344

  • Lei Y, Sui Y, Ding S and Zhang Q. (2022). Taming transitive redundancy for context-free language reachability. Proceedings of the ACM on Programming Languages. 6:OOPSLA2. (1556-1582). Online publication date: 31-Oct-2022.

    https://doi.org/10.1145/3563343

  • Boruch-Gruszecki A, Waśko R, Xu Y and Parreaux L. (2022). A case for DOT: theoretical foundations for objects with pattern matching and GADT-style reasoning. Proceedings of the ACM on Programming Languages. 6:OOPSLA2. (1526-1555). Online publication date: 31-Oct-2022.

    https://doi.org/10.1145/3563342

  • Moosbrugger M, Stankovič M, Bartocci E and Kovács L. (2022). This is the moment for probabilistic loops. Proceedings of the ACM on Programming Languages. 6:OOPSLA2. (1497-1525). Online publication date: 31-Oct-2022.

    https://doi.org/10.1145/3563341

  • Kolesar J, Piskac R and Hallahan W. (2022). Checking equivalence in a non-strict language. Proceedings of the ACM on Programming Languages. 6:OOPSLA2. (1469-1496). Online publication date: 31-Oct-2022.

    https://doi.org/10.1145/3563340

  • Choudhury P. (2022). Monadic and comonadic aspects of dependency analysis. Proceedings of the ACM on Programming Languages. 6:OOPSLA2. (1320-1348). Online publication date: 31-Oct-2022.

    https://doi.org/10.1145/3563335

  • Bianchini R, Dagnino F, Giannini P, Zucca E and Servetto M. (2022). Coeffects for sharing and mutation. Proceedings of the ACM on Programming Languages. 6:OOPSLA2. (870-898). Online publication date: 31-Oct-2022.

    https://doi.org/10.1145/3563319

  • Frumin D, D’Osualdo E, van den Heuvel B and Pérez J. (2022). A bunch of sessions: a propositions-as-sessions interpretation of bunched implications in channel-based concurrency. Proceedings of the ACM on Programming Languages. 6:OOPSLA2. (841-869). Online publication date: 31-Oct-2022.

    https://doi.org/10.1145/3563318

  • Sivaraman A, Sanchez-Stern A, Chen B, Lerner S and Millstein T. (2022). Data-driven lemma synthesis for interactive proofs. Proceedings of the ACM on Programming Languages. 6:OOPSLA2. (505-531). Online publication date: 31-Oct-2022.

    https://doi.org/10.1145/3563306

  • Hoeflich J, Findler R and Serrano M. (2022). Highly illogical, Kirk: spotting type mismatches in the large despite broken contracts, unsound types, and too many linters. Proceedings of the ACM on Programming Languages. 6:OOPSLA2. (479-504). Online publication date: 31-Oct-2022.

    https://doi.org/10.1145/3563305

  • Bierhoff K. (2022). Wildcards need witness protection. Proceedings of the ACM on Programming Languages. 6:OOPSLA2. (373-394). Online publication date: 31-Oct-2022.

    https://doi.org/10.1145/3563301

  • Sela G and Petrank E. (2022). Concurrent size. Proceedings of the ACM on Programming Languages. 6:OOPSLA2. (345-372). Online publication date: 31-Oct-2022.

    https://doi.org/10.1145/3563300

  • Dagnino F and Pasquali F. Logical Foundations of Quantitative Equality. Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science. (1-13).

    https://doi.org/10.1145/3531130.3533337

  • Brachthäuser J, Schuster P, Lee E and Boruch-Gruszecki A. (2022). Effects, capabilities, and boxes: from scope-based reasoning to type-based reasoning and back. Proceedings of the ACM on Programming Languages. 6:OOPSLA1. (1-30). Online publication date: 29-Apr-2022.

    https://doi.org/10.1145/3527320

  • Batz K, Gallus A, Kaminski B, Katoen J and Winkler T. (2022). Weighted programming: a programming paradigm for specifying mathematical models. Proceedings of the ACM on Programming Languages. 6:OOPSLA1. (1-30). Online publication date: 29-Apr-2022.

    https://doi.org/10.1145/3527310

  • Marshall D and Orchard D. (2022). Replicate, Reuse, Repeat: Capturing Non-Linear Communication via Session Types and Graded Modal Types. Electronic Proceedings in Theoretical Computer Science. 10.4204/EPTCS.356.1. 356. (1-11).

    http://arxiv.org/abs/2203.12875v1

  • Dal Lago U and Gavazzo F. (2022). A relational theory of effects and coeffects. Proceedings of the ACM on Programming Languages. 6:POPL. (1-28). Online publication date: 16-Jan-2022.

    https://doi.org/10.1145/3498692

  • Choudhury P, Eades H and Weirich S. (2022). A Dependent Dependency Calculus. Programming Languages and Systems. 10.1007/978-3-030-99336-8_15. (403-430).

    https://link.springer.com/10.1007/978-3-030-99336-8_15

  • Wood J and Atkey R. (2021). A Linear Algebra Approach to Linear Metatheory. Electronic Proceedings in Theoretical Computer Science. 10.4204/EPTCS.353.10. 353. (195-212).

    http://arxiv.org/abs/2005.02247v3

  • Punchihewa H and Wu N. Safe mutation with algebraic effects. Proceedings of the 14th ACM SIGPLAN International Symposium on Haskell. (122-135).

    https://doi.org/10.1145/3471874.3472988

  • Rajani V, Gaboardi M, Garg D and Hoffmann J. (2021). A unifying type-theory for higher-order (amortized) cost analysis. Proceedings of the ACM on Programming Languages. 5:POPL. (1-28). Online publication date: 4-Jan-2021.

    https://doi.org/10.1145/3434308

  • ALLAIS G, ATKEY R, CHAPMAN J, MCBRIDE C and MCKINNA J. (2021). A type- and scope-safe universe of syntaxes with binding: their semantics and proofs. Journal of Functional Programming. 10.1017/S0956796820000076. 31.

    https://www.cambridge.org/core/product/identifier/S0956796820000076/type/journal_article

  • Gaboardi M, Katsumata S, Orchard D and Sato T. (2021). Graded Hoare Logic and its Categorical Semantics. Programming Languages and Systems. 10.1007/978-3-030-72019-3_9. (234-263).

    http://link.springer.com/10.1007/978-3-030-72019-3_9

  • Moon B, Eades III H and Orchard D. (2021). Graded Modal Dependent Type Theory. Programming Languages and Systems. 10.1007/978-3-030-72019-3_17. (462-490).

    http://link.springer.com/10.1007/978-3-030-72019-3_17

  • Brachthäuser J, Schuster P and Ostermann K. (2020). Effects as capabilities: effect handlers and lightweight effect polymorphism. Proceedings of the ACM on Programming Languages. 4:OOPSLA. (1-30). Online publication date: 13-Nov-2020.

    https://doi.org/10.1145/3428194

  • Choudhury V and Krishnaswami N. (2020). Recovering purity with comonads and capabilities. Proceedings of the ACM on Programming Languages. 4:ICFP. (1-28). Online publication date: 2-Aug-2020.

    https://doi.org/10.1145/3408993

  • Abel A and Bernardy J. (2020). A unified view of modalities in type systems. Proceedings of the ACM on Programming Languages. 4:ICFP. (1-28). Online publication date: 2-Aug-2020.

    https://doi.org/10.1145/3408972

  • Johnsen E, Steffen M and Stumpf J. (2020). Assumption-Commitment Types for Resource Management in Virtually Timed Ambients. Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles. 10.1007/978-3-030-61362-4_6. (103-121).

    http://link.springer.com/10.1007/978-3-030-61362-4_6

  • Orchard D, Liepelt V and Eades III H. (2019). Quantitative program reasoning with graded modal types. Proceedings of the ACM on Programming Languages. 3:ICFP. (1-30). Online publication date: 26-Jul-2019.

    https://doi.org/10.1145/3341714

  • Kavvos G. (2019). Modalities, cohesion, and information flow. Proceedings of the ACM on Programming Languages. 3:POPL. (1-29). Online publication date: 2-Jan-2019.

    https://doi.org/10.1145/3290333

  • Hirsch A and Tate R. (2018). Strict and lazy semantics for effects: layering monads and comonads. Proceedings of the ACM on Programming Languages. 2:ICFP. (1-30). Online publication date: 30-Jul-2018.

    https://doi.org/10.1145/3236783

  • Bračevac O, Amin N, Salvaneschi G, Erdweg S, Eugster P and Mezini M. (2018). Versatile event correlation with algebraic effects. Proceedings of the ACM on Programming Languages. 2:ICFP. (1-31). Online publication date: 30-Jul-2018.

    https://doi.org/10.1145/3236762

  • Tanabe Y, Aotani T and Masuhara H. A Context-Oriented Programming Approach to Dependency Hell. Proceedings of the 10th ACM International Workshop on Context-Oriented Programming: Advanced Modularity for Run-time Composition. (8-14).

    https://doi.org/10.1145/3242921.3242923

  • Atkey R. Syntax and Semantics of Quantitative Type Theory. Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. (56-65).

    https://doi.org/10.1145/3209108.3209189

  • Asăvoae I, Asăvoae M and Riesco A. (2018). Context-Updates Analysis and Refinement in Chisel. Model Checking Software. 10.1007/978-3-319-94111-0_19. (328-346).

    http://link.springer.com/10.1007/978-3-319-94111-0_19

  • Osvald L, Essertel G, Wu X, Alayón L and Rompf T. (2016). Gentrification gone too far? affordable 2nd-class values for fun and (co-)effect. ACM SIGPLAN Notices. 51:10. (234-251). Online publication date: 5-Dec-2016.

    https://doi.org/10.1145/3022671.2984009

  • Gaboardi M, Katsumata S, Orchard D, Breuvart F and Uustalu T. (2016). Combining effects and coeffects via grading. ACM SIGPLAN Notices. 51:9. (476-489). Online publication date: 5-Dec-2016.

    https://doi.org/10.1145/3022670.2951939

  • Morris J. (2016). The best of both worlds: linear functional programming without compromise. ACM SIGPLAN Notices. 51:9. (448-461). Online publication date: 5-Dec-2016.

    https://doi.org/10.1145/3022670.2951925

  • Osvald L, Essertel G, Wu X, Alayón L and Rompf T. Gentrification gone too far? affordable 2nd-class values for fun and (co-)effect. Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications. (234-251).

    https://doi.org/10.1145/2983990.2984009

  • Gaboardi M, Katsumata S, Orchard D, Breuvart F and Uustalu T. Combining effects and coeffects via grading. Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. (476-489).

    https://doi.org/10.1145/2951913.2951939

  • Morris J. The best of both worlds: linear functional programming without compromise. Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. (448-461).

    https://doi.org/10.1145/2951913.2951925

  • Orchard D and Yoshida N. (2016). Using session types as an effect system. Electronic Proceedings in Theoretical Computer Science. 10.4204/EPTCS.203.1. 203. (1-13).

    http://arxiv.org/abs/1602.03591

  • McBride C. (2016). I Got Plenty o’ Nuttin’. A List of Successes That Can Change the World. 10.1007/978-3-319-30936-1_12. (207-233).

    http://link.springer.com/10.1007/978-3-319-30936-1_12

  • Dumas J, Duval D, Ekici B, Pous D and Reynaud J. Relative Hilbert-Post Completeness for Exceptions. Revised Selected Papers of the 6th International Conference on Mathematical Aspects of Computer and Information Sciences - Volume 9582. (596-610).

    https://doi.org/10.1007/978-3-319-32859-1_51

  • Hughes J and Orchard D. Program Synthesis from Graded Types. Programming Languages and Systems. (83-112).

    https://doi.org/10.1007/978-3-031-57262-3_4

  • Bianchini R, Dagnino F, Giannini P and Zucca E. (2023). A Java-like Calculus with Heterogeneous Coeffects. Theoretical Computer Science. 10.1016/j.tcs.2023.114063. (114063). Online publication date: 1-Jul-2023.

    https://linkinghub.elsevier.com/retrieve/pii/S0304397523003766

  • Melicher D, Xu A, Zhao V, Potanin A and Aldrich J. (2022). Bounded Abstract Effects. ACM Transactions on Programming Languages and Systems. 44:1. (1-48). Online publication date: 31-Mar-2022.

    https://doi.org/10.1145/3492427

  • Wood J and Atkey R. (2022). A Framework for Substructural Type Systems. Programming Languages and Systems. 10.1007/978-3-030-99336-8_14. (376-402).

    https://link.springer.com/10.1007/978-3-030-99336-8_14

  • Hughes J, Vollmer M and Orchard D. (2021). Deriving Distributive Laws for Graded Linear Types. Electronic Proceedings in Theoretical Computer Science. 10.4204/EPTCS.353.6. 353. (109-131).

    http://arxiv.org/abs/2112.14966v1

  • Elizarov R, Belyaev M, Akhin M and Usmanov I. Kotlin coroutines: design and implementation. Proceedings of the 2021 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software. (68-84).

    https://doi.org/10.1145/3486607.3486751

  • Uustalu T and Voorneveld N. Algebraic and Coalgebraic Perspectives on Interaction Laws. Programming Languages and Systems. (186-205).

    https://doi.org/10.1007/978-3-030-64437-6_10

  • McBride C. (2016). I Got Plenty o’ Nuttin’. A List of Successes That Can Change the World. 10.1007/978-3-319-30936-1_12. (207-233).

    http://link.springer.com/10.1007/978-3-319-30936-1_12

  • Dumas J, Duval D, Ekici B, Pous D and Reynaud J. Relative Hilbert-Post Completeness for Exceptions. Revised Selected Papers of the 6th International Conference on Mathematical Aspects of Computer and Information Sciences - Volume 9582. (596-610).

    https://doi.org/10.1007/978-3-319-32859-1_51

  • Mycroft A, Orchard D and Petricek T. Effect Systems Revisited--Control-Flow Algebra and Semantics. Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays on Semantics, Logics, and Calculi - Volume 9560. (1-32).

    https://doi.org/10.1007/978-3-319-27810-0_1