Previous Papers

In reverse chronological order.

Date	Paper	Presented By
12 May 2026	William R. Cook. 2009. On understanding data abstraction, revisited. In Proceedings of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applications (OOPSLA ’09), October 25, 2009. Association for Computing Machinery, New York, NY, USA, 557–572. https://doi.org/10.1145/1640089.1640133
05 May 2026	Daan Leijen. 2017. Structured asynchrony with algebraic effects. In Proceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development (TyDe 2017), September 03, 2017. Association for Computing Machinery, New York, NY, USA, 16–29. https://doi.org/10.1145/3122975.3122977
28 Apr 2026	Sam Lindley. 2014. Algebraic effects and effect handlers for idioms and arrows. In Proceedings of the 10th ACM SIGPLAN workshop on Generic programming, August 26, 2014. ACM, Gothenburg Sweden, 47–58. https://doi.org/10.1145/2633628.2633636
21 Apr 2026	Tom Schrijvers, Maciej Piróg, Nicolas Wu, and Mauro Jaskelioff. 2019. Monad transformers and modular algebraic effects: what binds them together. In Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell (Haskell 2019), August 08, 2019. Association for Computing Machinery, New York, NY, USA, 98–113. https://doi.org/10.1145/3331545.3342595
14 Apr 2026	sections 4 through 10 inclusive of: Andrey Mokhov, Neil Mitchell, and Simon Peyton Jones. 2020. Build systems à la carte: Theory and practice. Journal of Functional Programming 30, (January 2020), e11. https://doi.org/10.1017/S0956796820000088
07 Apr 2026	sections 1 through 5 inclusive of: Andrey Mokhov, Neil Mitchell, and Simon Peyton Jones. 2020. Build systems à la carte: Theory and practice. Journal of Functional Programming 30, (January 2020), e11. https://doi.org/10.1017/S0956796820000088
31 Mar 2026	John H. Howard. 1976. Proving monitors. Commun. ACM 19, 5 (May 1976), 273–279. https://doi.org/10.1145/360051.360079
24 Mar 2026	C. A. R. Hoare. 1974. Monitors: an operating system structuring concept. Commun. ACM 17, 10 (Oct. 1974), 549–557. https://doi.org/10.1145/355620.361161
17 Mar 2026	Richard Bornat, Cristiano Calcagno, Peter O’Hearn, and Matthew Parkinson. Permission accounting in separation logic. POPL ’05, page 259–270, https://doi.org/10.1145/1040305.1040327
10 Mar 2026	Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. 1993. The essence of compiling with continuations. SIGPLAN Not. 28, 6 (June 1993), 237–247. https://doi.org/10.1145/173262.155113
03 Mar 2026	Amr Sabry and Matthias Felleisen. 1992. Reasoning about programs in continuation-passing style. SIGPLAN Lisp Pointers V, 1 (January 1992), 288–298. https://doi.org/10.1145/141478.141563
24 Feb 2026	(Continued) William R. Cook, Walter Hill, and Peter S. Canning. 1989. Inheritance is not subtyping. In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '90). Association for Computing Machinery, New York, NY, USA, 125–135. https://doi.org/10.1145/96709.96721
17 Feb 2026	William R. Cook, Walter Hill, and Peter S. Canning. 1989. Inheritance is not subtyping. In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '90). Association for Computing Machinery, New York, NY, USA, 125–135. https://doi.org/10.1145/96709.96721
10 Feb 2026	Luc Maranget. 2008. Compiling pattern matching to good decision trees. In Proceedings of the 2008 ACM SIGPLAN workshop on ML - ML ’08, 2008. ACM Press, Victoria, BC, Canada, 35. https://doi.org/10.1145/1411304.1411311
03 Feb 2026	Patrick Redmond, Jonathan Castello, José Manuel Calderón Trilla, and Lindsey Kuper. 2025. Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern. Proc. ACM Program. Lang. 9, OOPSLA2 (October 2025), 1–28. https://doi.org/10.1145/3763050
27 Jan 2026	David Binder and Lean Ermantraut. The Algebra of Patterns. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 2:1-2:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ECOOP.2025.2
20 Jan 2026	Olivier Danvy. 2003. A Rational Deconstruction of Landin’s SECD Machine. BRICS Report Series 33 (October 2003). https://doi.org/10.7146/brics.v10i33.21801
13 Jan 2026	P. J. Landin, The Mechanical Evaluation of Expressions, The Computer Journal, Volume 6, Issue 4, January 1964, Pages 308–320, https://doi.org/10.1093/comjnl/6.4.308
09 Dec 2025	Ralf Hinze, Nicolas Wu, and Jeremy Gibbons. 2015. Conjugate Hylomorphisms -- Or: The Mother of All Structured Recursion Schemes. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '15). Association for Computing Machinery, New York, NY, USA, 527–538. https://doi.org/10.1145/2676726.2676989
02 Dec 2025	Xueying Qin, Liam O’Connor, Rob van Glabbeek, Peter Höfner, Ohad Kammar, and Michel Steuwer. 2024. Shoggoth: A Formal Foundation for Strategic Rewriting. Proc. ACM Program. Lang. 8, POPL, Article 3 (January 2024), 29 pages. https://doi.org/10.1145/3633211
25 Nov 2025	Oghenevwogaga Ebresafe, Ian Zhao, Ende Jin, Arthur Bright, Charles Jian, and Yizhou Zhang. 2025. Certified Compilers à la Carte. Proc. ACM Program. Lang. 9, PLDI, Article 162 (June 2025), 24 pages. https://doi.org/10.1145/3729261
18 Nov 2025	András Kovács. 2022. Staged compilation with two-level type theory. Proc. ACM Program. Lang. 6, ICFP (August 2022), 110:540-110:569. https://doi.org/10.1145/3547641
11 Nov 2025	Andrew Wagner, Olek Gierczak, Brianna Marshall, John M. Li, and Amal Ahmed. 2025. From Linearity to Borrowing. Proc. ACM Program. Lang. 9, OOPSLA2, Article 415 (October 2025), 27 pages. https://doi.org/10.1145/3764117 https://doi.org/10.1145/3764117
05 Nov 2025	Talk: Edwin Park. Formalising Oracle Computability in Lean. We formalise foundational results in degree theory in Lean, up to Kleene and Post’s theorem on the existence of incomparable sets below the halting set K. We build our theory from a concrete model of computation, namely Kleene’s μ-recursive functions, without relying on synthetic computability axioms. We demonstrate that, contrary to previous assumptions, such a non-synthetic formalisation of computability theory does not result in a large overhead in proofs, once basic primitives like the evaluation and use function are constructed.	Edwin Park
28 Oct 2025	Talk: Paraconsistent Mathematics Formalized in Isabelle. This is an introduction to paraconsistent (inconsistency-tolerant) logic and mathematics, as formalized in Isabelle.	Zach, Ellie
21 Oct 2025	Hrutvik Kanabar, Samuel Vivien, Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Johannes Åman Pohjola, and Riccardo Zanetti. 2023. PureCake: A Verified Compiler for a Lazy Functional Language. Proc. ACM Program. Lang. 7, PLDI, Article 145 (June 2023), 25 pages. https://doi.org/10.1145/3591259
14 Oct 2025	Gerard P. Huet. 1973. The undecidability of unification in third order logic. Information and Control, Volume 22, Issue 3. Pages 257-267. ISSN 0019-9958. https://doi.org/10.1016/S0019-9958(73)90301-X
07 Oct 2025	Robin Milner. 1978. A theory of type polymorphism in programming. Journal of Computer and System Sciences 17, 3 (December 1978), 348–375. https://doi.org/10.1016/0022-0000(78)90014-4
30 Sep 2025	Sacha-Élie Ayoun, Xavier Denis, Petar Maksimović, and Philippa Gardner. 2025. A Hybrid Approach to Semi-automated Rust Verification. Proc. ACM Program. Lang. 9, PLDI, Article 186 (June 2025), 23 pages. https://doi.org/10.1145/3729289
23 Sep 2025	Presentation of Neil's PhD research, on a formalised dependently typed DSL for data serialisation/deserialisation.	Neil
16 Sep 2025	Conor McBride. 2008. Clowns to the left of me, jokers to the right (pearl): dissecting data structures. In Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '08). Association for Computing Machinery, New York, NY, USA, 287–295. https://doi.org/10.1145/1328438.1328474
09 Sep 2025	Pamela Zave. 2017. Reasoning about identifier spaces: How to make Chord correct. IEEE Transactions on Software Engineering, 43(12):1144-1156, December , DOI=https://doi.org/10.1109/TSE.2017.2655056
02 Sep 2025	Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. 2021. Egg: Fast and extensible equality saturation. Proc. ACM Program. Lang. 5, POPL, Article 23 (January 2021), 29 pages. https://doi.org/10.1145/3434304
26 Aug 2025	Anton Lorenzen. 2025. Lightweight Testing of Persistent Amortized Time Complexity in the Credit Monad. Technical Report, University of Edinburgh. https://antonlorenzen.de/papers/creditmonad.pdf
19 Aug 2025	P-E. Dagand. 2017. The essence of ornaments. Journal of Functional Programming. 27:e9. https://doi.org/10.1017/S0956796816000356
12 Aug 2025	Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. 2019. Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang. 4, POPL, Article 51 (January 2020), 32 pages. https://doi.org/10.1145/3371119
05 Aug 2025	Matthew A. Hammer, Khoo Yit Phang, Michael Hicks, and Jeffrey S. Foster. 2014. Adapton: composable, demand-driven incremental computation. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '14). Association for Computing Machinery, New York, NY, USA, 156–166. https://doi.org/10.1145/2594291.2594324
29 Jul 2025	D. Vytiniotis, S. Peyton Jones, T. Schrijvers. 2007. Let Should Not Be Generalised. Proceedings of the 5th ACM SIGPLAN Workshop on Types in Language Design and Implementation. https://simon.peytonjones.org/let-generalised/
23 Jul 2025	David Chisnall, Colin Rothwell, Robert N.M. Watson, Jonathan Woodruff, Munraj Vadera, Simon W. Moore, Michael Roe, Brooks Davis, and Peter G. Neumann. 2015. Beyond the PDP-11: Architectural Support for a Memory-Safe C Abstract Machine. SIGARCH Comput. Archit. News 43, 1 (March 2015), 117–130. https://doi.org/10.1145/2786763.2694367
16 Jul 2025	N. Villani, J. Hostert, D. Dreyer, and R. Jung. 2025. Tree Borrows. Proc. ACM Program. Lang. 9, PLDI, Article 188 (June 2025), 24 pages. https://doi.org/10.1145/3735592
09 Jul 2025	A. Gundry. C. McBride A tutorial implementation of dynamic pattern unification, A dependently typed programming language implementation pearl. Preprint. https://adam.gundry.co.uk/pub/pattern-unify/
02 Jul 2025	W. Swierstra. 2008. Data types à la carte. Journal of Functional Programming. 18(4):423-436. doi:10.1017/S0956796808006758
25 Jun 2025	G. Pîrlea, V. Gladshtein, E. Kinsbruner, Q. Zhao, I. Sergey. Veil: A Framework for Automated and Interactive Verification of Transition Systems. CAV 2025
18 Jun 2025	Michael D. Adams, Eric Griffis, Thomas J. Porter, Sundara Vishnu Satish, Eric Zhao, and Cyrus Omar. 2025. Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus. Proc. ACM Program. Lang. 9, POPL, Article 73 (January 2025), 29 pages. https://doi.org/10.1145/3704909
11 Jun 2025	No Reading Group
04 Jun 2025	Erwig, M., Walkingshaw, E. 2012. Semantics First!. In: Sloane, A., Aßmann, U. (eds) Software Language Engineering. SLE 2011. Lecture Notes in Computer Science, vol 6940. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28830-2_14
28 May 2025	Carette, J., Farmer, W.M., Laskowski, P. (2018). HOL Light QE. In: Avigad, J., Mahboubi, A. (eds) Interactive Theorem Proving. ITP 2018. Lecture Notes in Computer Science, vol 10895. Springer, Cham. https://doi.org/10.1007/978-3-319-94821-8_13
21 May 2025	David M. Cerna, Temur Kutsia. Anti-unification and Generalization: A Survey. Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence (IJCAI-23). Pages 6563-6573. https://doi.org/10.24963/ijcai.2023/736
14 May 2025	Reynolds, J.C. 1984. Polymorphism is not set-theoretic. In: Kahn, G., MacQueen, D.B., Plotkin, G. (eds) Semantics of Data Types. SDT 1984. https://doi.org/10.1007/3-540-13346-1_7
07 May 2025	Martini, S. (2016). Several Types of Types in Programming Languages. In: Gadducci, F., Tavosanis, M. (eds) History and Philosophy of Computing. HaPoC 2015. IFIP Advances in Information and Communication Technology, vol 487. Springer, Cham. https://doi.org/10.1007/978-3-319-47286-7_15
30 Apr 2025	Johannes Åman Pohjola and Arve Gengelbach. A mechanised semantics for HOL with Ad-hoc overloading. Elvira Albert and Laura Kovacs (editors). LPAR23. LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, vol 73, pages 498-515. https://doi.org/10.29007/413d
23 Apr 2025	Cancelled due to public holidays
16 Apr 2025	Iavor S. Diatchki, Mike Dodds, Harrison Goldstein, Bill Harris, David A. Holland, Benoit Razet, Cole Schlesinger, and Simon Winwood. 2024. Daedalus: Safer Document Parsing. Proc. ACM Program. Lang. 8, PLDI, Article 180 (June 2024), 25 pages. https://doi.org/10.1145/3656410
09 Apr 2025	Conrad Watt. 2018. Mechanising and verifying the WebAssembly specification. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018). Association for Computing Machinery, New York, NY, USA, 53–65. https://doi.org/10.1145/3167082
02 Apr 2025	Paul Downen, Zena M. Ariola, Simon Peyton Jones, and Richard A. Eisenberg. 2020. Kinds are calling conventions. Proc. ACM Program. Lang. 4, ICFP, Article 104 (August 2020), 29 pages. https://doi.org/10.1145/3408986
28 Mar 2025	Geoff Sutcliffe. TPTP Hands On Geoff Sutcliffe is a Professor in the Department of Computer Science at the University of Miami. He received a BSc(Hons) and MSc from the University of Natal, and a PhD in Computer Science from the University of Western Australia. His research is in the area of Automated Theorem Proving (ATP), particularly in the evaluation and effective use of ATP systems. His most prominent achievements are: the first ever development of a heterogeneous parallel automated reasoning system (SSCPA); the development and ongoing maintenance of the TPTP World - the de facto standard framework for developing, testing, and applying ATP systems; and the development and ongoing organization of the CADE ATP System Competition - the world championship for classical logic ATP systems. He is one of the leaders of the StarExec project that provides computing infrastructure to logic-solving communities, to facilitate the experimental evaluation of logic solvers. The research has been supported by grants from the National Science Foundation, the German Ministry for Research, the Australian Research Council, the European Union, Amazon, and internal university grants from Edith Cowan University, James Cook University, and the University of Miami. The research has produced over 160 refereed journal, conference, and workshop papers.	Geoff Sutcliffe
19 Mar 2025	Per Martin-Löf, Constructive Mathematics and Computer Programming, Editor(s): L. Jonathan Cohen, Jerzy Łoś, Helmut Pfeiffer, Klaus-Peter Podewski, Studies in Logic and the Foundations of Mathematics, Elsevier, Volume 104, 1982, Pages 153-175, https://doi.org/10.1016/S0049-237X(09)70189-2
14 Mar 2025	Zhuo Zoey Chen, Johannes Åman Pohjola, Christine Rizkallah. A Verified Cost Model for Call-by-Push-Value. Draft.
07 Mar 2025	Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C++ concurrency. POPL '11. ACM, New York, NY, USA, 55–66. https://doi.org/10.1145/1926385.1926394
28 Feb 2025	Tim Harris, Simon Marlow, Simon Peyton-Jones, and Maurice Herlihy. 2005. Composable memory transactions. In Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming (PPoPP '05). Association for Computing Machinery, New York, NY, USA, 48–60. https://doi.org/10.1145/1065944.1065952
21 Feb 2025	Richard J. Lipton. 1975. Reduction: a method of proving properties of parallel programs. Commun. ACM 18, 12 (Dec. 1975), 717–721. https://doi.org/10.1145/361227.361234
14 Feb 2025	Rayhana Amjad, Rob van Glabbeek, Liam O’Connor. The Infinite, in Finite Time. Preprint.
07 Feb 2025	Dongjun Youn, Wonho Shin, Jaehyun Lee, Sukyoung Ryu, Joachim Breitner, Philippa Gardner, Sam Lindley, Matija Pretnar, Xiaojia Rao, Conrad Watt, and Andreas Rossberg. 2024. Bringing the WebAssembly Standard up to Speed with SpecTec. Proc. ACM Program. Lang. 8, PLDI, Article 210 (June 2024), 26 pages. https://doi.org/10.1145/3656440
31 Jan 2025	Alexander Bentkamp, Jasmin Blanchette, Visa Nummelin, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann. 2023. Mechanical Mathematicians. Commun. ACM 66, 4 (April 2023), 80–90. https://doi.org/10.1145/3557998
24 Jan 2025	Aïna Linn Georges, Benjamin Peters, Laila Elbeheiry, Leo White, Stephen Dolan, Richard A. Eisenberg, Chris Casinghino, François Pottier, and Derek Dreyer. 2025. Data Race Freedom à la Mode. Proc. ACM Program. Lang. 9, POPL, Article 23 (January 2025), 31 pages. https://doi.org/10.1145/3704859
13 Dec 2024	Luyu Cheng and Lionel Parreaux. 2024. The Ultimate Conditional Syntax. Proc. ACM Program. Lang. 8, OOPSLA2, Article 306 (October 2024), 30 pages. https://doi.org/10.1145/3689746
06 Dec 2024	Presentation: Adventures in Learning, Proving, Instantiation and Synthesis. Abstract: https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_3	Joseph Urban
29 Nov 2024	Presentation: Efficient interval reasoning for floating-point arithmetic. (part 2)	Mak Nazecic-Andrlon
22 Nov 2024	Presentation: Efficient interval reasoning for floating-point arithmetic. (part 1) Thesis: https://minerva-access.unimelb.edu.au/items/0f918540-6c84-4d2c-b384-010ca69f2566/full	Mak Nazecic-Andrlon
15 Nov 2024	Son Ho, Aymeric Fromherz, and Jonathan Protzenko. 2024. Sound Borrow-Checking for Rust via Symbolic Semantics. Proc. ACM Program. Lang. 8, ICFP, Article 251 (August 2024), 29 pages. https://doi.org/10.1145/3674640
08 Nov 2024	Ali Assaf, Guillaume Burel. Translating HOL to Dedukti. Fourth Workshop on Proof eXchange for Theorem Proving, PxTP'15, Aug 2015, Berlin, Germany. pp.74-88, ⟨10.4204/EPTCS.186.8⟩. ⟨hal-01097412v2⟩
01 Nov 2024	Mercury: an efficient purely declarative logic programming language. Zoltan Somogyi, Fergus Henderson and Thomas Conway. Proceedings of the Australian Computer Science Conference, Glenelg, Australia, February 1995, pages 499-512.
25 Oct 2024	Alejandro Russo. 2015. Functional pearl: two can keep a secret, if one of them uses Haskell. ICFP 2015. Association for Computing Machinery, New York, NY, USA, 280–288. https://doi.org/10.1145/2784731.2784756
18 Oct 2024	A. Chudnov, G. Kuan and D. A. Naumann. Information Flow Monitoring as Abstract Interpretation for Relational Logic. 2014 IEEE 27th Computer Security Foundations Symposium, Vienna, Austria, 2014. pp. 48-62, https://doi.org/10.1109/CSF.2014.12
11 Oct 2024	Talk by Aaron Bembenek. Making Formulog Fast: An Argument for Unconventional Datalog Evaluation. There is an associated paper: Aaron Bembenek, Michael Greenberg, Steven Chong. Making Formulog Fast: An Argument for Unconventional Datalog Evaluation. To appear: OOPSLA 2024.	Aaron Bembenek
04 Oct 2024	Continuing Cartesian Closed Categories and the Simply Typed Lambda Calculus.
27 Sep 2024	Public holiday at UoMelb. No RG.
20 Sep 2024	Cartesian Closed Categories and the Simply Typed Lambda Calculus.
13 Sep 2024	Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami. 2023. CN: Verifying Systems C Code with Separation-Logic Refinement Types. https://dl.acm.org/doi/10.1145/3571194.
06 Sep 2024	Talk: A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras. Associated paper: Vincent Jackson, Toby Murray, and Christine Rizkallah. A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.ITP.2024.23	Vincent
30 Aug 2024	Viktor Vafeiadis. 2011. Concurrent Separation Logic and Operational Semantics. Electronic Notes in Theoretical Computer Science, Volume 276, 2011. Pages 335-351. ISSN 1571-0661. https://doi.org/10.1016/j.entcs.2011.09.029.
23 Aug 2024	Nils Anders Danielsson, John Hughes, Patrik Jansson, and Jeremy Gibbons. 2006. Fast and loose reasoning is morally correct. In Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '06). Association for Computing Machinery, New York, NY, USA, 206–217. https://doi.org/10.1145/1111037.1111056
16 Aug 2024	Jennifer Hackett and Graham Hutton. 2019. Call-by-need is clairvoyant call-by-value. Proc. ACM Program. Lang. 3, ICFP, Article 114 (August 2019), 23 pages. https://doi.org/10.1145/3341718
06 Aug 2024	§4.2 The CYK Parsing Method of Dick Grune, Ceriel J. H. Jacobs. 2007. Parsing Techniques: A Practical Guide. Springer-Verlag New York. ISBN=978-0-387-68954-8. DOI=https://doi.org/10.1007/978-0-387-68954-8
30 Jul 2024	Sections 2‒3 (inclusive) of Chapter 4, Dirk van Dalen, Intuitionistic Logic, of Handbook of Philosophical Logic, Volume III: Alternatives to Classical Logic. 1986. Editors: Dov M. Gabbay, Franz Guenthner. Springer Science & Business Media, 2013. ISBN:9400952031. https://doi.org/10.1007/978-94-009-5203-4
25 Jun 2024	Sections 1‒2 (inclusive) of Chapter 4, Dirk van Dalen, Intuitionistic Logic, of Handbook of Philosophical Logic, Volume III: Alternatives to Classical Logic. 1986. Editors: Dov M. Gabbay, Franz Guenthner. Springer Science & Business Media, 2013. ISBN:9400952031. https://doi.org/10.1007/978-94-009-5203-4
16 Jul 2024	Jay Earley. 1970. An efficient context-free parsing algorithm. Commun. ACM 13, 2 (Feb 1970), 94–102. https://doi.org/10.1145/362007.362035
09 Jul 2024	Section §5 and onwards of Wickerson, J., Dodds, M., Parkinson, M. 2010. Explicit Stabilisation for Modular Rely-Guarantee Reasoning. ESOP 2010. https://doi.org/10.1007/978-3-642-11957-6_32
02 Jul 2024	Wickerson, J., Dodds, M., Parkinson, M. 2010. Explicit Stabilisation for Modular Rely-Guarantee Reasoning. ESOP 2010. https://doi.org/10.1007/978-3-642-11957-6_32
25 Jun 2024	Z. Paraskevopoulou, M. Fitzgibbons, M. Thalakottur, N. Mushtak, J. S. Mazur, A. Ahmed. RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly. https://dl.acm.org/doi/10.1145/3656444
18 Jun 2024	Nuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, and John Regehr. 2021. Alive2: bounded translation validation for LLVM. PLDI 2021. ACM, 65–79. https://doi.org/10.1145/3453483.3454030
11 Jun 2024	Jean Honorio Carillo. Learning Causal Networks: Identifiability, Certifiable Correctness and Efficient Algorithms	talk presented by Jean Honorio Carillo
04 Jun 2024	Roderick Chapman, Claire Dross, Stuart Matthews, and Yannick Moy. 2024. Co-Developing Programs and Their Proof of Correctness. Commun. ACM 67, 3 (March 2024), 84–94. https://doi.org/10.1145/3624728
28 May 2024	Cancelled as many travelling to the FM workshop
21 May 2024	Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011. Finding and understanding bugs in C compilers. PLDI 2011. Association for Computing Machinery, New York, NY, USA, 283–294. https://doi.org/10.1145/1993498.1993532
14 May 2024	Nick Benton. 2004. Simple relational correctness proofs for static analyses and program transformations. POPL '04. Association for Computing Machinery, New York, NY, USA, 14–25. https://doi.org/10.1145/964001.964003
07 May 2024	Matija Pretnar. An Introduction to Algebraic Effects and Handlers. Invited tutorial paper, ENTCS, Volume 319, 2015, Pages 19-35, ISSN 1571-0661, https://doi.org/10.1016/j.entcs.2015.12.003.
30 Apr 2024	Dan Grossman, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, and James Cheney. 2002. Region-based memory management in cyclone. PLDI '02. pp. 282–293. https://doi.org/10.1145/512529.512563
23 Apr 2024	Sections 5‒(end) of Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. 2008. Contextual modal type theory. ACM Trans. Comput. Logic 9, 3, Article 23 (June 2008), 49 pages. https://doi.org/10.1145/1352582.1352591
16 Apr 2024	Sections 1‒4 (inclusive) of Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. 2008. Contextual modal type theory. ACM Trans. Comput. Logic 9, 3, Article 23 (June 2008), 49 pages. https://doi.org/10.1145/1352582.1352591
09 Apr 2024	Dang, HH. (2014). Abstract Dynamic Frames. RAMICS 2014. LNCS vol 8428. Springer, Cham. https://doi.org/10.1007/978-3-319-06251-8_10
02 Apr 2024	Uni Melb holiday
26 Mar 2024	Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and Jeremy G. Siek. 2019. Gradual typing: a new perspective. Proc. ACM Program. Lang. 3, POPL, Article 16 (January 2019), 32 pages. https://doi.org/10.1145/3290329
19 Mar 2024	No RG
12 Mar 2024	Cyrus Omar, Ian Voysey, Michael Hilton, Joshua Sunshine, Claire Le Goues, Jonathan Aldrich, and Matthew A. Hammer. Toward Semantic Foundations for Program Editors. SNAPL 2017. LIPIcs, Volume 71, pp. 11:1-11:12 https://doi.org/10.4230/LIPIcs.SNAPL.2017.11
05 Mar 2024	Danielle Marshall, Dominic Orchard. Functional Ownership through Fractional Uniqueness. [arXiv:2310.18166] (https://arxiv.org/abs/2310.18166) [cs.PL]
27 Feb 2024	J. Lee, Y. Kim, Y. Song, C-K. Hur, S. Das, D. Majnemer, J. Regehr, and N. P. Lopes. 2017. Taming undefined behavior in LLVM. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). Association for Computing Machinery, New York, NY, USA, 633–647. https://doi.org/10.1145/3062341.3062343
20 Feb 2024	Andreas Lööw. 2021. Lutsig: a verified Verilog compiler for verified circuit development. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021). Association for Computing Machinery, New York, NY, USA, 46–60. https://doi.org/10.1145/3437992.3439916
13 Feb 2024	Emily First, Markus Rabe, Talia Ringer, and Yuriy Brun. 2023. Baldur: Whole-Proof Generation and Repair with Large Language Models. ESEC/FSE 2023. Association for Computing Machinery, New York, NY, USA, 1229–1241. https://doi.org/10.1145/3611643.3616243
06 Feb 2024	Cousot, P. (2001). Abstract Interpretation Based Formal Methods and Future Challenges. In: Wilhelm, R. (eds) Informatics. Lecture Notes in Computer Science, vol 2000. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44577-3_10
30 Jan 2024	N. Halbwachs. A synchronous language at work: the story of Lustre. Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2005. MEMOCODE '05., Verona, Italy, 2005, pp. 3-11, https://doi.org/10.1109/MEMCOD.2005.1487884
23 Jan 2024	Patrick Baudin, François Bobot, David Bühler, Loïc Correnson, Florent Kirchner, Nikolai Kosmatov, André Maroneze, Valentin Perrelle, Virgile Prevosto, Julien Signoles, and Nicky Williams. 2021. The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Commun. ACM 64, 8 (August 2021), 56–68. https://doi.org/10.1145/3470569
19 Dec 2023	Al Bessey, Ken Block, Ben Chelf, Andy Chou, Bryan Fulton, Seth Hallem, Charles Henri-Gros, Asya Kamsky, Scott McPeak, and Dawson Engler. 2010. A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM 53, 2 (February 2010), 66–75. https://doi.org/10.1145/1646353.1646374
12 Dec 2023	Brandon Hewer and Graham Hutton. 2024. Quotient Haskell: Lightweight Quotient Types for All. Proc. ACM Program. Lang. 1, POPL, Article 1 (January 2024), 31 pages. https://www.cs.nott.ac.uk/~pszgmh/quotient-haskell.pdf
05 Dec 2023	Edsger W. Dijkstra. 1975. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18, 8 (August 1975), 453–457. http://doi.org/10.1145/360933.360975
28 Nov 2023	Floyd, Robert W. 1967. Assigning Meaning to Programs. Mathematical Aspects of Computer Science (Proceedings of a Symposium in Applied Mathematics) (ed. J. T. Schwarz), Volume 19, American Mathematical Society. pp. 19–32. doi: https://doi.org/10.1090/psapm/019 Carroll Morgan annotated copy
21 Oct 2023	F. L. Morris and C. B. Jones. An Early Program Proof by Alan Turing. Annals of the History of Computing, vol. 6, no. 2, pp. 139-143. April-June 1984. doi.org/10.1109/MAHC.1984.10017
14 Oct 2023	Urban, C. Nominal Techniques in Isabelle/HOL. J Autom Reasoning 40, 327–356 (2008). https://doi.org/10.1007/s10817-008-9097-2
07 Oct 2023	D. Patterson, N. Mushtak, A. Wagner, and A. Ahmed. 2022. Semantic soundness for language interoperability. PLDI 2022. ACM, 609–624. https://doi.org/10.1145/3519939.3523703
31 Oct 2023	Chris Hathhorn, Chucky Ellison, and Grigore Roşu. 2015. Defining the undefinedness of C. PLDI '15. ACM, 336–345. https://doi.org/10.1145/2737924.2737979
24 Oct 2023	Cancelled due to the CIS Doctoral Colloquium
17 Oct 2023	Abdul Dakkak, Tom Wickham-Jones, and Wen-mei Hwu. 2020. The design and implementation of the wolfram language compiler. CGO 2020. ACM. https://doi.org/10.1145/3368826.3377913
10 Oct 2023	Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco, Ana Nora Evans, Guglielmo Fachini, Catalin Hritcu, Théo Laurent, Benjamin C. Pierce, Marco Stronati, and Andrew Tolmach. 2018. When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (CCS '18). Association for Computing Machinery, New York, NY, USA, 1351–1368. https://doi.org/10.1145/3243734.3243745
03 Oct 2023	Santosh Nagarakatte, Jianzhou Zhao, Milo M.K. Martin, and Steve Zdancewic. 2009. SoftBound: highly compatible and complete spatial memory safety for c. In Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '09). Association for Computing Machinery, New York, NY, USA, 245–258. https://doi.org/10.1145/1542476.1542504
26 Sep 2023	Thaïs Baudon, Gabriel Radanne, and Laure Gonnord. 2023. Bit-Stealing Made Legal: Compilation for Custom Memory Representations of Algebraic Data Types. Proc. ACM Program. Lang. 7, ICFP, Article 216 (August 2023), 34 pages. https://doi.org/10.1145/3607858
19 Sep 2023	Pierre-Marie Pédrot. 2014. A functional functional interpretation. CSL-LICS '14. Association for Computing Machinery, New York, NY, USA, Article 77, 1–10. https://doi.org/10.1145/2603088.2603094
12 Sep 2023	Michael Arntzenius and Neelakantan R. Krishnaswami. 2016. Datafun: a functional Datalog. ICFP 2016. pp. 214–227. https://doi.org/10.1145/2951913.2951948
05 Sep 2023	S. Ceri, G. Gottlob, L. Tanca. 1989. What you always wanted to know about Datalog (and never dared to ask). IEEE Transactions on Knowledge and Data Engineering. DOI:doi.org/10.1109/69.43410
29 Aug 2023	L. Kuper, A. Turon, N. Krishnaswami, and R. Newton. 2014. Freeze after writing: quasi-deterministic parallel programming with LVars. POPL '14. https://doi.org/10.1145/2535838.2535842
22 Aug 2023	Joseph M. Hellerstein and Peter Alvaro. 2020. Keeping CALM: when distributed consistency is easy. Commun. ACM 63, 9 (September 2020), 72–81. https://doi.org/10.1145/3369736
15 Aug 2023	Ruy Ley-Wild and Aleksandar Nanevski. 2013. Subjective auxiliary state for coarse-grained concurrency. POPL '13. https://doi.org/10.1145/2429069.2429134
08 Aug 2023	Chang, E., Manna, Z., Pnueli, A. (1992). Characterization of temporal property classes. In: Automata, Languages and Programming. ICALP 1992. https://doi.org/10.1007/3-540-55719-9_97
01 Aug 2023	Noam Zilberstein, Derek Dreyer, and Alexandra Silva. 2023. Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning. Proc. ACM Program. Lang. 7, OOPSLA1, Article 93 (April 2023), 29 pages. https://doi.org/10.1145/3586045
25 Jul 2023	Peter W. O’Hearn. 2020. Incorrectness Logic. Proc. ACM Program. Lang. 4, POPL, Article 10 (January 2020), 32 pages. https://doi.org/10.1145/3371078
18 Jul 2023	D. Ahman, C. Fournet, C. Hriţcu, K. Maillard, A. Rastogi, and N. Swamy. 2017. Recalling a witness: foundations and applications of monotonic state. POPL 2018, 30 pages. https://doi.org/10.1145/3158153
11 Jul 2023	A. Bohannon, J.N. Foster, B.C. Pierce, A. Pilkiewicz, and A. Schmitt. 2008. Boomerang: resourceful lenses for string data. POPL '08. Association for Computing Machinery, New York, NY, USA, 407–419. https://doi.org/10.1145/1328438.1328487
04 Jul 2023	§1‒4 (inclusive) of Son Ho, Jonathan Protzenko. Aeneas: Rust Verification by Functional Translation. arXiv:2206.07185 [cs.PL]. DOI=https://doi.org/10.48550/arXiv.2206.07185
27 Jun 2023	§5 onwards of Yang, Z., Wu, N. (2022). Fantastic Morphisms and Where to Find Them. In: Komendantskaya, E. (eds) Mathematics of Program Construction. MPC 2022. Lecture Notes in Computer Science, vol 13544. Springer, Cham. https://doi.org/10.1007/978-3-031-16912-0_9
20 Jun 2023	§1‒§5 (inclusive) of Yang, Z., Wu, N. (2022). Fantastic Morphisms and Where to Find Them. In: Komendantskaya, E. (eds) Mathematics of Program Construction. MPC 2022. Lecture Notes in Computer Science, vol 13544. Springer, Cham. https://doi.org/10.1007/978-3-031-16912-0_9
13 Jun 2023	Oege de Moor, Jeremy Gibbons, Bridging the algorithm gap: A linear-time functional program for paragraph formatting, Science of Computer Programming, Volume 35, Issue 1, 1999, Pages 3-27, ISSN 0167-6423, https://doi.org/10.1016/S0167-6423(99)00005-2
06 Jun 2023	Philip Wadler. 2003. A perttier printer. The Fun of Programming. Richard Bird's 60th Birthday Symposium. Oxford. (Original paper April 1997, revised March 1998.)
30 May 2023	Conor McBride. 2008. Clowns to the left of me, jokers to the right (pearl): dissecting data structures. POPL '08. https://doi.org/10.1145/1328438.1328474
23 May 2023	Sections 1, 2, 4.3, 5.3, and 5.5 of Goranko, Valentin and Antje Rumberg, "Temporal Logic", The Stanford Encyclopedia of Philosophy (Summer 2022 Edition), Edward N. Zalta (ed.), URL: https://plato.stanford.edu/archives/sum2022/entries/logic-temporal/.
16 May 2023	Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H. (2000). Counterexample-Guided Abstraction Refinement . CAV 2000. LNCS 1855. https://doi.org/10.1007/10722167_15
09 May 2023	Pierre Wolper. 1986. Expressing interesting properties of programs in propositional temporal logic. POPL '86. https://doi.org/10.1145/512644.512661
02 May 2023	Cao, Q., Cuellar, S., Appel, A.W. (2017). Bringing Order to the Separation Logic Jungle. APLAS 2017. https://doi.org/10.1007/978-3-319-71237-6_10
25 Apr 2023	Cancelled. Public holiday.
18 Apr 2023	Verifying memory safety: Integrating type and proof theory.	Selene
11 Apr 2023	Cancelled. UMelb holiday.
04 Apr 2023	Verification of Neural Networks.	Zilin
28 Mar 2023	Jean-Yves Girard. 1993. On the unity of logic. Annals of Pure and Applied Logic, Volume 59, Issue 3, https://doi.org/10.1016/0168-0072(93)90093-S
21 Mar 2023	Henry DeYoung, Frank Pfenning. Data Layout from a Type-Theoretic Perspective. Electronic Notes in Theoretical Informatics and Computer Science, February 22, 2023, Volume 1. https://doi.org/10.46298/entics.10507
14 Mar 2023	Pimentel, E., Pereira, L.C. & de Paiva, V. An ecumenical notion of entailment. Synthese 198 (Suppl 22), 5391–5413 (2021). https://doi.org/10.1007/s11229-019-02226-5
07 Mar 2023	The Runabout Inference-Ticket. A. N. Prior. Analysis, Volume 21, Issue 2, December 1960, Pages 38–39, https://doi.org/10.1093/analys/21.2.38 and Tonk, Plonk and Plink. Nuel D. Belnap. Analysis, Volume 22, Issue 6, June 1962, Pages 130–134, https://doi.org/10.1093/analys/22.6.130
28 Feb 2023	Dana Harrington, Uniqueness logic, Theoretical Computer Science, Volume 354, Issue 1, 2006, https://doi.org/10.1016/j.tcs.2005.11.006
21 Feb 2023	Levy, P.B. (1999). Call-by-Push-Value: A Subsuming Paradigm. TLCA 1999. https://doi.org/10.1007/3-540-48959-2_17
14 Feb 2023	Ben Lippmeier. Don’t Substitute Into Abstractions (Functional Pearl). Preprint. p1-6.
07 Feb 2023	Gordon, A.D. (1995). A Tutorial on Co-induction and Functional Programming. Functional Programming, Glasgow 1994. https://doi.org/10.1007/978-1-4471-3573-9_6
31 Jan 2023	Sections 1‒3 (inclusive) of Marshall, D., Vollmer, M., Orchard, D. (2022). Linearity and Uniqueness: An Entente Cordiale. ESOP 2022. https://doi.org/10.1007/978-3-030-99336-8_13
24 Jan 2023	Conal Elliott. 2021. Symbolic and automatic differentiation of languages. Proc. ACM Program. Lang. 5, ICFP, Article 78 (August 2021), 18 pages. https://doi.org/10.1145/3473583
13 Dec 2022	Talk. Title: Formal verification of an industrial OS micro-kernel: an experience report Abstract: This talk is about a project of formal verification of an OS micro-kernel I worked on a few years back: Which choices did we make? What were the challenges we faced? What lessons did we learn? And how it created the need to develop new kinds of static analyses.	Benoît Montagu
06 Dec 2022	Olivier Danvy and Mayer Goldberg. 2002. There and back again. ICFP '02. 230–234. https://doi.org/10.1145/581478.581500
29 Nov 2022	Sections 1‒4 (inclusive) (equivalently, up to page 19) of Timany, A., Krebbers, R., Dreyer, D., Birkedal, L. 2022. A Logical Approach to Type Soundness. Preprint.
22 Nov 2022	Dal Lago, U. (2022). Implicit computation complexity in higher-order programming languages: A Survey in Memory of Martin Hofmann. Mathematical Structures in Computer Science, 1-17. doi.org/10.1017/S0960129521000505
15 Nov 2022	Owens, S., Reppy, J., & Turon, A. (2009). Regular-expression derivatives re-examined. Journal of Functional Programming, 19(2), 173-190. doi.org/10.1017/S0956796808007090
08 Nov 2022	Vafeiadis, V., Parkinson, M. (2007). A Marriage of Rely/Guarantee and Separation Logic. CONCUR 2007. https://doi.org/10.1007/978-3-540-74407-8_18 (continued)
01 Nov 2022	Cancelled
25 Oct 2022	Vafeiadis, V., Parkinson, M. (2007). A Marriage of Rely/Guarantee and Separation Logic. CONCUR 2007. https://doi.org/10.1007/978-3-540-74407-8_18
18 Oct 2022	Pengbo Yan and Toby Murray. 2021. SecRSL: security separation logic for C11 release-acquire concurrency. Proc. ACM Program. Lang. 5, OOPSLA, Article 99 (October 2021), 26 pages. https://doi.org/10.1145/3485476	Pengbo
11 Oct 2022	Viktor Vafeiadis and Chinmay Narayan. 2013. Relaxed separation logic: a program logic for C11 concurrency. In Proceedings of the 2013. OOPSLA '13. https://doi.org/10.1145/2509136.2509532	Pengbo
02 Oct 2022	Leuschel, M., Tamarit, S., Vidal, G. (2010). Fast and Accurate Strong Termination Analysis with an Application to Partial Evaluation. WFLP 2009. https://doi.org/10.1007/978-3-642-11999-6_8
27 Sep 2022	Cancelled
20 Sep 2022	Yao Li and Stephanie Weirich. 2022. Program Adverbs and Tlön Embeddings. Proc. ACM Program. Lang. 6, ICFP, Article 101 (August 2022), 32 pages. https://doi.org/10.1145/3547632 https://arxiv.org/pdf/2207.05227.pdf
13 Sep 2022	Louis presented on suffix arrays	Louis
06 Sep 2022	Feedback session for Zilin's thesis
30 Aug 2022	Derek Dreyer, Karl Crary, and Robert Harper. 2003. A type system for higher-order modules. SIGPLAN Not. 38, 1 (January 2003), 236–249. https://doi.org/10.1145/640128.604151
23 Aug 2022	Karl Crary. 2019. Fully abstract module compilation. Proc. ACM Program. Lang. 3, POPL, Article 10 (January 2019), 29 pages. https://doi.org/10.1145/3290323
16 Aug 2022	Cancelled
09 Aug 2022	Joshua Yanovski, Hoang-Hai Dang, Ralf Jung, and Derek Dreyer. 2021. GhostCell: Separating Permissions from Data in Rust.Proc. ACM Program. Lang. 5, ICFP, Article 92 (August 2021), 30 pages. https://doi.org/10.1145/3473597 (cont'd)
02 Aug 2022	Joshua Yanovski, Hoang-Hai Dang, Ralf Jung, and Derek Dreyer. 2021. GhostCell: Separating Permissions from Data in Rust.Proc. ACM Program. Lang. 5, ICFP, Article 92 (August 2021), 30 pages. https://doi.org/10.1145/3473597
26 Jul 2022	Raphael to present his work on termination checking	Raphael
19 Jul 2022	Andreas Abel, Thorsten Altenkirch. 2002. A predicative analysis of structural recursion. JFP. https://doi.org/10.1017/S0956796801004191
12 Jul 2022	Derek Dreyer. Milner Award Lecture: The Type Soundness Theorem That You Really Want to Prove (and now you can (https://www.youtube.com/watch?v=8Xyk_dGcAwk). POPL 2018.
05 Jul 2022	Zilin presents his paper draft: A Hoare-Logic Style Refinement Types Formalisation (to appear in TyDe'22)	Zilin
28 Jun 2022	A.K. Wright, M. Felleisen. 1994. A Syntactic Approach to Type Soundness. Information and Computation, Volume 115, Issue 1, 1994, Pages 38-94, ISSN 0890-5401. https://doi.org/10.1006/inco.1994.1093 (Cont'd)
21 Jun 2022	Shortest path formalisation by Christine	Christine
14 Jun 2022	In person free discussion @ UoM
07 Jun 2022	A.K. Wright, M. Felleisen. 1994. A Syntactic Approach to Type Soundness. Information and Computation, Volume 115, Issue 1, 1994, Pages 38-94, ISSN 0890-5401. https://doi.org/10.1006/inco.1994.1093
31 May 2022	Zoey's HOL formalisation of cost models for weak call by value lambda calculus. (Part 3)	Zoey
24 May 2022	The second half of Chapter 13: Abstract Interpretation. Tobias Nipkow, Gerwin Klein. 2021. Concrete Semantics with Isabelle/HOL. Springer-Verlag.
17 May 2022	Zoey's HOL formalisation of cost models for weak call by value lambda calculus. (Part 2)	Zoey
10 May 2022	The first half of Chapter 13: Abstract Interpretation. Tobias Nipkow, Gerwin Klein. 2021. Concrete Semantics with Isabelle/HOL. Springer-Verlag.
03 May 2022	Zoey's HOL formalisation of cost models for weak call by value lambda calculus. (Part 1) Her formalisation: https://github.com/ZhuoZoeyChen/HOL-wcbv-reasonable It is based on the Coq formalisation: https://ps.uni-saarland.de/extras/wcbv-reasonable/	Zoey
26 Apr 2022	Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B. (2012). Frama-C. SEFM 2012. Lecture Notes in Computer Science, vol 7504. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33826-7_16
19 Apr 2022	No RG due to UoMelb Easter Holiday
12 Apr 2022	Selene's Isabelle formalisation on memory safety (cont'd)	Selene
05 Apr 2022	Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. 2020. The Machinery of Interaction. PPDP '20. Association for Computing Machinery, New York, NY, USA, Article 4, 1–15. DOI:https://doi.org/10.1145/3414080.3414108
29 Mar 2022	Selene's Isabelle formalisation on memory safety. Reference: https://arxiv.org/pdf/1705.07354.pdf	Selene
22 Mar 2022	John C. Mitchell and Gordon D. Plotkin. 1988. Abstract types have existential type. ACM Trans. Program. Lang. Syst. 10, 3 (July 1988), 470–502. DOI:https://doi.org/10.1145/44501.45065
15 Mar 2022	Zilin's Agda formalisation on refinement types	Zilin
08 Mar 2022	Dybjer, P. (2000). A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65(2), 525-549. doi:https://doi.org/10.2307/2586554
01 Mar 2022	Vincent's sep logic formalisation. (part 2)	Vincent
22 Feb 2022	Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory. ACM Trans. Program. Lang. Syst. 36, 2, Article 7 (July 2014), 74 pages. DOI:https://doi.org/10.1145/2627752 from sections 1 through to 4 (inclusive).
15 Feb 2022	Vincent's sep logic formalisation. Suggested reading: * Alexey Gotsman, Josh Berdine, Byron Cook. 2011. Precision and the Conjunction Rule in Concurrent Separation Logic. Electronic Notes in Theoretical Computer Science, Volume 276. Pages 171-190, DOI:https://doi.org/10.1016/j.entcs.2011.09.021. * Stephen Brookes and Peter W. O'Hearn. 2016. Concurrent separation logic. ACM SIGLOG News 3, 3 (July 2016), 47–65. DOI:https://doi.org/10.1145/2984450.2984457	Vincent
08 Feb 2022	Dalvandi, S., Dongol, B., Doherty, S. et al. Integrating Owicki–Gries for C11-Style Memory Models into Isabelle/HOL. J Autom Reasoning 66, 141–171 (2022). https://doi.org/10.1007/s10817-021-09610-2
01 Feb 2022	Austin's formalisation on CBPV	Austin
17 Jan 2022	Pearce D.J. (2013) Sound and Complete Flow Typing with Unions, Intersections and Negations. VMCAI 2013. https://doi.org/10.1007/978-3-642-35873-9_21.
30 Nov 2021	David Walker, Kevin Watkins. 2001. On Regions and Linear Types (Extended Abstract). ICFP 6.
02 Nov 2021	Azevedo de Amorim A., Hriţcu C., Pierce B.C. (2018) The Meaning of Memory Safety. In: Bauer L., Küsters R. (eds) Principles of Security and Trust. POST 2018. Lecture Notes in Computer Science, vol 10804. Springer, Cham. https://doi.org/10.1007/978-3-319-89722-6_4
06 Oct 2021	Arnaud Spiwack. A Dissection Of L. Technical Report
29 Sep 2021	Coq formalisation session
21 Sep 2021	P. Dagand and L. Rieg and G. Scherer. 2020 . Dependent Pearl: Normalization by realizability. arXiv:1908.09123
14 Sep 2021	Coq formalisation session
07 Sep 2021	Coq formalisation session
31 Aug 2021	Slind, Konrad. Specifying Message Formats with Contiguity Types. ITP 2021. DOI=https://doi.org/10.4230/LIPIcs.ITP.2021.30.
24 Aug 2021	Coq formalisation session
10 Aug 2021	Coq formalisation session
03 Aug 2021	Aleksandar Nanevski, Viktor Vafeiadis, and Josh Berdine. 2010. Structuring the verification of heap-manipulating programs. POPL '10. DOI:https://doi.org/10.1145/1706299.1706331
13 Jul 2021	Michael Sammler, et. al. 2021. RefinedC: automating the foundational verification of C code with refined ownership types. PLDI 2021. DOI:https://doi.org/10.1145/3453483.3454036
08 Jun 2021	Noam Zeilberger. 2008. Focusing and higher-order abstract syntax. POPL '08. pp. 359–369. DOI:https://doi.org/10.1145/1328438.1328482
01 Jun 2021	David Van Horn and Matthew Might. 2010. Abstracting abstract machines. ICFP '10. Association for Computing Machinery, New York, NY, USA, 51–62. DOI:https://doi.org/10.1145/1863543.1863553
25 May 2021	The IRIS Team. Iris tutorial POPL 2021. Video Tutorial
18 May 2021	G. Bierman, A. Gordon, C. Hriţcu, and D. Langworthy. 2010. ICFP '10. pp. 105–116. DOI:https://doi.org/10.1145/1863543.1863560
11 May 2021	Piecha, T., Schroeder-Heister, P. 2019. Incompleteness of Intuitionistic Propositional Logic with Respect to Proof-Theoretic Semantics. Studia Logica 107, pp. 233–246. https://doi.org/10.1007/s11225-018-9823-7
04 May 2021	Giuseppe Castagna and Alain Frisch. 2005. A gentle introduction to semantic subtyping. PPDP '05. pp. 198–199. DOI:https://doi.org/10.1145/1069774.1069793
27 Apr 2021, 20 Apr 2021	Nico Lehmann and Éric Tanter. 2017. Gradual refinement types. POPL 2017. pp. 775–788. DOI:https://doi.org/10.1145/3009837.3009856
13 Apr 2021	Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. 2008. Liquid types. PLDI '08. pp. 159–169. DOI:https://doi.org/10.1145/1375581.1375602
06 Apr 2021	No reading group
30 Mar 2021	D. Kesner. 2007. The Theory of Calculi with Explicit Substitutions Revisited. Computer Science Logic. CSL 2007. https://doi.org/10.1007/978-3-540-74915-8_20
23 Mar 2021	Andrew Moran and David Sands. 1999. Improvement in a lazy context: an operational theory for call-by-need. In Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '99). Association for Computing Machinery, New York, NY, USA, 43–56. DOI:https://doi.org/10.1145/292540.292547
16 Mar 2021	Patrick Cousot & Radhia Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 238‒252, Los Angeles, California. ACM Press, New York.
09 Mar 2021	Zvonimir Pavlinovic, Yusen Su, Thomas Wies. 2020. Data Flow Refinement Type Inference. https://arxiv.org/abs/2011.04876 (to appear POPL2021)
02 Mar 2021, 23 Feb 2021, 16 Feb 2021	Craig McLaughlin. Extending Cogent with resource management. Unpublished Draft	Craig
25 Jan 2021, 01 Dec 2020	Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, and Viktor Vafeiadis. 2021. PerSeVerE: Persistency Semantics for Verification under Ext4. In POPL 2021 (To Appear)
24 Nov 2020	Damien Pous. 2016. Coinduction All the Way Up. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '16). Association for Computing Machinery, New York, NY, USA, 307–316. DOI:https://dl.acm.org/doi/10.1145/2933575.2934564
17 Nov 2020	Robin Milner. (1977). Fully abstract models of typed λ-calculi. Theoretical Computer Science, Volume 4, Issue 1, 1977. pp. 1‒22. ISSN 0304-3975. DOI=https://doi.org/10.1016/0304-3975(77)90053-6
10 Nov 2020	T. Hirschowitz, A. Lafont. A categorical framework for congruence of applicative bisimilarity in higher-order languages.https://hal.archives-ouvertes.fr/hal-02966439
03 Nov 2020	Sections 5.6 onwards of Andrew Pitts. Howe’s method for higher-order languages. D. Sangorgi and J. Rutten (eds), Advanced Topics in Bisimulation and Coinduction, Cambridge Tracts in Theoretical Computer Science. No. 52, chapter 5, pages 197‒232
26 Oct 2020	Sections 5.1 up-to 5.6 of Andrew Pitts. Howe’s method for higher-order languages. D. Sangorgi and J. Rutten (eds), Advanced Topics in Bisimulation and Coinduction, Cambridge Tracts in Theoretical Computer Science. No. 52, chapter 5, pages 197‒232
19 Oct 2020	Arthur Charguéraud. 2010. Program verification through characteristic formulae. In Proceedings of the 15th ACM SIGPLAN international conference on Functional programming (ICFP'10). Association for Computing Machinery, New York, NY, USA, 321–332. DOI:https://doi.org/10.1145/1863543.1863590
12 Oct 2020	Arthur Charguéraud. 2020. Separation logic for sequential programs (functional pearl). Proc. ACM Program. Lang. 4, ICFP, Article 116 (August 2020), 34 pages. DOI:https://doi.org/10.1145/3408998
05 Oct 2020	Public Holiday
28 Sep 2020	Sections 1&2 of Robert J. Simmons. 2014. Structural Focalization. ACM Trans. Comput. Logic 15, 3, Article 21 (July 2014), 33 pages. DOI:https://doi.org/10.1145/2629678
21 Sep 2020	Chapter 3 of McLaughlin, Craig. Relational reasoning for effects and handlers. PhD Thesis. University of Edinburgh
14 Sep 2020	C. Rizkallah, D. Garbuzov and S. Zdancewic. A Formal Equational Theory for Call-By-Push-Value. Interactive Theorem Proving (ITP), pages 523‒541, 2018.
07 Sep 2020	Chapter 3 of Paul Blain Levy. 2001. Call-By-Push-Value. PhD Thesis, University of London.
31 Aug 2020	P. J. Landin. 1966. The next 700 programming languages. Commun. ACM 9, 3 (March 1966), 157-166. DOI=http://dx.doi.org/10.1145/365230.365257
24 Aug 2020	Bulwahn L., Krauss A., Nipkow T. 2007. Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL. TPHOLs 2007. LNCS vol 4732. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74591-4_5
17 Aug 2020	A. Appel. (2001). Foundational Proof-Carrying Code. Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, Boston, MA, USA, 2001. pp. 02–47. DOI=https://doi.org/10.1109/LICS.2001.932501
10 Aug 2020	Postponed
03 Aug 2020	F. Besson, S. Blazy, P. Wilke. A Concrete Memory Model for CompCert. ITP 2015 : 6th International Conference on Interactive Theorem Proving, Aug 2015, Nanjing, China. pp.67-83, DOI=https://doi.org/10.1007/978-3-319-22102-1\_5
27 Jul 2020	Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM 52, 7 (July 2009), 107–115. DOI:https://hal.inria.fr/hal-01194549
20 Jul 2020	Peter Lammich. 2019. Generating Verified LLVM from Isabelle/HOL. 10th International Conference on Interactive Theorem Proving (ITP 2019). DOI=https://doi.org/10.4230/LIPIcs.ITP.2019.22
13 Jul 2020	Adjourned
06 Jul 2020	P. Vukmirović et. al. 2020. Efficient Full Higher-Order Unification. 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). DOI=https://doi.org/10.4230/LIPIcs.FSCD.2020.5
29 Jun 2020	J. Garrett Morris. 2016. The best of both worlds: linear functional programming without compromise. SIGPLAN Not. 51, 9 (September 2016), 448–461. DOI:https://doi.org/10.1145/3022670.2951925
22 Jun 2020	Gabriel Radanne, Hannes Saffrich, Peter Thiemann. Kindly Bent to Free Us. https://arxiv.org/abs/1908.09681
15 Jun 2020	Morrisett G., Ahmed A., Fluet M. 2005. L3: A Linear Language with Locations. TLCA 2005. Lecture Notes in Computer Science, vol 3461. Springer, Berlin, Heidelberg. DOI=https://doi.org/10.1007/11417170_22
09 Jun 2020	J.L. Bell. 2004. Russell’s Paradox and Diagonalization in a Constructive Context. 100 Years of Russell’s Paradox, Munich 2001. Walter de Gruyter.
01 Jun 2020	Cyrus Omar, et. al. Hazelnut: A Bidirectionally Typed Structure Editor Calculus. https://arxiv.org/abs/1607.04180
25 May 2020	Read, S. (2015). General-Elimination Harmony and Higher-Level Rules. In: Wansing, H. (eds) Dag Prawitz on Proofs and Meaning. Outstanding Contributions to Logic, vol 7. Springer, Cham. https://doi.org/10.1007/978-3-319-11041-7_13
18 May 2020	Schroeder-Heister, P. A natural extension of natural deduction. Journal of Symbolic Logic. 1984;49(4):1284-1300. https://doi.org/10.2307/2274279
04 May 2020	Erik Palmgren. On Universes in Type Theory. in: G. Sambin and J. Smith (eds.) Twenty Five Years of Constructive Type Theory. Oxford Logic Guides, Oxford University Press 1998, 191-204 (refereed collection of papers).
29 Apr 2020	V. R. Pratt. Semantical consideration on Floyd–Hoare logic. 17th Annual Symposium on Foundations of Computer Science (sfcs 1976), Houston, TX, USA, 1976, pp. 109‒121. DOI=ttps://doi.org/10.1109/SFCS.1976.27
22 Apr 2020	Matt Brown and Jens Palsberg. 2016. Breaking through the normalization barrier: a self-interpreter for f-omega. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’16). Association for Computing Machinery, New York, NY, USA, 5–17. DOI:https://doi.org/10.1145/2837614.2837623
15 Apr 2020	Andrej Bauer, et. al. Design and Implementation of the Andromeda Proof Assistant. https://arxiv.org/abs/1802.06217
08 Apr 2020	Adjourned due to the seL4 Foundation Launch
01 Apr 2020	Malayeri, D. and Aldrich, J. (2008). Integrating Nominal and Structural Subtyping. In Proceedings of the 22nd European conference on Object-Oriented Programming (ECOOP ’08). Springer-Verlag, Berlin, Heidelberg, 260–284. DOI:https://doi.org/10.1007/978-3-540-70592-5_12
25 Mar 2020	Kiselyov O., Shan C. (2007) Delimited Continuations in Operating Systems. Modeling and Using Context (CONTEXT 2007). Lecture Notes in Computer Science, vol 4635. Springer, Berlin, Heidelberg
04 Mar 2020	Iavor S. Diatchki and Mark P. Jones. 2006. Strongly typed memory areas programming systems-level data structures in a functional language. In Proceedings of the 2006 ACM SIGPLAN workshop on Haskell (Haskell ’06). Association for Computing Machinery, New York, NY, USA, 72–83. DOI:https://doi.org/10.1145/1159842.1159851
26 Feb 2020	M. Vollmer, et al. 2019. LoCal: a language for programs operating on serialized data. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2019). Association for Computing Machinery, New York, NY, USA, 48–62. DOI:https://doi.org/10.1145/3314221.3314631
19 Feb 2020	Danel Ahman, Andrej Bauer. Runners in action. https://arxiv.org/abs/1910.11629
12 Feb 2020	Adam Gundry, Conor McBride, and James McKinna. 2010. Type inference in context. In Proceedings of the third ACM SIGPLAN workshop on Mathematically structured functional programming (MSFP ’10). Association for Computing Machinery, New York, NY, USA, 43–54. DOI:https://doi.org/10.1145/1863597.1863608
05 Feb 2020	Philip Wadler. 2003. Call-by-value is dual to call-by-name. In Proceedings of the eighth ACM SIGPLAN international conference on Functional programming (ICFP '03). ACM, New York, NY, USA, 189-201. DOI=http://dx.doi.org/10.1145/944705.944723
29 Jan 2020	Hutton, G. and Wright, J. (2007) What is the meaning of these constant interruptions?, Journal of Functional Programming. Cambridge University Press, 17(6), pp. 777–792. https://doi.org/10.1017/S0956796807006363	Craig
24 Jan 2020	Herbelin H. (2005) On the Degeneracy of Σ-Types in Presence of Computational Classical Logic. Urzyczyn P. (eds) Typed Lambda Calculi and Applications. TLCA 2005. Lecture Notes in Computer Science, vol 3461. Springer, Berlin, Heidelberg	Zoltan
15 Jan 2020	Emina Torlak and Rastislav Bodik. 2014. A lightweight symbolic virtual machine for solver-aided host languages. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '14). ACM, New York, NY, USA, 530-541. DOI: https://doi.org/10.1145/2594291.2594340
18 Dec 2019	Craig McLaughlin, James McKinna, and Ian Stark. 2018. Triangulating context lemmas. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018). ACM, New York, NY, USA, 102-114. DOI:https://doi.org/10.1145/3167081	Craig
04 Dec 2019	Kumar, R., Arthan, R., Myreen, M.O. et al. (2016). Self-Formalisation of Higher-Order Logic: Semantics, Soundness, and a Verified Implementation. J Autom Reasoning (2016) 56: 221. https://doi.org/10.1007/s10817-015-9357-x
27 Nov 2019	K. Wang, Y. Lin, S. M. Blackburn, M. Norrish, and A. L. Hosking. Draining the Swamp: Micro Virtual Machines as Solid Foundation for Language Development. In T. Ball, R. Bodík, S. Krishnamurthi, B. S. Lerner, and G. Morrisett, editors, Inaugural Summit on Advances in Programming Languages, SNAPL, pages 321–336, Asilomar, California, May 2015. DOI=https://dx.doi.org/10.4230/LIPIcs.SNAPL.2015.321
20 Nov 2019	Hupel L., Nipkow T. (2018) A Verified Compiler from Isabelle/HOL to CakeML. In: Ahmed A. (eds) Programming Languages and Systems. ESOP 2018. Lecture Notes in Computer Science, vol 10801. Springer, Cham. DOI=https://doi.org/10.1007/978-3-319-89884-1_35
13 Nov 2019	David Gries, Fred B. Schneider. (1995). Equational propositional logic. Information Processing Letters, Volume 53, Issue 3, 1995. Pages 145‒152. DOI=https://doi.org/10.1016/0020-0190(94)00198-8
06 Nov 2019	No reading group
30 Oct 2019	Chapman P., McKinna J., Urban C. (2008) Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle. In: Autexier S., Campbell J., Rubio J., Sorge V., Suzuki M., Wiedijk F. (eds) Intelligent Computer Mathematics. CICM 2008. Lecture Notes in Computer Science, vol 5144. Springer, Berlin, Heidelberg
16 Oct 2019	N. Koh, et. al. (2019). From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP).
09 Oct 2019	Guillaume Boisseau and Jeremy Gibbons. 2018. What you needa know about Yoneda: profunctor optics and the Yoneda lemma (functional pearl). Proc. ACM Program. Lang. 2, ICFP, Article 84 (July 2018), 27 pages. DOI:https://doi.org/10.1145/3236779
25 Sep 2019, 02 Oct 2019	Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, and Adam Chlipala. 2019. Narcissus: correct-by-construction derivation of decoders and encoders from binary formats. Proc. ACM Program. Lang. 3, ICFP, Article 82 (July 2019), 29 pages. DOI:https://doi.org/10.1145/3341686
18 Sep 2019	Philip Wadler. 2003. Call-by-value is dual to call-by-name. In Proceedings of the eighth ACM SIGPLAN international conference on Functional programming (ICFP '03). ACM, New York, NY, USA, 189-201. DOI=http://dx.doi.org/10.1145/944705.944723
11 Sep 2019	Artem Alimarine, Sjaak Smetsers, Arjen van Weelden, Marko van Eekelen, and Rinus Plasmeijer. 2005. There and back again: arrows for invertible programming. In Proceedings of the 2005 ACM SIGPLAN workshop on Haskell (Haskell '05). ACM, New York, NY, USA, 86-97. DOI=http://dx.doi.org/10.1145/1088348.1088357
03 Sep 2019	Levy P.B. (1999) Call-by-Push-Value: A Subsuming Paradigm. In: Girard JY. (eds) Typed Lambda Calculi and Applications. TLCA 1999. Lecture Notes in Computer Science, vol 1581. Springer, Berlin, Heidelberg. DOI=https://doi.org/10.1007/3-540-48959-2_17
28 Aug 2019	Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones. 2019. Making a faster Curry with extensional types. In Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell (Haskell 2019). ACM, New York, NY, USA, 58-70. DOI:https://doi.org/10.1145/3331545.3342594
21 Aug 2019	Daniel Patterson and Amal Ahmed. 2019. The next 700 compiler correctness theorems (functional pearl). Proc. ACM Program. Lang. 3, ICFP, Article 85 (July 2019), 29 pages. DOI: https://doi.org/10.1145/3341689
14 Aug 2019	Maximilian Algehed and Jean-Philippe Bernardy. 2019. Simple noninterference from parametricity. Proc. ACM Program. Lang. 3, ICFP, Article 89 (July 2019), 22 pages. DOI:https://doi.org/10.1145/3341693
07 Aug 2019	Lovas W., Pfenning F. (2009) Refinement Types as Proof Irrelevance. In: Curien PL. (eds) Typed Lambda Calculi and Applications. TLCA 2009. Lecture Notes in Computer Science, vol 5608. Springer, Berlin, Heidelberg. DOI=https://doi.org/10.1007/978-3-642-02273-9_13
31 Jul 2019	pages 1–26 of van Dalen, D. (preprint). Intuitionistic Logic. The Blackwell Guide to Philosophical Logic, L. Goble (Ed.). (obtained from author's site)
24 Jul 2019	Neil Tennant. 1994. Intuitionistic mathematics does not need ex falso quodlibet. Topoi, Vol. 13, No. 2. pp.127–133. DOI=https://doi.org/10.1007/BF00763511
17 Jul 2019	Andres Löh, Conor McBride, Wouter Swierstra. 2010. A Tutorial Implementation of a Dependently Typed Lambda Calculus. Fundam. Inform. 102(2). pp. 177–207. DOI=http://dx.doi.org/10.3233/FI-2010-304
10 Jul 2019	Jay Earley. 1970. An efficient context-free parsing algorithm. Commun. ACM 13, 2 (February 1970), 94–102. DOI=http://dx.doi.org/10.1145/362007.362035
03 Jul 2019	Conor McBride. 2010. Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation. In Proceedings of the 6th ACM SIGPLAN workshop on Generic programming (WGP '10). ACM, New York, NY, USA, 1–12. DOI:https://doi.org/10.1145/1863495.1863497	Liam
26 Jun 2019	Barry Jay. 2019. A simpler lambda calculus. In Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2019). ACM, New York, NY, USA, 1–9. DOI:https://doi.org/10.1145/3294032.3294085
19 Jun 2019	Sections 1–3 of Vytiniotis, D. and Peyton Jones, S. and Schrijvers, T. and Sulzmann, M. (2011). OUTSIDEIN(X) Modular type inference with local assumptions. Journal of Functional Programming, 21(4–5), 333–412. doi:https://doi.org/10.1017/S0956796811000098
12 Jun 2019	P. Wadler and S. Blott. 1989. How to make ad-hoc polymorphism less ad hoc. In Proceedings of the 16th ACM SIGPLAN–SIGACT symposium on Principles of programming languages (POPL '89), CORPORATE New York, NY Association for Computing Machinery (Ed.). ACM, New York, NY, USA, 60–76. DOI:https://doi.org/10.1145/75277.75283
04 Jun 2019	Postponed due to scheduling conflicts
28 May 2019	Hoare, C. A. R.. 1972. Proof of correctness of data representations. Acta Informatica, Vol. 1, No. 4, 01 December 1972. pp. 271–281. doi=https://doi.org/10.1007/BF00289507
21 May 2019	Adjourned due to Cogent dive-in
14 May 2019	Edsger W. Dijkstra. 1975. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18, 8 (August 1975), 453–457. DOI=http://dx.doi.org/10.1145/360933.360975	Carroll
07 May 2019	C. A. R. Hoare. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 10 (October 1969), 576–580. DOI=http://dx.doi.org/10.1145/363235.363259	Zilin
30 Apr 2019	Postponed due to TS town hall meeting
23 Apr 2019	Floyd, Robert W. 1967. Assigning meanings to programs. Mathematical Aspects of Computer Science (Proceedings of a Symposium in Applied Mathematics) (ed. J. T. Schwarz), Volume 19, American Mathematical Society. pp. 19–32. doi:https://doi.org/10.1090/psapm/019
16 Apr 2019	Morris Jr., James H. 1973. Types are not sets. POPL '73 Proceedings of the 1st Annual ACM SIGACT–SIGPLAN Symposium on Principles of Programming Languages. pp. 120–124. https://doi.org/10.1145/512927.512938
09 Apr 2019	Martini, S. (2016). Several types of types in programming languages. History and Philosophy of Computing 2016. pp. 216–227. http://arxiv.org/abs/1510.03726
26 Mar 2019, 02 Apr 2019	Abate, C. et al. (2018). Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation. doi:https://doi.org/10.1109/CSF.2019.00025
19 Mar 2019	Mike Gordon. (1996). Set theory, higher order logic or both?. TPHOLs 1996: Theorem Proving in Higher Order Logics. pp. 191–201. DOI:https://doi.org/10.1007/BFb0105405
12 Mar 2019	Presentation on Wadler's Theorems for Free	Santiago
12 Feb 2019, 19 Feb 2019, 26 Feb 2019, 05 Mar 2019	Wadler, P. (1989). Theorems for free!. 4'th International Conference on Functional Programming and Computer Architecture, London, September 1989.
05 Feb 2019	Bernardy, J., et al. (2017). Linear Haskell: practical linearity in a higher–order polymorphic language. Proceedings of the ACM on Programming Languages, 2(POPL), pp.1–29. https://arxiv.org/abs/1710.09756
27 Jan 2019	Wadler, P. (1990). Linear types can change the world!. Programming Concepts and Methods, M. Broy and C. Jones, editors, North Holland, 1990.
08 Jan 2019	Myhill, J. (1973), Embedding Classical Logic in Intuitionistic Logic. Mathematical Logic Quarterly, 19. pp. 93–96. doi:https://doi.org/10.1002/malq.19730190307
18 Dec 2018	Howard, W. A. (1980). The formulae-as-types notion of construction. To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, Academic Press, pp. 479–491. Reprint, Armando B. Matos, 2017.
11 Dec 2018	Kolmogorov, A. (1932). On the Interpretation of Intuitionistic Logic. Mathematische Zeitschrift, vol. 35, pp. 58–65
04 Dec 2018	Wadler, P. (2015). Propositions as types. Communications of the ACM, 58(12): pp. 75–84. https://doi.org/10.1145/2699407
27 Nov 2018	Church, A. (1936). An Unsolvable Problem of Elementary Number Theory. American Journal of Mathematics, 58(2), pp. 345–363. https://doi.org/10.2307/2371045
20 Nov 2018	Church, A. (1940). A formulation of the simple theory of types. Journal of Symbolic Logic, Cambridge University Press, 5(2), pp. 56–68. https://doi.org/10.2307/2266170. Supplementary Reading: Cardone, F & Milner, R. (2006) History of Lambda–calculus and Combinatory Logic. (preprint)