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.