Ctrl K

Code underlying the publication: ExEl: Building an Elaborator Using Extensible Constraints

Code underlying the publication: ExEl: Building an Elaborator Using Extensible Constraints

2
contributors

Description

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.

Logo of Code underlying the publication: ExEl: Building an Elaborator Using Extensible Constraints
Keywords
Dependent Types
elaboration
elaborators
extensible datatype
open datatype
type-checking
Programming languages
License
  • BSD-3-Clause
</>Source code
Packages

Reference papers

Contributors

BL
JC
Jesper Cockx

Member of community

4TU