TY - DATA T1 - Code underlying the publication: ExEl: Building an Elaborator Using Extensible Constraints PY - 2024/03/21 AU - Bohdan Liesnikov AU - Jesper Cockx UR - DO - 10.4121/e74fd14a-da79-4686-97e8-143ac5e0858d.v1 KW - dependent types KW - elaborators KW - elaboration KW - open datatype KW - extensible datatype KW - type-checking N2 -

This repository contains source code for the paper, slides, extended abstract and a demo implementation for the ExEl paper. This research is addressing some of the common problems in the implementations of dependently typed languages. In particular we present a modular architecture for implementing the transformation from user-friendly surface syntax into a small and well-behaved core language, also known as elaboration. Our architecture is made modular through the use of an open datatype of constraints and a plugin system for solvers that work on these constraints, which means that each new feature is contained in its own module. The implementation was developed by the authors of the paper in through 2022 and 2023.

ER -