Используется как базис для системы интерактивного доказательства Coq и ряда подобных инструментов
https://ru.wikipedia.org/wiki/Кодирование_Чёрча
https://ru.wikipedia.org/wiki/Формальная_система
Ну может не в таком жутком виде, но в адаптированном эти вещи вроде как подходят для исчисления моделей.
Имеется ввиду сама идейная часть. Надо думать.
На самом деле остенсивные определения по сути соответствуют константам в абстрактном языке (абстрактной формальной системе) "конкретная данная кошка", кошка это уже тип данных, а также может соответствовать типизированной переменной и т.п.
https://ru.wikipedia.org/wiki/Тип_данных
https://ru.wikipedia.org/wiki/Теория_типов
https://ru.wikipedia.org/wiki/Система_типов
https://ru.wikipedia.org/wiki/Семантика_(программирование)