Ответ 1
ООП не вытекает из какого-либо строгого формализма, но это действительно формализм. Был предпринят ряд попыток правильно определить этот формализм. Наиболее заметную работу выполняет Luca Cardelli: http://lucacardelli.name/indexPapers.html (см. Раздел "Объекты" )
Императивное программирование может быть основано на любом формализме, эквивалентном Тьюрингу, включая лямбда-исчисление, СК-логику, абстрактную машину Тьюринга, алгоритмы Маркова или любую другую аналогичную систему перезаписи времени (TRS). Общее программирование ничем не отличается, это термин переписывающей системы рода.
Итак, для наиболее распространенных математических оснований буквально все, что вам нужно, чтобы зарыться в системы перезаписи терминов.
Более поздняя работа - недавняя работа AbdelGawad в Университете Райса. Он создает математическую модель основного ООП (например, Java, С#, С++, Scala, X10 и т.д.), Называемую NOOP. Вот ссылка на его кандидатскую диссертацию http://scholarship.rice.edu/handle/1911/70199