Что делает язык (и его систему типов) способным доказывать теоремы о своих собственных терминах?

Недавно я попытался реализовать Cedille-Core Аарона , минималистский язык программирования, способный доказывать математические теоремы о своих собственных терминах. Я также доказал индукцию для λ-кодированных типов данных на нем, что прояснило, почему его расширения были бы необходимы.

Тем не менее, мне все еще интересно, откуда взялись эти расширения. Почему они такие, какие они есть? Что их оправдывает? Я знаю, например, что некоторые расширения, такие как рекурсия, разрушают язык как систему доказательств. Если бы я решил расширить CoC с другими примитивами, как бы я оправдал это? Я понимаю, что требуется нормализация, но это не доказывает, что эти примитивы "имеют смысл".

Короче говоря, что конкретно определяет язык (и его систему типов) как систему, способную доказывать теоремы о своих собственных терминах?

[Самореклама следует, но я думаю, что это актуально.]

$t$$u$$t \equiv u$$t$$u$$\forall v, (\lambda x.x)\;v \equiv v$

Конечно, вы также можете предполагать эквивалентности, и существует несколько различных форм квантификаторов (типизированные / нетипизированные, универсальные / экзистенциальные). Этот механизм может быть использован для рассуждения о любой программе (их не нужно доказывать, что они завершились или даже напечатаны). Единственным ограничением является то, что программы, используемые в качестве доказательств, должны быть доказаны прекращением системой (произвольная общая рекурсия приводит к несогласованности).

Вот несколько ссылок, если вы хотите проверить это:

• https://lepigre.fr/files/docs/lepigre2017_pml2.pdf (недавняя статья с примерами)
• https://tel.archives-ouvertes.fr/tel-01590363 (кандидатская диссертация на английском языке)
• https://github.com/rlepigre/pml (языковая реализация)