Ну, вот на Схеме можно легко писать телеграм ботов, и можно уже давно. Но популярности это не добавляет. Контрпример :)

Первое соответствие совсем не понятно. Потому что я до сих пор думал, что cut - это правило, а не терм. Состояние, ведь, должно быть термом. Разве не так?

эм

вполне себе терм

здесь правда не видно разделение на термы и котермы, вот LJT

тут их аж 4 :)

на самом деле тут принципален только Cut3, остальные это явные подстановки

термы с пустой ступой - собственно термы, с заполненной - котермы

https://arxiv.org/abs/1807.05923

Это оно?

В том числе. У него лекции ещё есть.

Спасибо, не зря уточнил.

Я запутался. Что же мы считаем термом? Дроби?

это система ND, узнаете лямбда-исчисление? :)

вот то же самое на идрисе

data Term : List Ty -> Ty -> Type where
  Var : Elem a g -> Term g a
  Lam : Term (a::g) b -> Term g (a~>b)
  App : Term g (a~>b) -> Term g a -> Term g b

Initial commit, done https://t.me/compiler_jobs

замечания, предложения, помощь, и тп в личку - так как я в перерывчике просто по ХХ(который тут выше пнули) пролистал
в режиме пассивном, но надеюсь не без помощи, предлагаю закинуть другие ресурсы, включая прямые от компаний.

формат и прочее, а также администрирование, сборк статистики тоже приветствуется

data Term : List Ty -> Ty -> Type where
  Var : Elem a g -> Term g a
  Lam : Term (a::g) b -> Term g (a~>b)
  App : Term g (a~>b) -> Term g a -> Term g b

Ну. Это, вроде, стандартная интерпретация и узнать легко. Но не понятно, как правила вывода можно считать термами. Нет, конечно, понятно, что дерево доказательства можно записать в виде данных. И можно записать протокол работы абстрактной машины.

Но это же будут просто выражения. Не понятно интуитивно, откуда вылазит отсюда ко... Ну. Вроде как, ко-это же верхний предел, всевозможные варианты и всякие такие вещи. А тут, вроде, состояние и состояние. Не видно тонкостей.

По сути, лямбда-терм кодирует дерево вывода...