F* PoP Up Seminar by Subhajit Roy
5 views
Skip to first unread message
Aseem Rastogi
Aug 29, 2023, 11:58:35 PM8/29/23
to fstar-mai...@googlegroups.com
On 19th 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.
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 Or call in (audio only)
+1 323-849-4874,,603229037#
United States, Los Angeles
0008000401142,,,,603229037#
India (Toll-free)
________________________________________________________________________________
Reply all
Reply to author
Forward
0 new messages