Пирс Б. Типы в языках программирования
Подождите немного. Документ загружается.
B.3. Соглашения по именам и индексам 461
Trifonov, Valery and Scott Smith. Subtyping constrained types. In Proceedings of the Third International
Static Analysis Symposium, volume 1145 of LNCS, pages 349–365. Springer-Verlag, September 1996.
Turner, David N., Philip Wadler, and Christian Mossin. Once upon a type. In ACM Symposium on Functional
Programming Languages and Computer Architecture (FPCA), San Diego, California, 1995.
Turner, Raymond. Constructive Foundations for Functional Languages. McGraw Hill, 1991.
Ullman, JeMrey D. Elements of ML Programming. Prentice-Hall, ML97 edition,1997.
Ungar, David and Randall B. Smith. Self: The power of simplicity. In ACM Symposium on Object Oriented
Programming: Systems, Languages, and Applications (OOPSLA), pages 227–241, 1987.
U.S. Dept. of Defense.Reference Manual for the Ada Programming Language. GPO 008-000-00354-8, 1980.
van Benthem, Johan. Language in Action: Categories, Lambdas, and Dynamic Logic. MIT Press, 1995.
van Benthem, Johan F. A. K. and Alice Ter Meulen, editors.Handbook of Logic and Language. MIT Press,
1997.
van Heijenoort, Jan, editor.From Frege to G¨odel. Harvard University Press, Cambridge, Massachusetts, 1967.
van Wijngaarden, Adriaan, B. J. Mailloux, J. E. L. Peck, C. H. A. Koster, M. Sintzoff, C. H. Lindsey, L. G.
L. T. Meertens, and R. G. Fisker. Revised report on the algorithmic language ALGOL 68. Acta Informatica,
5(1–3):1–236, 1975.
Vouillon, J´erˆome. Conception et r´ealisation d’une extension du langage ML avec des objets. PhD thesis,
Universit´e Paris 7, October 2000.
Vouillon, J´erˆome. Combining subsumption and binary methods: An object calculus with views. In ACM
Symposium on Principles of Programming Languages (POPL), London, England, 2001.
Wadler, Philip. Theorems for free! In Functional Programming Languages and Computer Architecture, pages
347–359. ACM Press, September 1989. Imperial College, London.
Wadler, Philip. Linear types can change the world. In TC 2 Working Conference on Programming Concepts
and Methods (Preprint), pages 546–566, 1990.
Wadler, Philip. Is there a use for linear logic? In Proceedings of ACM Symposium on Partial Evaluation and
Semantics-Based Program Manipulation, pages 255–273, 1991.
Wadler, Philip. New languages, old logic. Dr. Dobbs Journal, December 2000.
Wadler, Philip. The Girard-Reynolds isomorphism. In Naoki Kobayashi and Benjamin Pierce, editors,
Theoretical Aspects of Computer Software (TACS), Sendai, Japan, Lecture Notes in Computer Science.
Springer-Verlag, 2001.
Wadler, Philip and Stephen Blott. How to make ad-hoc polymorphism less ad hoc. In ACM Symposium on
Principles of Programming Languages (POPL), Austin, Texas, pages 60–76, 1989.
Wadsworth, Christopher P. Semantics and pragmatics of the lambda-calculus. PhD thesis, Programming
Research Group,Oxford University, 1971.
Wand, Mitchell. Finding the source of type errors. 13th ACM SIGACT-SIGPLAN Symposium on Principles
of Programming Languages (POPL), pages 38–43, 1986.
Wand, Mitchell. Complete type inference for simple objects. In Proceedings of the IEEE Symposium on Logic
in Computer Science, Ithaca, NY, June 1987.
Wand, Mitchell. Corrigendum: Complete type inference for simple objects. In Proceedings of the IEEE
Symposium on Logic in Computer Science, 1988.
rev. 104
462 B.3. Соглашения по именам и индексам
Wand, Mitchell. Type inference for objects with instance variables and inheritance. Technical Report NU-CCS-
89-2, College of Computer Science, Northeastern University,February 1989a. Also in Carl A. Gunter and John
C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language
Design (MIT Press, 1994).
Wand, Mitchell. Type inference for record concatenation and multiple inheritance. In Fourth Annual IEEE
Symposium on Logic in Computer Science, pages 92–97, Pacific Grove, CA, June 1989b.
Weis, Pierre, Mar´ıa-Virginia Aponte, Alain Laville, Michel Mauny, and Asc´ander Su´arez. The CAML reference
manual, Version 2.6. Technical report, Projet Formel, INRIA-ENS, 1989.
Wells, Joe B. Typability and type checking in the second-order λ-calculus are equivalent and undecidable. In
Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS), pages 176–185,
1994.
Whitehead, Alfred North and Bertrand Russell. Principia Mathematica. Cambridge University Press,
Cambridge, 1910. Three volumes (1910; 1912; 1913).
Wickline, Philip, Peter Lee, Frank Pfenning, and Rowan Davies. Modal types as staging specifications for
run-time code generation. ACM Computing Surveys, 30(3es), September 1998. Article 8.
Wille, Christoph. Presenting C#. SAMS Publishing, 2000.
Winskel, Glynn. The Formal Semantics of Programming Languages: An Introduction. MIT Press, 1993.
Wirth, Niklaus. The programming language Pascal. Acta Informatica, 1(1):35–63, 1971.
Wright, Andrew K. Typing references by effect inference. In Bernd Krieg-Bruckner, editor, ESOP ’92, 4th
European Symposium on Programming, Rennes, France, volume 582 of Lecture Notes in Computer Science,
pages 473–491. Springer-Verlag, New York, N.Y., 1992.
Wright, Andrew K. Simple imperative polymorphism.Lisp and Symbolic Computation,8(4):343–355, 1995.
Wright, Andrew K. and Matthias Felleisen. A syntactic approach to type soundness. Information and
Computation, 115(1):38–94, 15 November 1994.
Xi, Hongwei and Robert Harper. A dependently typed assembly language. In International Conference on
Functional Programming (ICFP), Firenze, Italy, 2001.
Xi, Hongwei and Frank Pfenning. Eliminating array bound checking through dependent types. In ACM
SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Montreal, Canada,
pages 249–257, 1998.
Xi, Hongwei and Frank Pfenning. Dependent types in practical programming. In ACM Symposium on Principles
of Programming Languages (POPL), San Antonio, Texas, ACM SIGPLAN Notices, pages 214–227, 1999.
XML 1998. Extensible markup language (XML
TM
),February 1998. XML 1.0, W3C Recommendation, http:
//www.w3.org/XML/.
XS 2000. XML Schema Part 0: Primer, W3C Working Draft. http://www.w3.org/TR/xmlschema-0/,2000.
Yelick, Kathy, Luigi Semenzato, Geoff Pike, Carleton Miyamoto, Ben Liblit, Arvind Krishnamurthy, Paul
Hilfinger, Susan Graham, David Gay, Phil Colella, and Alex Aiken. Titanium: a high-performance Java
dialect. Concurrency: Practice and Experience, 10(11–13):825–836, September 1998. Special Issue: Java for
High-performance Network Computing.
Zwanenburg, Jan. Pure type systems with subtyping. In J.-Y. Girard, editor, Typed Lambda Calculus and
Applications (TLCA), pages 381–396. Springer-Verlag, 1999. Lecture Notes in Computer Science, volume
1581.
rev. 104
B.3. Соглашения по именам и индексам 463
Секрет креативности
заключается в знании того, как
спрятать свои источники.
Альберт Эйнштейн
rev. 104
Предметный указатель
F -консистентно, 224
F -опорным, 230
F -поддерживается, 230
F -висячим, 230
F -замкнуто, 224
Y -комбинатор с вызовом по значению, 59
АСД, 50
АТД, 287
Абстрактный синтаксис, 50
Аксиоматическая семантика, 36
Алгоритм W, 262
Алгоритм унификации, 256
Безопасность, 12
Числа Чёрча, 271
Дамасу-Милнеру, 258
Денотационная семантика, 36
Древовидный тип, 226
Естественной Семантики, 36
Экземпляр, 38
Главным решением, 257
Главным унификатором, 255
Хвостовым вызовом, 234
Исчисление Милнера-Майкрофта, 263
Конкретный (или поверхностный) синтаксис, 50
Конструкция последовательного исполнения, 99
Конструктор типов, 84
Лексикографический (или «словарный») порядок,
24
Логическая интуиция, 283
Лямбда-исчисление, 50
Множество ограничений, 252
Мультметоды, 182
Областью определения, 21
Областью значений, 21
Обобщаем, 260
Обобщение, 278
Одношаговое отношение вычисления, 38
Операционная семантика, 35
Отношение алгоритмической типизации, 172
Отношение многошагового вычисления, 40
Отношение типизации с ограничениями, 252
Параметрический полиморфизм, 265
Пенсильванской трансляцией, 161
Пи-исчисление, 49
Полиморфизм через наследование, 266
Положительные, 331
Последовательность, 23
Правило введения, 89
Размер, 33, 61
Рефлексивно-транзитивное замыкание, 23
Рефлексивное замыкание, 22
Решением, 251, 253
Система F, 265, 266
Специализированный полиморфизм, 266
Структурной Операционной Семантики, 36
Тип-перечисление, 111
Убывающая цепочка, 23
Вес, 327, 328
Ядерная Fun, 305
Янтарное правило, 244
Зависмые функциональные типы, 355
Значением, 36
абстрагировать, 185
абстрагируя, 265
абстракции, 101, 154
абстракции, определенные программистом, 286
абстракций, 12
абстракциями типа, 267
абстрактные синтаксические деревья, 50
абстрактные типы данных, 286
абстрактных типов данных, 268
абстрактный, 362
абстрактный синтаксис, 30
абстрактный тип данных, 287
абстрактный тип данных (АТД), 182
абстрактно, 14
абстрактной машины, 128
абстрактную машину, 35
адрес, 127
адресов памяти, 127
аксиомами, 31
алгоритмическое отношение наследования, 167
алгоритмическое отношение типизации, 167
альфа-конверсией, 63
анализ псевдонимов, 135
анализ размерностей, 13
аннотаций типов, 13
аннотацию, 109
антисимметрично, 22
арифметику указателей, 127
464
Предметный указатель 465
ассоциативности, 51
атомарным, 97
автоматически, 12
барьера абстракции, 287
базовые типы, 117
базовых типов, 97
бестиповое, 49
бета-редукцией, 52
безымянному терму, 66
безопасность, 80
бинарных операций, 292
бинарным отношением, 21
бисимуляции, 225
более обобщенной, 255
целей, 233
цикл, 130
частичным порядком, 22
частично абстрактными типами, 313
частичное вычисление, управляемое типами, 121
частичного вычисления, 90
частичной функцией, 22
частичной реконструкции типов, 263
частичную функцию, 46
числа Чёрча, 55
числовых значений, 41
чистые системы типов, 11
чистых, 123
чисто функциональными, 286
чистое, 49, 85
декартово произведение, 103
декларативные, 167
делегации, 209
делегатов, 182
дерево, 226, 413
дерево вывода, 38
дерево вывода типов, 79
деревьев вывода типов, 293
деревья типизации, 85
деревья вывода, 79
деструкторы типов, 377
диагностируемыми, 15
динамических, 12
динамическим, 266
динамическую проверку типов, 154
диспетчеризация методов, 181
доказательств, 13
доказательством, 356
достижим, 232, 396
достижим за один шаг, 396
достижимость, 396
единиц компиляции, 286
единственности типов, 87
естественная семантика, 43
естественной семантикой, 36
эффективные, 13
эквациональной унификации, 263, 418
эквирекурсивном, 219
эквиваленитны, 157
эквивалентны, 106
эквивалентные по определению, 219
эквивалентности определений, 340, 344
экзистенциальных унификандов, 251
экзистенциальную модель объектов, 367
финализаторы, 396
формальных методов, 11
функцией, 22
функцией перехода, 36
функцией с конечным множеством состояний, 232
функцией тождества, 52
функции интерпретации, 36
функции высшего порядка, 54
функция раскрытия сокращений, 99
функция тождества, 267
генератор счетчиков, 184
генератором, 115
гетерогенными, 107
гибкие кортежи, 307
гипотез, 233
главный, 257
главный тип, 249
главным типом, 257
главной типизации, 263
глубина, 34
глупое, 206
графах, 53
грязные, 123
имен типов, 200
именных, 214
именными, 200
импредикативный, 266
импредикативным, 280
импредикативного полиморфизма, 263
индексами де Брауна, 66
индексы, 69
индексов де Брауна, 295
индукция по выводам, 38
индуктивные доказательства, 33
индуктивные определения, 33
интенсиональный полиморфизм, 266
интерфейс, 182
интерфейсы, 206
интерфейсом, 181
инварианты, 36
инвариантный, 156
исчисление конструкций, 357
исчисление объектов, 49, 209
исчисления объектов, 147
исключения, 142
rev. 104
466 Предметный указатель
исключенного третьего, 90
изменчивости, 373
изоморфизм Карри-Ховарда, 89
изорекурсивное, 244
изорекурсивном, 220
канонических форм, 80
карринг, 340
каррированием, 54
категориальная грамматика, 16
классами-примесями, 209
классы, 182, 185
классов типов, 263
кодирование по Чёрчу, 271
когерентна, 163
когерентность, 163
коиндукции, 223
комбинатор неподвижной точки, 59
комбинаторами, 52
комбинаторной логике, 65
компоновки, 286
композиционально, 12
конечен, 226
конечной перегрузки операторов, 164
конечную высоту, 414
конфлюэнтно, 349
конкретизацией типа, 267
конкретизировать, 249
конкретизируем, 260
конкретизируется, 138
конкретных правил, 32
консервативен, 78
консервативны, 12
конструктивная теория типов, 11
конструкторы объектов, 199
конструкторы типов, 117, 339
конструктором типа, 347
контекст типизации, 84
контекста именования, 67
контекстов времени выполнения, 207
контравариантен, 147, 365
корректны, 169
корректность, 12, 80
кортежами, 104
кортежи, 103
ковариантен, 147, 365
красивой печати, 73
куб Барендрегта, 357
кучей, 123
кумулятивны, 32
квантификации высшего порядка, 339
латентных, 12
лексем, 50
лексер, 50
лексический анализатор, 50
лемма о подстановке, 86
лемма об инверсии, 351
лемма об обращении, 86
леммой о порождении, 79
ленивые, 53
линейная логика, 90
линейным порядком, 22
логические отношения, 119, 120
логические предикаты, 120
логическими конструкциями, 357
локальная реконструкция типов, 277
локальный вывод типов, 277
лямбда-абстракциями, 50
лямбда-исчисление, 49
лямбда-исчислением второго порядка, 267, 354
лямбда-куб, 357
лямбда-терм, 50
менее конкретной, 255
мерой завершения, 40
мета-математики, 30
метапеременной, 30
метатеория, 30
метаязыка, 30
меткой, 105
методами, 181
методы, 367
методов, 183
мини-ML, 263
минимальные предположения, 263
минимальный, 173
минимальный тип, 323
минимального ядра, 197
множествами кандидатов на редуцируемость, 119
множественного наследования, 377
модальные логики, 90
модульного программировния, 268
модульности, 12
модуля, 284
мониторинг исполнения, 11
монотипы, 279
монотонна, 224
мультиметоды, 209, 266
надтип, 154
наиболее общая, 251
наиболее общий, 257
наиболее общий унификатор, 255
насыщенными множествами, 119
наследование, 145
наследования интерфейсов, 370
наследования в глубину, 146
наследования в ширину, 146
натуральных чисел, 21
не завершаются, 59
недиагностируемыми, 15
rev. 104
Предметный указатель 467
неинтерпретируемых, 97, 249
неизвестных, 97
неопределенным элементом, 117
неперекрывающимися объединениями, 114
неподвижной точкой, 224
нестрогие, 53
неявно аннотированные, 259
неявно типизированными, 84
незащищенным, 277
незавершающийся комбинатор, 58
независимость представлений, 288
нисходящее, 154
нормализации, 275
нормализация вычислением, 121
нормализуем, 119
нормализуемых, 164
нормального порядка вычислений, 52
нормальной форме, 39
нормальной формой, 58
новое, 99
объединением, 22, 174
объединений, 168
объединения, 333
объект, 183
объекта, 126
объекты, 286
объектно-ориентированных, 145
объектно-ориентированной, 289
объектного языка, 30
объявлялся, 114
обладает объединениями, 174
обладает ограниченными пересечениями, 174
обладает пересечениями, 174
область видимости, 51
облегченного формального метода, 11
обобщает, 102
обобщенные функции, 266
обобщенных библиотек, 258
обработчики исключений, 139
обработчику исключений, 137
обращением к полю, 199
обратимой, 230
образцов, 106
общая рекурсия, 188
одноэлементные виды, 344
одноэлементных видов, 356
одноэлементными видами, 340
ограничена снизу, 174
ограничение на наследование, 302
ограничение на значения, 262, 279
ограничениями, 267
ограниченная квантификация, 302
ограниченные экзистенциальные типы, 313
ограниченных операторов над типами, 361, 365
ограниченным кванторам высших порядков, 362
ограниченную квантификацию, 301
окрашенный локальный вывод типов, 277
окружение, 74
окружение типизации, 84
опциональные значения, 110
операций над записями, 164
операционная интуиция, 283
операционная семантика с малым шагом, 36
операторами над типами, 339
операторами высших порядков над типами, 341
оператором над типами, 347
операторов над типами, 213
определена, 22
определением, 15
определениями, 340, 344
оставаться абстрактными, 250
освобождение, 126
ошибками типов времени выполнения, 12
ошибки, 142
ошибки времени выполнения, 42
ошибок времени выполнения, 39
отношение, 21
отношение типизации, 79
отношение вычисления, 37
отношением эквивалентности, 22
отношением видообразования, 339
отрицательные, 331
пакета, 284
памятью, 123
параллельная редукция, 349
параметрические типы данных, 343
параметрическому полиморфизму, 250
параметричности, 280
параметризован, 114
параметризованное сокращение, 339
пары, 103
перегрузка, 266
переменная строки, 418
переменные строк, 263
переменных, 65
переменных экземпляра, 183
переопределения, 209
переопределяет, 187
пересечением, 22, 174
пересечения, 163
перестановкой, 23
перезапускает, 141
поддеревом, 235
подинтерфейсам, 371
подклассами, 186
подклассов, 142
подстановка типов, 249
подстановка, свободная от захвата, 62
rev. 104
468 Предметный указатель
подстановки, 249
подтипом, 145
подвыражением, 240, 241
полей, 183
полиморфизм, 258
полиморфизм через let, 258, 266
полиморфизм первого класса, 266
полиморфизм ранга 2, 279
полиморфизма 2-го ранга, 263
полиморфизме переменных строк, 165, 377
полиморфизмом через наследование, 145
полиморфная перепаковка, 377
полиморфная рекурсия, 263
полиморфные, 265
полиморфное лямбда-исчисление, 267
полиморфное обновление, 372
полиморфного обновления, 367, 373
полиморфного обновления записей, 370
политипы, 279
полная F
<:
, 303
полная абстракция, 116
полны, 169
полным, 23
полное, 303
полной бета-редукции, 52
полноправные элементы языка, 339
полностью ограниченная квантификация, 333
полярность, 365
порождающей функцией, 224
порождения, 32
порождения кода во время выполнения, 90
посылка объекту сообщения, 181
последовательного исполнения, 124
постановки тегов, 107
поточечно, 361
поведенчески эквивалентен, 58
повышается, 138
повышая, 323
позднее связывание, 182, 188
позитивное наследование, 377
правил вывода, 31, 224
правила типизации, 79
правило удаления, 89
правилом соответствия, 38
правильно построен, 353
правильно типизировано, 133
предикативным, 280
предикатом, 21
предпорядком, 22, 148
предупреждение о глупости, 206
пренекс-полиморфизм, 279
преобразованием, 101
преобразований типа, 145
применением, 267
принципом безопасной подстановки, 146
приоритете, 51
приписывание, 100
приписывания типа, 153
присваивание, 124
присваивания, 123
присвоения видов, 344
приведение типа, 199
приведением типов, 154
приведения типов, 278
процессов, 216
продолжение, 293
продвижения, 80
проектировании абстракций, 289
программы проверки моделей, 11
произведение, 103
производная форма, 99
производные формы, 97
производных классов, 182
производных конструкций, 49
промежуточного языка, 128
простая теория типов, 11
простых классов, 371
простых типов, 84
простыми типами, 341
простое типизированное лямбда-исчисление с опе-
раторами над типами, 344
проверка на вхождение, 256
проверки моделей, 225
проверку на вхождение, 263
псевдонимами, 125
рабочими правилами, 38
расхождения, 22
распечаткой, 100
расширения субъекта, 89
расширить, 185
расширяемым вариантным типом, 141
расширять, 187
разделение, 356
разделением, 344
разыменование, 124
разыменовать, 123
разрешающей процедурой, 169
разрешимый, 13
редексом, 52
редукцией, 37
редукции субъекта, 82
редукцию, 353
рефлексии, 155
рефлексивно, 22
регулярным, 235
регулярными, 219
регулярными типами, 235
реконструировать, 84
rev. 104
Предметный указатель 469
реконструкции типов, 91, 249, 251, 266, 276, 390
рекурсивные типы, 107, 126
рекурсивным, 114
рекурсивным типам, 201
рекурсивными типами, 213
с большим шагом, 36, 43
с малым шагом, 43
самый левый лист, 278
сами, 36
санк, 191
сборку мусора, 126
сценариев доказательств, 356
счетным, 21
семантических доменов, 36
семантика подмножеств, 146
семантика с передачей типов, 278
семантике, 35
семантике со стиранием типов, 278
семантики через преобразования типов, 293
семантики на основе преобразования типов, 159
семантику на основе преобразования типов, 179
сырых, 198
сырых µ-типов, 236
схемы правил, 32
схемы типов, 279
схему типа, 260
сильными бинарными операциями, 292
сильной нормализации, 275
симметрично, 22
синонимом, 336
синтаксический анализатор, 51
синтаксическим сахаром, 100
синтаксическое упроавление помехами, 135
систем чистых типов, 343, 357
систем линейных типов, 90
систем модулей, 294, 356
системы присвоения типов, 84
системы типов, 11
скрытым типом-представлением, 284
слабая заголовочная редукция, 353
слабые указатели, 396
слабых типовых переменных, 262
слабыми бинарными операциями, 292
слоистым, 280
соглашение Барендрегта, 65
сохранения, 80
сохраняет, 22
сокращенную запись, 99
сократим, 237
соответствие Карри-Ховарда, 12, 89
соответствия, 370
соответствию Карри-Ховарда, 267, 331
сопоставления с образцом, 106
сопровождения, 13
состояние, 36, 183
состояние памяти, 261
состоянием, 367
создать экземпляр, 185
специфицированных типов, 263
ссылка, 123, 127
ссылкой, 125
ссылок, 271
статически, 78
статическим, 266
статическое, 12
стеков, 289
степенные типы, 344
степенные виды, 344
стилем Карри, 91
стирания, 90
стирания типов, 275
стратегию вычисления, 37
строгая нормализация, 121
строковые виды, 344
структурная индукция, 24
структурная операционая семантика, 36
структурных, 214
структурными, 200
структурное развертывание, 377
структуру данных, 411
структуру типизации памяти, 130
сужения, 310, 328
свидетельства, 90
свободных переменных, 61
свободно, 52
свойством Чёрча-Россера, 349
свойством ромба, 382
связаны, 21
связанным, 52
связыванием-пустышкой, 100
связывающее определение, 52
тактик, 356
тегами типов, 156
тегов типов, 12
теговое, 159
теории категорий, 19
теория доменов, 36
теория типов, 11
термами де Брауна, 66
термов, 29
терпят неудачу, 22
тип, 341
тип-объединение, 114
тип-вариант, 141
типам каналов, 158
типы форм, 356
типы-пересечения, 279, 309, 377
типы-уточнения, 164
rev. 104
470 Предметный указатель
типизируем, 79
типизируемым, 91, 276
типом представления, 185
типом состояния, 367
типом-свидетелем, 284
типов, 267
типов ограничений, 263
типов-объединений, 164
типов-сумм, 107
типов-вариантов, 110
типовых переменных, 94
типовым оператором, 114
типовым переменным, 249
точной нижней гранью, 22
точной верхней гранью, 22
тотальный, 327
тотальное, 229
тождества объектов, 195
транзитивно, 22, 227
транзитивное замыкание, 22
тупиковым, 42
удалением сахара, 100
удалять, 283
удовлетворяет, 252
указатель, 123, 127
унифицирует, 252
унификации, 255
универсальных доменов, 218
универсальное множество, 223
упакованное, 159
управляются синтаксисом, 167
уровни де Брауна, 69
устранения сечений, 90
утверждение (или суждение) о вычислении t t
выводимо, 38
утверждения, 79
утверждения как типы, 90
в стиле ML, 258, 266
в стиле Чёрча, 91
в тупике, 200
вариантные типы, 107
верны по построению, 356
ветвящаяся теория типов, 11
вычисление, 37
вычислении субъекта, 82
вычислительными эффектами, 123
выделение памяти, 124
выполняется, 38
вырожденным, 85
вывести, 84, 99
вывод типов, 251
вывода регионов, 16
вызов метода, 181, 199
вызов по необходимости, 53
вызова по значению, 53
вызовом по имени, 53
видами, 267
виды записей, 344
видов, 340
видов уровня i, 354
висячих ссылок, 127
включения, 146
вложенной индукцией, 24
внешним языком, 50
вниз, 206
внутренних классов, 198
внутренним языком, 50
восходящее, 154
вполне упорядоченным множеством, 23
всюду определенной (тотальной) функцией, 22
всюду определено, 169
вверх, 206
вводить, 283
ячейкой памяти, 125
ядерная F
<:
, 303
ядерное, 303
ядерное правило, 305
явных подстановок, 65
явно типизированными, 84
явную подстановку, 74
языков описания модулей, 14
захват переменных, 62
замкнутым, 52
записей активации, 139
зависимые виды, 344
зависимых типов, 15, 355
значений, 37
значениями, 31
значению, 53
жадного вывода типов, 277
cons с хэшированием, 178
0-термами, 66
проверку выхода за границы массивов, 15
F-ограниченная квантификация, 303
LF, 357
Objective Caml, 45
OCaml, 45
PCF, 116
rev. 104