POPL 2022 (series) / WITS 2022 (series) /
WITS 2022 Program
This is the WITS 2022 program - see the full program for POPL 2022 and all affiliated events.
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sat 22 JanDisplayed time zone: Eastern Time (US & Canada) change
Sat 22 Jan
Displayed time zone: Eastern Time (US & Canada) change
09:00 - 10:00 | |||
09:00 15mTalk | CN: A Refinement Type System for CRemote WITS Christopher Pulte University of Cambridge, UK, Dhruv Makwana University of Cambridge, Kayvan Memarian University of Cambridge, Jean Pichon-Pharabod Aarhus University, Peter Sewell University of Cambridge, Neel Krishnaswami University of Cambridge | ||
09:15 45mOther | Type-aware equational rewriting (discussion)In-Person WITS Richard A. Eisenberg Tweag | ||
09:15 45mOther | Multi case trees: confluence and coverage (discussion)In-Person WITS Tesla Zhang The Pennsylvania State University | ||
09:15 45mOther | Intrinsically-Typed Interpreters for Effectful and Coeffectful Languages (discussion)Remote WITS Syouki Tsuyama Tokyo Institute of Technology, Youyou Cong Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology File Attached | ||
09:15 45mOther | The Expression Problem and Theorem Proving (discussion)Remote WITS Yao Li University of Pennsylvania, Nick Rioux University of Pennsylvania, Stephanie Weirich University of Pennsylvania | ||
10:20 - 12:00 | |||
10:20 45mKeynote | Make Three To Throw Away: Frontiers in Homotopical Proof AssistantsRemote WITS Jonathan Sterling Aarhus University | ||
11:05 15mTalk | The curious case of case: correct & efficient representation of case analysis in Coq and MetaCoqRemote WITS Matthieu Sozeau Inria, Meven Lennon-Bertrand Inria – LS2N, Université de Nantes, Yannick Forster Inria | ||
11:20 40mOther | Elaborator reflection APIs (discussion)Remote WITS Jesper Cockx TU Delft | ||
11:20 40mOther | Invisible arguments: language design (discussion)In-Person WITS Richard A. Eisenberg Tweag | ||
13:30 - 14:45 | |||
13:30 15mTalk | Tries that matchRemote WITS Sebastian Graf Karlsruhe Institute of Technology | ||
13:45 15mTalk | Gotta prove fast: building an ecosystem for effortless native compilation of tacticsRemote WITS Sebastian Ullrich Karlsruhe Institute of Technology | ||
14:00 45mOther | Benchmarking Binding (discussion)In-Person WITS Stephanie Weirich University of Pennsylvania | ||
14:00 45mOther | Fancy module systems (discussion)Remote WITS Jesper Cockx TU Delft | ||
15:05 - 16:20 | |||
15:05 15mTalk | mitten: A Flexible Multimodal Proof AssistantRemote WITS Philipp Stassen Aarhus University, Daniel Gratzer Aarhus University, Lars Birkedal Aarhus University | ||
15:20 15mTalk | Understandable and Useful Error Messages for Liquid TypesRemote WITS Alcides Fonseca LASIGE, Faculdade de Ciências da Universidade de Lisboa, Catarina Gamboa LASIGE, Faculdade de Ciências da Universidade de Lisboa, João David LASIGE, Faculdade de Ciências da Universidade de Lisboa, Guilherme Espada LASIGE, Faculdade de Ciências da Universidade de Lisboa, Paulo Canelas LASIGE, Faculdade de Ciências da Universidade de Lisboa | ||
15:35 15mTalk | Deciding type equivalence with simple grammarsIn-Person WITS Bernardo Almeida LASIGE, Faculty of Sciences, University of Lisbon, Andreia Mordido Lasige / Faculty of Sciences, Universidade de Lisboa, Vasco T. Vasconcelos LASIGE, Faculty of Sciences, University of Lisbon | ||
15:50 15mTalk | Typechecking up to CongruenceIn-Person WITS Jad Elkhaleq Ghalayini University of Cambridge | ||
16:05 15mTalk | À bas l’η — Coq’s troublesome η-conversionRemote WITS Meven Lennon-Bertrand Inria – LS2N, Université de Nantes | ||
16:40 - 17:30 | |||
16:40 15mTalk | Using Dependent Types at Scale: Maintaining the Agda Standard LibraryIn-Person WITS | ||
16:55 15mTalk | Setting the Record Straight with SingletonsRemote WITS Reed Mullanix University of Minnesota | ||
17:10 15mTalk | First-class pattern synonymsIn-Person WITS Tesla Zhang The Pennsylvania State University | ||