We are excited to announce the first release of asai 浅い on OPAM, along with new versions of algaeff and yuujinchou 友人帳. We also released bwd and mugen 無限 on OPAM earlier but didn’t make an announcement.
All these packages are part of our research project to dissect a typical proof assistant into composable components so that everyone can easily build a high-quality, usable prototype out of their type checker. It turns out that many components are useful for writing compilers, too. Here are our packages: (
means it’s on OPAM.)
- asai 浅い for compiler diagnostics.
- yuujinchou 友人帳 for namespaces and lexical scoping. See my TYPES 2022 talk for its design principles.
- bantorra for library management (still under heavy development and revisions)
- mugen 無限 for universe levels. See our POPL 2023 paper for a theoretic analysis of its design.
- kado カド for handling cofibrations in Cartesian Cubical Type Theory. This was also used for implementing unfolding control.
together with these more general-purpose packages:
- algaeff for well-known composable effects-based gadgets (e.g., state, reader, etc.)
- bwd for backward lists
We have a prototype system showing how these packages may be used together. Many packages have been used in our proof assistant cooltt, @jonsterling’s forester tool and Topos Institute’s polytt. We invite you to try out our packages the next time you want to build a proof assistant or compiler!