POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States

This program is tentative and subject to change.

Sat 25 Jan 2025 10:00 - 10:30 at Duck, Duck Goose - Session 1

We present work-in-progress on generic implementations of higher-order unification algorithms in Haskell. We rely on the Free Foil library for generic (in the style of data types à la carte) representation of syntax with binders. We extend Free Foil with parametrised metavariables to achieve a (limited) version of Second-Order Abstract Syntax, over which we then implement generalized versions of Huet’s preunification and Miller’s higher-order pattern unification algorithms. We also plan to work towards a dedicated benchmark suite to compare standalone unification algorithms. Our goal is to provide a library of sufficiently reusable and reasonably performant language-agnostic higher-order unification algorithms to assist development of systems such as dependently typed languages.

Abstract (wits25-paper4.pdf)353KiB

This program is tentative and subject to change.

Sat 25 Jan

Displayed time zone: Mountain Time (US & Canada) change

09:00 - 10:30
09:00
60m
Keynote
Invited Talk: Type inference in OCaml and GHC using Levels
WITS
10:00
30m
Talk
Towards Generic Higher-Order Unification Implementations in HaskellRemote
WITS
Nikolai Kudasov Innopolis University, Artem Starikov Innopolis University, Fedor Ivanov Innopolis University, Damir Alfiatonov Innopolis University
File Attached