Reading Group
Mojtaba, Pancho, Alex, Amir, Martin and Vasilis meet up
regularly (in person or by telecommuting) to read 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:
- Introduction to Shannon's information theory (Amir, 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?
Future. We will be reading the following
papers. If you are interested in introducing one of them -- or if you
want to propose other papers to read -- please let us know.
- M. Abadi, B. Blanchet, C. Fournet,
The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication: Updated 2016 version. (Amir, details TBC)
- Monte Carlo tree search (Martin, details TBC)
- K. Claessen, N. Smallbone, J. Hughes, Guessing Formal Specifications using Testing (Martin / Pancho, details TBC)
- C. Elliott,
The simple essence of automatic differentiation. (Martin, date TBC)
Past. It's fine to re-read papers, for example
to take a deeper look at details the second time.
- 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 (Pancho)
- B Churchill et al, Semantic Program Alignment for Equivalence Checking (Pancho)
- T Chanh Le et al, SLING: Using Dynamic Analysis to Infer Program Invariants in Separation Logic (Pancho)
- K. Liao, M. Hammer, A. Mille, ILC: A Calculus for Composable, Computational Cryptography (Amir)
- W. T. Hallahan, A. Xue, M. T. Bland, R. Jhala, R. Piska, Lazy Counterfactual Symbolic Execution (Amir)
- T. Sotiropoulos, B. Livshit, Static Analysis for Asynchronous JavaScript Programs (Amir)
- 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. Elliot, 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.