Формальные модели объектно - ориентированного программирования:

A Semantics of Multiple Inheritance Luca Cardelli, (Семантика Множественного Наследования);
A theory of objects Luca Cardelli, Martin Abady;
версия 0.90 перевода статьи Семантика Множественного Наследования;
An Imperative Object Calculus Martin Abadi And Luca Cardelli, (Императивное Исчисление Объектов); Теория объектов Martin Abadi And Luca Cardelli, ;
On Understanding Types, Data Abstraction, and Polymorphism Luca Cardelli, Peter Wegner;
О понимании типов, абстракций данных и полиморфизма. On Understanding Types, Data Abstraction, and Polymorphism. Перевод журнала "Технология Клиент-Сервер". Почемуто не указали авторов исходной статьи
Basic Polymorphic Typechecking Luca Cardelli;
Базовая полиморфная проверка типов . Luca Cardelli, Basic Polymorphic Typechecking. Перевод Роман Душкин;
Мономорфизм, полиморфизм и экзистенциальные типы Роман Душкин;
Типы данных как решетки Дана Скотт (1975),
An Interpretation of Objects and Objects Types Martin Abadi, Luca Cardelli, Ramesh Viswanathan (Интерпретация Объектов и их Типов);
Object - Oriented Programming in Explicit Mathematics: Towards The Mathematics of Objects, Thomas Studer von Werthenstein (Объектно Ориентированное Программирование в Явной Математике: К Математике Объектов);
Towards Object - Oriented Refinement Calculus, Jamie Shield (К Объектно Ориентированному Исчислению Детализации);
Unifying Theories of Objects, Michael Anthony Smith and Jeremy Gibbons (Объединяя Теории Объектов);
rCOS: A Refinement Calculus for Object Systems, He Jifeng, Xiaoshan Li and Zhiming Liu (rCOS: Исчисления Детализации для Объектных Систем);
An Object-Oriented Approach to Formal Specification, Graeme Paul Smith (Объектно - Ориентированный подход к Формальным Спецификациям);
The Quarks of Object- Oriented Development, Deborach J. Armstrong (Кварки Объектно Ориентированной Разработки);
Современные языки программирования и .NET. Основы объектно-ориентированного подхода. Курс лекций Зыков С.
Объектно-ориентированное моделирование сложных динамических систем Ю.Б. Колесов
Абстрактные структуры: для и от данных, Шишков.

Типы и классы. Определения:

Карделли:
Есть множество V всех значений, содержащее такие простые значения, как целые, структуры данных, например, пары, записи, variant-типы и функции. Это законченный частичный порядок, созданный с помощью техники Скотта , но в первом приближении его можно рассматривать, как просто большое множество всех возможных вычисляемых типов.
Тип - это множество элементов V. Не все подмножества V являются корректными типами: они должны удовлетворять некоторым техническим требованиям. Подмножества V, удовлетворяющие таким требованиям, называются идеалами (ideals). Все типы в языках программирования в этом смысле являются идеальными, и нам не придется беспокоиться о подмножествах V, которые не являются идеалами.
Следовательно, тип - это идеал, который является множеством значений. Более того, множество всех типов (идеалов) в V, будучи упорядоченным посредством включения множеств, формирует структуру. На вершине этой структуры находится тип Top (множество всех значений, то есть сама V). Основание структуры - это, в сущности, пустое множество (реально - одноэлементное множество, содержащее наименьший элемент V).
Словосочетание <иметь тип>, таким образом, можно интерпретировать как членство в соответствующем множестве. Поскольку идеалы в V могут перекрываться, значения могут иметь много типов.

Гради Буч: Большинству смертных различать типы и классы просто противно и бесполезно.

Страуструп: Класс - это пользовательский тип.

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

Бадд: Новый взгляд на классы .

Википедия:
A data type (or datatype) In programming, a classification identifying one of various types of data, as floating-point, integer, or Boolean, stating the possible values for that type, the operations that can be done on that type, and the way the values of that type are stored.[1] (в программировании тип данных есть классификация указывающая один из многих типов данных, такие как плавающие точки, целые или логические, задающая возможные значения этого типа и операции, которые могут быть сделаны над данными этого типа, и способ, при помощи которого хранятся значения)

Харпер: В ML тип есть множество значений.

Дойч: тип это точная характеристика свойств, включая структуру и поведение, относящаяся к некоторой совокупности объектов.

Бертран Мейер: Класс - это абстрактный тип данных, поставляемый с возможно частичной реализацией.

Пискунов (дополнение к Мейеру): Тип - это спецификация класса.
В идеальном случае, задается множество значений данного типа (которое называется домен типа) и аксиомы, описывающие функции определенные на домене типа.
Например, аксиоматика натуральных чисел Пеано является основой для типа, то есть, спецификации класса unsigned int. Аксиоматика Пеано (на языке спецификаций RSL): домен типа и его свойства: множество целых и аксиома индукции, аксиомы которым должны удовлетворять функции сложения и умножения
Скорее всего, на систему аксиом - спецификацию типа должны накладываться дополнительные ограничения в смысле непротиворечивости и полноты. Чтобы тип задавал уникальный класс как в случаях, например, кольца целых и поля вещественных.
Пискунов: Класс - это синоним термина "абстрактный автомат".

Шопырин, Поликарпова: Объектно - ориентированный подход к моделированию и спецификации сущностей со сложным поведением


Типы против классов. Проблемы:

References and Footnotes: Subtyping, Subclassing, and Trouble with OOP;
The Liskov Substitution Principle. Example Принцип подстановки (замещения) Лисков, Роберт Мартин;
Об одном примере нарушения принципа подстановки Лисков кроме теоретико множественного анализа нарушения, расстривается возможность наследования между классами целых и натуральных чисел;
Subtyping and Inheritance for Inductive Types Выделение типа и наследование для индуктивных типов, Эрик Полл. Следующие его работы заводят в дебри чистой алгебры и теории катерогий. Эта достаточно программисткая;
Types vs classes: what is the difference?
Distinguishing Subclassing from Subtypes: из Теории объектов Карделли;
Практически закончен перевод книги Бенджамин Пирс Типы в языках программирования.

Типы, Множества и Классы. Обсуждение, проектирование и теория типов:

Классы и типы в языках, основанных на классах Luca Cardelli, Martin Abady (две главы из Теории Объектов);
Что такое тип? , частичный перевод текстов относительно типов из первого тома Инженерии програмного обеспечения Дениса Бьйорнера (Dines Bj0rner. Software Engineering 1. Abstraction and Modelling) ;
The RAISE Method Group: АЛГЕБРАИЧЕСКОЕ ПРОЕКТИРОВАНИЕ КЛАССА (200x)- формальная процедуры выбора аксиом для полного описания поведения функций-методов класса, по видимому, предложенная Гуттагом (John Guttag)
Abstract Data Types and Development of Data Structures Гуттаг, (1977), пример выбора аксиом для достаточно полного ("sufficiently complete") описания поведения функций абстрактного типа данных.
Лямбда- исчисление. Его синтаксис и семантика, Барендрегт, Мир, 1985 - с 548 страницы излагается типизинованное лямбда - исчисление.
A Formulation of the Simple Theory of Types, Alonzo Church, The Journal of Symbolic Logic, Vol. 5, No. 2., 1940;
Аксиоматические системы теории множества, Ван Хао, Мак-Нотон, Издательство иностранной литературы, Москва, 1963. 11 - 15 страница содержит теорию типов Рассела;
Введение в теорию типов Herman Geuvers, Radboud University Nijmegen and Technical University Eindhoven, The Netherlands, 2008.
Simple Type Theory as a Clausal Theory Gilles Dowek, ?Ecole polytechnique, 91128 Palaiseau Cedex, France.
THE CLAUSAL THEORY OF TYPES D.A. WOLFRAM, University of Oxford, Cambridge Tracts in Theoretical Computer Science.
Декларативное программирование, раздел Программы как теории, Дехтяренко, 2003 или pdf-файл Программы как теории на 6 странице содержит русскоязычное описание вариации простой теории типов Черча.
Формализация ООП: Типы, множества и классы, Пискунов А.Г, Петренко С.М., 2010.
Наследование абстрактных автоматов, Пискунов А.Г, 2008.

Formalization of the OOP Paradigm: Inheritance Of Abstract Automata, Piskunov A.G.;

Полезные книги:
Введение в матлогику Черч
Вычислимое и невычислимое Манин
Машина Поста Успенский
Теоретическая арифметика Арнольд. 1933
Universal coalgebra: a theory of systems , Универсальная коалгебра: теория систем. J, Rutten;
Tutorial On (Co)algebras and (Co)Induction , Руководство по (ко)алгебрам, Jacobs, Rutten;
Топосы. Категорный анализ логики, Р. Голдблатт, Москва, Мир, 1983;
Алгебраическая теория автоматов Под редакцией Арбиба
Djvu - вьюверы:
WinDjView-1.0-Setup.exe
Djvu.Reader.v2.0.26.zip

Замечания можно слать на адрес: agp1 точка ua ухо gmail точка com
Rambler's Top100