The below are potential topics to choose from. Each topic is associated with one, two, or three papers. For the discussion in a week for which a topic is scheduled, students are supposed to have read all the papers associated with the topic. The student presenting should have read some additional related work in order to give a well-rounded presentation.

Topic Paper 1 Paper 2 Paper 3
Code Surveys A large scale study of programming languages and code quality in github On the Impact of Programming Languages on Code Quality: A Reproduction Study  
Concurrency Separation logic: a logic for shared mutable data structures Balancing expressiveness in formal approaches to concurrency  
Dynamic OO language implementation An efficient implementation of SELF, a dynamically-typed object-oriented language based on prototypes Improving JavaScript performance by deconstructing the type system  
Expressive Power On the Expressive Power of Programming Languages    
Functional Languages Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I A Metalanguage for interactive proof in LCF  
Gradual Typing Gradual Typing for Functional Languages Is Sound Gradual Typing Dead?  
Java Soundness Featherweight Java: A Minimal Core Calculus for Java and GJ Java and scala’s type systems are unsound: the existential crisis of null pointers Featherweight Java (Journal Version for additional info)
Object-Oriented Programming On Understanding Data Abstraction, Revisited The Power of Interoperability: Why Objects are Inevitable  
Parametricity Types, Abstraction and Parametric Polymorphism Theorems for Free!  
Performance Measurement Producing wrong data without doing anything obviously wrong! Rethinking Java Performance Analysis  
Progress & Preservation A Syntactic Approach to Type Soundness    
Security Recognizing safety and liveness Enforceable Security Policies  
SMT Solvers/Verifiers Simplification by Cooperating Decision Procedures Z3: An Efficient SMT Solver Dafny: An Automatic Program Verifier for Functional Correctness
Type Inference A theory of type polymorphism in programming The Principal Type-Scheme of an Object in Combinatory Logic  
Verified Compilation From System F to Typed Assembly Language    
Verified Compilers Formal verification of a realistic compiler CakeML: A Verified Implementation of ML  
bars search times