Mathematics and Programming: The Past, Present and Future A Personal Perspective

Speaker: Dr. Pritam Choudhury

Abstract: In his article „Constructive Mathematics and Computer Programming‟, the renowned logician and type-theorist, Per Martin-Löf notes, “If programming is understood not as the writing of instructions for this or that computing machine but as the design of methods of computation that it is the computer‟s duty to execute (a difference that Dijkstra has referred to as the difference between computer science and computing science), then it no longer seems possible to distinguish the discipline of programming from constructive mathematics.”
Indeed, mathematics (constructive) and programming can be viewed as two sides of the same coin via the celebrated Curry-Howard or Propositions-as-Types Correspondence. This correspondence has been of great value to both mathematics and programming. On one side, it enabled mechanization of mathematics and consequently, production of machine-certified proofs of mathematical theorems. On the other side, it provided a solid mathematical foundation for programming languages and guided their development.
In this talk, I shall first introduce the Curry-Howard Correspondence through examples and then present some of its technical details. We shall start with a key result, which states that the Simply-Typed λ-calculus, a foundational functional programming language, is nothing but intuitionistic/constructive propositional logic. Thereafter, I shall touch upon multiple other similar correspondences, all manifestations of the overarching Curry-Howard Correspondence, and discuss how these correspondences guided the development of programming languages. Then, I shall present some of my research work on extending the Curry-Howard Correspondence in the area of dependency analysis over the Simply-Typed λ- calculus (https://dl.acm.org/doi/10.1145/3563335). Note that dependency analysis is vital to several applications, such as, language-based security, multi-stage compilation, code optimization, etc. Finally, I shall wind up the talk discussing some of my ongoing and future research projects that leverage the close connection between mathematics and programming for their mutual benefit.

Bio: Pritam Choudhury is a researcher in type systems and programming language design. His research focuses on graded type systems and their applications. In his doctoral dissertation, he used graded type systems to analyze linearity and dependency in programming languages. Linearity and dependency analyses are particularly useful in memory management, language-based security, multi-stage compilation and code optimization. Pritam completed his PhD at University of Pennsylvania in August 2023. After graduating from UPenn, he taught as a Visiting Assistant Professor of Computer Science at Haverford College for a year. Before joining UPenn, he worked on formal verification at University of Cambridge. Pritam received his M.Phil. in Advanced Computer Science from University of Cambridge in 2015 and his B.Tech. in Electrical Engineering from IIT Roorkee in 2014.