add guest talk

Author: ltzone

_posts/2024-04-30-jason-hu.md

@@ -0,0 +1,30 @@
+--- 
+layout:  post 
+title:   Layered Modal Type Theory
+authors: Jason Hu
+date:    2024-4-30 9:30:00 +0800
+venue:   CB308
+--- 
+
+This is a guest talk by Jason Hu from McGill University (website: https://hustmphrrr.github.io)
+
+### Abstract
+
+In this talk, we describe a type theory based on modal logic which supports meta-programming and intensional analysis. What sits at the core is the idea of layering. In a layered modal type theory, a language at a higher layer extends one at a lower layer with the extra power of meta-programming through the box modality. This architecture not only ensures a universal run primitive which executes code as programs, but also enables pattern matching on code while still retaining normalization. Our type theory is proven normalization by evaluation using an extended presheaf model. We see this development as a significant first step to support meta-programming in proof assistants' core languages. 
+
+### Venue information
+
+The speaker will give the talk via Zoom. All are welcome to join the talk in person at CB308 or online via Zoom.
+
+```
+Topic: HKU PL Group Seminar
+Time: Apr 30, 2024 09:00 AM Hong Kong SAR
+
+Join Zoom Meeting
+https://hku.zoom.us/j/93429804537?pwd=N0lDVmlXSHlHQzZZZ1ltZGJjeXAzdz09
+
+Meeting ID: 934 2980 4537
+Password: 428671
+```
+
+The talk will start at 9:30 am, but please feel free to join the meeting at 9:00 am for a chat.