Extensible elaborators for dependently-typed languages

Bohdan Liesnikov

Date: Wed, September 21, 2022
Time: 12:00
Room: E.420 Turing (building 28) / Zoom room tba

There are a few established implementations of dependently-typed languages like Agda, Coq or Idris. However successful they are the implementation details are quite complex and only a few dare to extend them. This exists in contrast with Haskell, which has a rich culture of extensions, both in the form of pragmas and plugins.

This work aims to bring similar capabilities to the dependently-typed world. We are working on a design sketch of a dependently-typed language that would be extensible on the front-end, without affecting the core and thus, soundness of the language. The focus is on constraint-solving as part of the elaboration procedure, leaving syntax extensions to be solved at a later point. This is work-in-progress.

Previous: |
Next: Paul van der Stel |