Reading Group

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:

- B. C. Pierce, Recursive types, Chapters 20 & 21 of TAPL. (Amir, Wednesday 22 May, 14:00 - 15:00)

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.

- Alex and/or Martin will present a paper on graded modal typing systems, 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.

- 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*.

- S. Buro, I. Mastroeni,
- 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*.

- P. Cousot, R. Giacobazzi, F. Ranzato,
- 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*.

- R. Neykova, R. Hu, N. Yoshida,
F. Abdeljallal,
- 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*.

- J.-P. Bernardy, M. Boespflug, R. N. Newton, S. Peyton
Jones, A. Spiwack,
- 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*.