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:
- R. N. M. Watson, S. W. Moore, P. Sewell, P. G. Neumann,
An Introduction to CHERI. (Martin, 24 Sept, time: 17:00 - 18:00)
- C. Hahn, F. Schmitt, J. U. Kreber, M. N. Rabe, B. Finkbeiner,
Teaching Temporal Logics to Neural Networks (Hsi-Ming, 8 Oct, details 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.
- 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^{2}I: Abstract^{2} 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.