[cjfd]

What exactly are the foundations of this? The rules on the page suggest that it is basically the calculus of constructions but the example involving the list suggests that there are inductive types too. Are the inductive types part of the foundations and omitted in the list of rules or are they something else that is not part of the foundation?

[caotic123]

Pompom does not offer inductive data types, instead, it provides static symbols (as in the LF framework or λΠ-Calculus Modulo). Of course, we do not use the rewriting foundation of these frameworks, however, we apply a usual unification algorithm to get the same power. There are a lot of things that need proper formalization in the core, but the intention of this work is not it yet. To be fair, not inductive data types as Coq/Agda.