Re: F* PoP Up Seminar by Subhajit Roy

[Nikhil Swamy]

Looking forward to seeing you all tomorrow for Subhajit Roy's talk!

Just a heads up that the meeting will be on Zoom, as usual. Please ignore the link to the Teams meeting at the bottom of the email.

-Nik

---

From: Aseem Rastogi
Sent: Tuesday, August 29, 2023 9:01 PM
To: Aseem Rastogi <ase...@microsoft.com>; fstar-mai...@googlegroups.com <fstar-mai...@googlegroups.com>
Cc: Nikhil Swamy <nsw...@microsoft.com>; abhishek...@gmail.com <abhishek...@gmail.com>; seo...@uci.edu <seo...@uci.edu>; theo.win...@gmail.com <theo.win...@gmail.com>; adharsh...@gmail.com <adharsh...@gmail.com>; Tahina Ramananandro <tara...@microsoft.com>; Guido Martinez <guima...@microsoft.com>; Gowtham Kaki <Gowtha...@colorado.edu>; catalin...@gmail.com <catalin...@gmail.com>
Subject: F* PoP Up Seminar by Subhajit Roy
When: Tuesday, September 19, 2023 8:30 AM-9:30 AM.
Where: Microsoft Teams Meeting

 

On 19^th September, 8:30am PDT, we will have our next F* PoP Up Seminar where Prof. Subhajit Roy from IIT Kanpur will tell us about his experience of using F* to teach PL semantics.

Zoom link: https://cmu.zoom.us/j/97804414550?pwd=Q3NQWjRxNWwwYnVLSDVSMllmb01jQT09

Hope to see you there,

-Aseem.

Speaker: Prof. Subhajit Roy, IIT Kanpur

Title: The Lazy Professor's Route to Teaching Programming Language Semantics a.k.a. A Theorem Proving Approach to PL Semantics

Abstract:

The talk will unfold the story of a lazy professor who felt that using theorem provers is an "easy" shortcut to messy proofs while teaching programming languages theory. We will discuss his experience of using this methodology (and the story of distressed students) in an ACM summer school on programming languages. Once the program and its semantics are encoded in any of the different styles—operational, denotational, or axiomatic, powerful proof assistants like F* can prove exciting language features with minimal human assistance. The hope is that teaching programming languages via proof assistants will not only provide a more concrete understanding of this topic but also prepare future programming language researchers to use theorem provers as fundamental tools in their research and not as an afterthought. Well, although the methodology was born out of the professor's attempt at saving face after a heavy dose of procrastination, it opens up interesting questions on if undergraduate students are ready enough to date theorem provers.

________________________________________________________________________________

Microsoft Teams meeting

Join on your computer, mobile app or room device

Click here to join the meeting

Meeting ID: 223 175 846 443
Passcode: dQV9WA

Download Teams | Join on the web

Or call in (audio only)

+1 323-849-4874,,603229037#   United States, Los Angeles

0008000401142,,,,603229037#   India (Toll-free)

Phone Conference ID: 603 229 037#

Find a local number | Reset PIN

Learn More | Meeting options

________________________________________________________________________________

--
You received this message because you are subscribed to the Google Groups "fstar-mailing-list" group.
To unsubscribe from this group and stop receiving emails from it, send an email to fstar-mailing-l...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/fstar-mailing-list/KL1P15301MB0404C3F44EBAF189B11F2DD2CCE6A%40KL1P15301MB0404.APCP153.PROD.OUTLOOK.COM.
For more options, visit https://groups.google.com/d/optout.