Writings

These are slides based on Prof. Peter O’Hearn’s POPL'19 Paper on Incorrectness Logic, presented over two 1.5-hour lectures for the course COL731: Advanced Compiler Techniques offered by Prof. Sorav Bansal at IITD in Sem I, 2023-24.

The slides do not cover Section 5 of the paper because we decided to skip it in class. Most of the content borrows from the paper, except a few new examples, typo-fixes and reorganisation. I am deeply grateful to Prof. O’Hearn for writing a clear, accessible and interesting paper (and of course, for the content in these slides).

These slides cover the following two papers on Compositional Reasoning for Weak Memory Models:

1. Coughlin, Nicholas, Kirsten Winter, and Graeme Smith. “Compositional Reasoning for Non-Multicopy Atomic Architectures.” Formal Aspects of Computing, December 14, 2022, 3574137.

2. Coughlin, Nicholas, Kirsten Winter, and Graeme Smith. “Rely/Guarantee Reasoning for Multicopy Atomic Weak Memory Models.” In Formal Methods, edited by Marieke Huisman, Corina Păsăreanu, and Naijun Zhan, 292–310. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2021.

Mrunmayi Bhalerao and I presented these as part of the course Special Module in Concurrency : Formal Verification of Concurrent Programs (COV889) offered by Prof. Subodh Sharma at IIT Delhi, Sem II 2022-23. Most of the content in the slides borrows from the papers. We acknowledge and thank the authors for this content, and for writing these wonderful papers.

These notes were written for the course COL832: Proofs and Types, offered by Prof. S. Arun-Kumar at IITD in Sem I, 2022-23. In this lecture, we have two main goals:

1. Complete a proof of the equivalence between the class of partial recursive functions and the class of λ-definable partial numeric functions.

2. Prove the Scott-Curry Theorem (which implies undecidability of β-equality in the untyped λ-Calculus).

We start by defining the class of partial recursive functions and the notion of λ-definability and then look at two theorems proving the equivalence. Then, we define an encoding for the λ-terms to Church numerals, and use that to prove the Second Recursion Theorem. Using the Second Recursion Theorem, we prove the Scott-Curry Theorem, and end with a corollary showing the undecidability of β-equality in the λ-Calculus.

This was written as part of an Independent Study I did on Automatic Synthesis of Smart Contracts with Prof. Subodh Sharma in Sem II, 2021-22.

The article is about applications of program synthesis techniques to the field of smart contracts. We first discuss program synthesis and outline three general challenges that any program synthesis system has to solve. Then, we give a brief introduction to smart contracts, highlighting the aspects useful for their formal specification, modelling and synthesis. Next, we illustrate one important application area, namely optimisation, through discussing the paper “Synthesis of Super-Optimized Smart Contracts Using Max-SMT”. We explain how optimisation is framed as a synthesis problem, and examine how the paper deals with two important challenges in program synthesis - target specification and program space representation. We end with some directions for future work, discussing broad challenges in applying program synthesis to smart contracts.