Title: Proof-oriented Programming in F*

Speaker: Aseem Rastogi    (bio) (bio)

Aseem Rastogi is a Principal Researcher at Microsoft Research India. His work spans the areas of language design, type systems, program verification, and software security. More specifically, his interest lies in developing formal techniques for writing provably correct and secure software. He is one of the core designers and developers of F*, a language for program verification.

When: Tuesday, 10 May 2022 at 1900 hrs (IST)

Abstract:
F* is a proof-oriented programming language that has been used to develop, and deploy, critical software components backed with mathematical proofs of correctness and security. Deployments of programs written and proven in F* include Microsoft Windows Hyper-V, Microsoft Azure, Firefox, Linux, mbedTLS, and several other production systems. In this talk, I will begin with an overview of F* and its applications. I will then talk about our recent work on Steel, a language for programming and proving concurrent programs embedded in F*. Steel is based on a higher-order Concurrent Separation Logic, also derived in F* using a denotation of computations in the effectful semantics of non-deterministically interleaved atomic actions. With Steel we have programmed several verified programs and libraries, including spinlocks, protocol-indexed channel, and various sequential and concurrent data-structures.