This is a study on the design of extensible elaborators for dependently-typed languages. The gist of the idea is to allow extensiblity in the constraints datatypes and solvers.
abstract
contains markdown sources for the TYPES abstract submissionexel
contains Haskell sources for the prototype implementationpaper
contains text and illustration files for the paperslides
contains sources for the slides
Everything in this repo is buildable with nix, but can also be built with tools available.
For the LaTeX files you'll find dependencies listed in the paper.nix
file (or slides.nix
, abstract.nix
respectively for each subfolder).