POPL 2025 (series) / WITS 2025 (series) / WITS 2025 / Towards Generic Type Checking Implementations in Haskell via Second-Order Abstract Syntax
Towards Generic Type Checking Implementations in Haskell via Second-Order Abstract SyntaxRemote
This program is tentative and subject to change.
Sat 25 Jan 2025 11:00 - 11:30 at Duck, Duck Goose - Session 2
We present work-in-progress on the implementation of generic versions of the two most common classes of type checking algorithms — bidirectional typing and Hindley-Milner-style type inference — within the Free Foil framework, an efficient scope-safe representation for syntax with binders.
| Abstract (wits25-paper7.pdf) | 354KiB |
This program is tentative and subject to change.
Sat 25 JanDisplayed time zone: Mountain Time (US & Canada) change
Sat 25 Jan
Displayed time zone: Mountain Time (US & Canada) change
11:00 - 12:30 | |||
11:00 30mTalk | Towards Generic Type Checking Implementations in Haskell via Second-Order Abstract SyntaxRemote WITS Nikolai Kudasov Innopolis University, Anastasia Smirnova Innopolis University, Vladislav Deryabkin Innopolis University, Diana Tomilovskaia Innopolis University, Ekaterina Maksimova Innopolis University File Attached | ||
11:30 30mTalk | McTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory WITS Junyoung Jang McGill University, Jason Z.S. Hu Amazon Web Services, USA, Antoine Gaulin McGill University, Brigitte Pientka McGill University Pre-print File Attached | ||
12:00 30mTalk | Eta conversion for the unit type (is still not that simple)Remote WITS András Kovács University of Gothenburg and Chalmers University of Technology File Attached | ||