Reading Group

Mojtaba, Amir, Hsi-Ming, Ian Mackie, Martin, and guests meet up regularly (for now, online over Zoom) to read and discuss papers of interest for our research. We mostly read papers in the general area of programming languages, compilers, typing systems, logic and verification. We look at classic papers as well as recent work. From time to time we also read papers of general interest from other parts of science. The next papers we read are:

• Mojtaba will present our work on regular expression synthesis. (Mojtaba, Friday 17 March, 18:00-19:00)
• S. Gulwani, S. Jha, A. Tiwari, R. Venkatesan, Synthesis of loop-free programs. (Luke, TBC)
• J. Cambronero, J. Gulwani, V. Le, D. Perelman, A. Radhakrishna, C. Simon, A. Tiwari, FlashFill++: Scaling Programming by Example by Cutting to the Chase. (Martin and/or Mojtaba, details TBC)
• Gentle introduction to formal power series, based on N. Chomsky and M. P. Schützenberger's pioneering 1963 work The Algebraic Theory of Context-Free Languages. (Martin, date/time TBC)
• Gentle introduction to GPUs and GPU-programming with CUDA. (Mojtaba, date/time TBC)

Please take a look at the paper beforehand, even if you are not the speaker. Here are some guiding questions that might help you structure your thoughs and reading: What is the key idea in the paper, what is the key novelty? Can you summarise the paper in a few sentences? What do you understand, what is unclear? Where do you get stuck? How does the paper relate to your research? What were the 3 most important things you have learned from this paper? Can you think of any improvements on the paper?

Past. It's fine to re-read papers, for example to take a deeper look at details the second time.

• J. Lee, D. Kim, C.-K. Hur, N. P. Lopes, An SMT Encoding of LLVM's Memory Model for Bounded Translation Validation (Carl Friedrich Bolz-Tereick, Thursday 23 February, 1800 - 1900)
• R. Sasnauskas, Y. Chen, P. Collingbourne, J. Ketema, G. Lup, J. Taneja, J. Regehr, A Synthesizing Superoptimizer (Luke, Thursday, 15 Dec, 18:00 - 19:00))
• A. Fawzi, M. Balog, A. Huang, T. Hubert, B. Romera-Paredes, M. Barekatain, A. Novikov, F. J. R. Ruiz, J. Schrittwieser, G. Swirszcz, D. Silver, D. Hassabis, P. Kohli, Discovering faster matrix multiplication algorithms with reinforcement learning. (Hsi-Ming, Thurs 27th October, 15:00 - 16:00.)
• Gentle introduction to Memory Dependence prediction (aka Load-To-Store prediction), with emphasis on the stores-sets algorithm from: G. Z. Chrysos, J. S. Emer, Memory Dependence Prediction using Store Sets (Luke Panayi, Friday 5 August, 15:00 - 16:00)
• K. Loughlin, S. Saroiu, A. Wolman, Y. A. Manerkar, B. Kasikci, MOESI-prime: Preventing Coherence-Induced Hammering in Commodity Workloads. (Amir, Wednesday 3 August, 17:00-18:00)
• Gentle introduction to active (automata) learning. (Amir, 1 July, 17:00 - 18:00)
• Y. Tobah, A. Kwong, I. Kang, D. Genkin, K. G. Shin, SpecHammer: Combining Spectre and Rowhammer for New Speculative Attacka. (Amir, Friday 18 Feb 2022, 17:00-18:00)
• M. Lee, S. So, H. Oh, Synthesizing Regular Expressions from Examples for Introductory Automata Assignments. (Mojtaba, Friday 11 Feb 2022, 17:00-18:00)
• Mojtaba will introduce his novel algorithm for the synthesis of regular expressions. (Wednesday 15. Dec, 17:00 - 18:00)
• P. Jattke, V. van der Veen, P. Frigo, S. Gunter, K. Razavi, BLACKSMITH: Scalable Rowhammering in the Frequency Domain. (Amir, Friday 3. Dec, 17:00 - 18:00)
• D. Hedin, A. Sabelfeld, A Perspective on Information-Flow Control (Amir, Friday 29 October, 17:00 - 18:00)
• C. Hahn, F. Schmitt, J. U. Kreber, M. N. Rabe, B. Finkbeiner, Teaching Temporal Logics to Neural Networks (Hsi-Ming, Friday 15 Oct, 17:00-18:00)
• R. N. M. Watson, S. W. Moore, P. Sewell, P. G. Neumann, An Introduction to CHERI. (Martin, 24 Sept, time: 17:00 - 18:00)
• Gentle introdution to SMT-solving with Z3. (Mojtaba, Friday 17 Sept 2021, 17:00 - 18:00)
• A. G. Yağlıkçı, M. Patel, J. S. Kim, R. Azizi, A. Olgun, L. Orosa, H. Hassan, J. Park, K. Kanellopoulos, T. Shahroodi, S. Ghose, O. Mutlu, BlockHammer: Preventing RowHammer at Low Cost by Blacklisting Rapidly-Accessed DRAM Rows. (Amir, 9 Sept 2021, 15:00 - 16:00)
• J. Hughes, D. Marshall, J. Wood, D. Orchard, Linear Exponentials as Graded Modal Types (Jack Hughes, Friday 23 July, 17:00)
• POPL, PLDI etc 2021 lightning session. We'll looked at the following papers (each paper just 2-3 minutes).
  • M. Gaboardi, S.-Y. Katsumata, D. Orchard, T. Sato, Graded Hoare Logic and its Categorical Semantics. (Pancho)
  • P. Pistone, On Generalized Metric Spaces for the Simply Typed Lambda-Calculus. (Pancho)
  • R. Beutner, L. . Ong, On Probabilistic Termination of Functional Programs with Continuous Distributions. (Amir)
  • J. Wang, Y. Sun, H. Fu, K. Chatterjee, A. Kafshdar Goharshady, Quantitative Analysis of Assertion Violations in Probabilistic Programs. (Amir)
  • F. A. Saad, M. C. Rinard, V. K. Mansinghka, SPPL: Probabilistic Programming with Fast Exact Symbolic Inference. (Amir)
  • J. Rosemann, S. Moll, S. Hack, An Abstract Interpretation for SPMD Divergence on Reducible Control Flow Graphs. (Martin)
  • J. O. Gutsfeld, M. Mueller-Olm, C. Ohrem, Automata and Fixpoints for Asynchronous Hyperproperties. (Martin)
  • A. Barriere, S. Blazy, O. Flueckiger, D. Pichardie, J. Vitek, Formally Verified Speculation and Deoptimization in a JIT Compiler. (Martin)
  • Y. M. Y. Feldman, M. Sagiv, S. Shoham, J. R. Wilcox, Learning the Boundary of Inductive Invariants. (Martin)
  • C. Stanford, M. Veanes, N. Bjoerner, Symbolic Boolean Derivatives: for Efficiently Solving Extended Regular Expression Constraints. (Mojtaba)
  • J R. Koenig, O. Padon, A. Aiken, Adaptive Restarts for Stochastic Synthesis. (Mojtaba)
  We meet Friday 11 June, 17:00-18:0 0
• Introduction to Rust and its ecosystem. (Amir, 21 Mai, 18:00 - 19:00)
• M. Alvarez Picallo, A. Eyers-Taylor, M. Peyton Jones, C.-H. L. Ong, Fixing incremental computation: Derivatives of fixpoints, and the recursive semantics of Datalog. (Speaker: Martin, Friday 7 May, 17:00-18:00)
• Y. Cai, P. G. Giarrusso, T. Rendel, K. Ostermann, A Theory of Changes for Higher-Order Languages: Incrementalizing λ-Calculi by Static Differentiation. (Speaker: Mario Alvarez Picallo, Friday 16 April, time 17:00-18:00)
• M. Guarnieri, B. Köpf, J. F. Morales, J. Reineke, A. Sanchez, Spectector: Principled Detection of Speculative Information Flow (Amir, Thurs 4 March, 18:00 - 19:00)
• S. Bansal, A. Aiken, Automatic Generation of Peephole Superoptimizers (Mojtaba, 10 February, 17:00-18:00)
• A. Armstrong, T. Bauereiss, B. Campbell, A. Reid, K. E. Gray, R. M. Norton, P. Mundkur, M. Wassell, J. French, C. Pulte, S. Flur, I. Stark, N. Krishnaswami, P. Sewell, ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS (Martin, 20 November, 18:00-19:00))
• C. Canella, J. Van Bulck, M. Schwarz, M. Lipp, B. von Berg, P. Ortner, F. Piessens, D. Evtyushkin, D. Gruss, A Systematic Evaluation of Transient Execution Attacks and Defenses. (Amir, 13 November, 18:00 - 19:00)
• J. K. Feser, S. Chaudhuri, I. Dillig, Synthesizing Data Structure Transformations from Input-Output Examples. (Mojtaba, 6 Nov, 18:00 - 19:00)
• L. Simon, Implementation of CDCL SAT solvers. (Mojtaba, Friday 9 October, 18:00 - 19:00, over Zoom)
• J. Hughes, D. Orchard, Resourceful Program Synthesis from Graded Linear Types. (Jack, Friday 2 Oct, 17:00 - 18:00)
• P. Frigo, E. Vannacci, H. Hassan, V. van der Veen, O. Mutlu, C. Giuffrida, H. Bos, K. Razavi, TRRespass: Exploiting the Many Sides of Target Row Refresh. (Amir, Wednesday, 23 Sep 2020, 17:00 - 18:00)
• P. Blackburn, M. Tzakova, Hybrid Languages and Temporal Logic. (Pancho, Wednesday 16 Sept, 16:00)
• A. Kwong, D. Genkin, D. Gruss, Y. Yarom, RAMBleed: Reading Bits in Memory Without Accessing Them. (Amir, Friday 26 June, 17:00, email me for a Zoom invite)
• V. Mnih, K. Kavukcuoglu, D. Silver, A. Graves, I. Antonoglou, D. Wierstra, M. Riedmiller, Playing Atari with Deep Reinforcement Learning. (Rafael, 27 May, 18:00 over Zoom, email me for a Zoom invite)
• S. Vig, S. Bhattacharya, D. Mukhopadhyay, S. Lam, Rapid Detection of RowHammer Attacks using Dynamic Skewed Hash Tree. (Amir, Wed 20 May 2020 at 17:30-18:30 over Zoom, email me for a Zoom invite)
• Mohammad Nourian will give a gentle introduction to the Longest common subsequence problem (LCS). (Wednesday 6 May, 17:15 - 18:15.)
• J. L. Hennessy, D. A. Patterson, A New Golden Age for Computer Architecture. (Martin, 22 April, 16:00 - 17:00 over Zoom, email me for a Zoom invite)
• Mojtaba will introduce Bayesian Inference and application in variational autoencoders. (Date and time: Wed 1 April, 17:00 - 18:00 over Zoom (Meeting ID: 186 911 683, Password: 855079)
• D. Gruss, C. Maurice, S. Mangard, Rowhammer.js: A Remote Software-Induced Fault Attack in JavaScript. (Amir, online over Zoom, Wednesday 25 March, 16:15 - 17:15)
• C. Smith, A. Albarghouthi, Synthesizing differentially private programs. (Jack Hughes, 11 March, 15:00 - 16:00, in Chichester 3, Room 3R241)
• V. Klimis, B. Reus, G. Parisis, Towards Model Checking Real-World Software-Defined Networks. (Vasilis, 26 Feb, 15:00 - 16:00)
• Chapters 38 & 39 ("The Single Neuron as a Classifier") of MacKay's Information Theory, Inference, and Learning Algorithms. (Mojtaba, 19 Feb, 15:00 - 16:00).
• Z. Zhang, Y. Cheng, D. Liu, S. Nepal, Z. Wang, TeleHammer: Cross-Privilege-Boundary Rowhammer through Implicit Accesses. (Amir, 12 Feb, 15:00 - 16:00).
• Introduction session: Pancho and Amir ELI5 their respective PhD research to Mojtaba:
  • Rowhammer and information flow.
  • Program logics for fresh name generation.
• Codereview of Amir's current Rowhammer work..
• B. Powers, D. Tench, E. D. Berger, A. McGregor, Mesh: Compacting Memory Management for C/C++ Applications
• P. W. O'Hearn, Incorrectness Logic
• A. Sabelfeld, A. C. Myers, Language-Based Information-Flow Security
• S. Hunt, D. Sands, On Flow-Sensitive Security Types
• D. Walker, Objects in the Pi-calculus.
• ECOOP'19 and PLDI'19 lightning session. We'll looked at the following papers.
  • K. Fernandez-Reyes, E. Broch Johnsen, D. Clarke, L. Henrio, T. Wrigstad, Godot: All the Benefits of Implicit and Explicit (Alex)
  • C. Watt et al A Program Logic for First-Order Encapsulated WebAssembly.
  • B Churchill et al, Semantic Program Alignment for Equivalence Checking.
  • T Chanh Le et al, SLING: Using Dynamic Analysis to Infer Program Invariants in Separation Logic.
  • K. Liao, M. Hammer, A. Mille, ILC: A Calculus for Composable, Computational Cryptography.
  • W. T. Hallahan, A. Xue, M. T. Bland, R. Jhala, R. Piska, Lazy Counterfactual Symbolic Execution.
  • T. Sotiropoulos, B. Livshit, Static Analysis for Asynchronous JavaScript Programs.
• A. Arslanagic, J. A. Perez, E. Voogd, Minimal Session Types.
• B. C. Pierce, Recursive types, Chapters 20 & 21 of TAPL.
• ESOP 2019 lightning session. We looked at the following papers.
  • S. Buro, I. Mastroeni, On the Multi-Language Construction.
  • S. Balzer, B. Toninho, F. Pfenning, Manifest Deadlock-Freedom for Shared Session Types.
  • L. Bocchi, V. Murgia, V. T. Vasconcelos, N. Yoshida, Asynchronous Timed Session Types: From Duality to Time-Sensitive Processes.
  • R. van Glabbeek, P. Höfner, M. Markl, A Process Algebra for Link Layer Protocols.
  • G. Martínez et al, Meta-F^*: Proof Automation with SMT, Tactics, and Metaprograms On the Multi-Language Construction
  • F. Besson, S. Blazy, A. Dang, T. Jensen, P. Wilke, Compiling Sandboxes: Formally Verified Software Fault Isolation
  • F. Vesely, K. Fisher, One Step at a Time: A Functional Derivation of Small-Step Evaluators from Big-Step Counterparts.
  • M. Patrignani, D. Garg, Robustly Safe Compilation.
• B. C. d. S. Oliveira, A. Moors, M. Odersky, Type Classes as Objects and Implicits.
• J. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures.
• R. Alur, D. Dill, Automata for modeling real-time systems.
• P. Wadler, Monads for functional programming.
• Trace semantics and control-flow graphs, a gentle yet formal introduction.
• POPL 2019 (and CCS'18) lightning session. We looked at the following papers.
  • P. Cousot, R. Giacobazzi, F. Ranzato, A²I: Abstract² Interpretation.
  • U. Dal Lago, M. De Visme, D. Mazza, A. Yoshimizu, Intersection Types and Runtime Errors in the Pi-Calculus.
  • D. Castro, R. Hu, S.-S. Jongmans, N. Ng, N. Yoshida, Distributed Programming using Role-Parametric Session Types in Go.
  • Y. Miyazaki, T. Sekiyama, A. Igarashi, Dynamic Type Inference for Gradual Hindley–Milner Typing.
  • J. Van Bulck, F. Piessens, R. Strackx, Nemesis: Studying Microarchitectural Timing Leaks in Rudimentary CPU Interrupt Logic. (
  • K. Memarian, V. B. F. Gomes, B. Davis, S. Kell, A. Richardson, R. N. M. Watson, P. Sewell, Exploring C Semantics and Pointer Provenance.
  • T. Sato, A. Aguirre, G. Barthe, M. Gaboardi, D. Garg, J. Hsu, Formal Verification of Higher-Order Probabilistic Programs.
  • D. Unruh, Quantum Relational Hoare Logic.
  • C. Watt, J. Renner, N. Popescu, S. Cauligi, D. Stefan, CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem.
  • M. Vassena, A. Russo, D. Garg, V. Rajani, D. Stefan, From Fine- to Coarse-Grained Dynamic Information Flow Control and Back.
  • G. Park, J. Hong, G. L. Steele Jr., S. Ryu, Polymorphic Symmetric Multiple Dispatch with Variance.
  • D. Wang, J. Hoffmann, Type-Guided Worst-Case Input Generation.
• Z. DeVito, J. Hegarty, A. Aiken, P. Hanrahan, J. Vitek, Terra: A Multi-Stage Language for High-Performance Computing.
• N. Amin, T. Rompf, M. Odersky, Foundations of Path-Dependent Types.
• L. Damas, R. Milner, Principal type-schemes for functional programs.
• E. M. Clarke, E. A. Emerson, Design and synthesis of synchronization skeletons using branching time temporal logic.
• A. Naseredini, Introduction to penetration testing.
• M. Sipser, Chapters 1, 2, 3 of Introduction to the Theory of Computation on the Chomsky hierarchy of languages.
• S. Lösch, A. M. Pitts, Relating Two Semantics of Locally Scoped Names.
• D. Dolev, A. Yao, On the security of public-key protocols.
• A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, Y. Zhu, Bounded Model Checking.
• N. Amin, K. Gruetter, M. Odersky, T. Rompf, S. Stucki, The Essence of Dependent Object Types.
• E. Schkufza, R. Sharma, A. Aiken, Stochastic Program Optimization.
• R. Demangeon, N. Yoshida, Causal Computational Complexity of Distributed Processes.
• A. Pitts, Nominal logic, a first order theory of names and binding.
• R. Milner, Functions as Processes.
• Post S-REPLS 9 Session.
  • R. Neykova, R. Hu, N. Yoshida, F. Abdeljallal, Session Type Providers: Compile-time API Generation for Distributed Protocols with Interaction Refinements in F#.
  • D. R. Ghica, K.Muroya, T. Waugh Ambridge A Graph-Rewriting Perspective of the Beta-Law.
• I.-S. Kim, K. Yi, C. Calcagno, A Polymorphic Modal Type System for Lisp-like Multi-Staged Languages.
• C. Click, J. Rose, Fast subtype checking in the HotSpot JVM.
• M. Coppo, M. Dezani-Ciancaglini, L. Padovani, N. Yoshida, Gentle Introduction to Multiparty Asynchronous Session Types.
• G. Munch-Maccagnoni, Resource Polymorphism.
• A. Jeffery, M. Berger, Asynchronous Sessions with Implicit Functions and Messages.
• L. Parreaux, A. Voizard, A. Shaikhha, C. E. Koch, Unifying Analytic and Statically-Typed Quasiquotes.
• T. Kraska, A. Beutel, E. H. Chi, J. Dean, N. Polyzotis, The Case for Learned Index Structures.
• J.-P. Bernardy, M. Boespflug, R. N. Newton, S. Peyton Jones, A. Spiwack, Linear Haskell: practical linearity in a higher-order polymorphic language.
• POPL 2018 lightning session. We looked at the following papers.
  • J.-P. Bernardy, M. Boespflug, R. N. Newton, S. Peyton Jones, A. Spiwack, Linear Haskell: practical linearity in a higher-order polymorphic language.
  • R. Jung, J.-H. Jourdan, R. Krebbers, D. Dreyer, RustBelt: Securing the Foundations of the Rust Programming Language.
  • N. Amin, T. Rompf, Collapsing Towers of Interpreters.
  • H.-S. Ko, Z. Hu, An Axiomatic Basis for Bidirectional Programming.
  • K. Chandra, R. Bodik, Bonsai: Synthesis-Based Reasoning for Type Systems.
  • X. Wand, I. Dillig, R. Singh, Program Synthesis using Abstraction Refinement.
  • O. Fluckiger, G. Scherer, M.-H. Yee, A. Goel, A. Ahmed, J. Vitek, Correctness of Speculative Optimizations with Dynamic Deoptimization.
• K. Honda, N. Yoshida. A compositional logic for polymorphic higher-order functions..
• P. Wadler, Propositions as types.
• B. C. Pierce, Recursive types, Chapters 20 & 21 of TAPL.
• R. Davies, A Temporal-Logic Approach to Binding-Time Analysis.
• P. Eliott, Gentle introduction to modal logic.
• E. Barrett, C. F. Bolz, R. Killick, V. Knight, S. Mount, L. Tratt, Virtual Machine Warmup Blows Hot and Cold.
• J. K. Feser, S. Chaudhuri, I. Dillig, Synthesizing Data Structure Transformations from Input-Output Examples.
• B. C. Pierce, D. N. Turner, Local Type Inference.
• T. Sheard, S. Peyton Jones, Template Meta-programming for Haskell.
• B. C. Pierce, Type soundness proofs, Chapters 8 & 9 of TAPL.
• M. Berger, L. Tratt, C. Urban, Modelling homogeneous generative meta-programming.
• B. C. Pierce, Type Operators and Kinding, Chapters 29 & 30 of TAPL.
• M. Odersky, A. Biboudis, F. Liu, O. Blanvillain, Foundations of Implicit Function Types.
• P. Wadler S. Blott, How to make ad-hoc polymorphism less ad hoc.
• L. Damas, R. Milner, Principal type-schemes for functional programs.
• S. Gay, V. T. Vasconcelos, Linear type theory for asynchronous session types.
• A. Haas, A. Rossberg, D. L. Schuff, B. L. Titzer, M. Holman, D. Gohman, L. Wagner, A. Zakai, J.-F. Bastien, Bringing the Web up to Speed with WebAssembly.
• S.-Y. Guo, J. Palsberg, The Essence of Compiling with Traces.
• V. Bala, E. Duesterwald, S. Banerji, Dynamo: A Transparent Dynamic Optimization System.
• M. Bebenita, F. Brandner, M. Fahndrich, F. Logozzo, W. Schulte, N. Tillmann, H. Venter, SPUR: A Trace-Based JIT Compiler for CIL.
• T. Kotzmann, C. Wimmer, H. Mossenböck, T. Rodriguez, K. Russell, D. Cox, Design of the Java HotSpot Client Compiler for Java 6.
• U. Hölzle, C. Chambers, D. Ungar, Optimizing Dynamically-Typed Object-Oriented Languages With Polymorphic Inline Caches.
• C. Chambers, D. Ungar, E. Lee, An efficient implementation of SELF: a dynamically-typed object-oriented language based on prototypes.
• L. P. Deutsch, A. M. Schiffman, Efficient Implementation of the Smalltalk-80 System.