Термин

Русские аналоги

Комментарии

alias analysis

анализ псевдонимов

array bounds checking

проверка выхода за границы массива

arrow type

стрелочный тип

boilerplate

служебный код? --- VictorNazarov
котельное железо, подлежащее сдаче в металлолом (Scrap your boilerplate) -- DenisMoskvin

bottom

основание

наименьший элемент ?...
Пусть будет по Харрисону - основание -- DenisMoskvin

bounded quantification

ограниченная квантификация

the Calculus of Communicating Systems (CCS)

Исчисление Взаимодействующих Систем

call-by-value lambda calculus

лямбда-исчисление с вызовом по значению

closure

замыкание

computation rule

рабочее правило

к сожалению, прямой перевод не проходит, поскольку computation rules -- подвид evaluation rules -- YuraBronnikov (see TaPL 3.5)

congruence rule

правило соответствия

здесь, наоборот, прямой перевод вроде и есть, но по-русски из него ничего не понятно. "Правило выбора"? -- YuraBronnikov

continuation

продолжение

не уверен -- EugeneKirpichov

core language

базовый язык

Curry-Howard correspondence

Соответствие Карри-Ховарда

currying

карринг, каррирование

карринг - по переводу Филда и Харрисона, каррирование - по Душкину -- DimitriTimofeev
предлагаю оставить только карринг

de Bruijn term

терм де Брюйна

проблема с транслитерацией фамилии -- YuraBronnikov

dependent types

зависимые типы

derived form

производная форма

destructive updates

divergence

расхождение

domain theory

теория доменов

downcast type conversion

нисходящее преобразование типов

eager (evaluation)

Кажется Денис говорил "энергичное". Не уверен, что хорошо
энергичное - распространенный вариант -- DimitriTimofeev

effect systems

системы эффектов

evaluation relation

отношение вычисления

evaluation strategy

стратегия вычисления

existentional polymorphism

экзистенциональный полиморфизм

first-class (objects/citizens)

объекты первого класса

"граждане" вряд ли стоит переводить
я так понимаю, это взято из социального устройства Древнего Рима

fixed point

неподвижная точка

по аналогии с общепринятым переводом в функциональном анализе

fixed point combinator

комбинатор неподвижной точки

не уверен -- IvanTarasov
по-моему OK -- DenisMoskvin

fusion

спаивание --- VictorNazarov
слияние -- DenisMoskvin

general recursive function

общерекурсивная функция

есть возражения? -- IvanTarasov

guard

защита

страж, охрана, "охрана" и "охранное выражение" чаще всего вижу -- SergeyLymar, предохранитель не нравится --- VictorNazarov
защита - из защищенных команд Дейкстры

guard (in a conditional)

условие

head normal form

заголовочная нормальная форма

У Филда-Харрисона - заголовочная нормальная форма (ЗНФ) (параграф 6.5) -- DenisMoskvin

higher-order function

функция высшего порядка

impredicative polymorphism

импредикативный полиморфизм

incremental

инкрементальный

наверное, есть еще более "русский" перевод?
наращиваемый/накапливающий(ся) --- VictorNazarov

instance declaration

объявление экземпляра

ох, не нравится мне -- DenisMoskvin

intersection types

типы-пересечения

... is lazy in ...

... ленив по ...

lazy evaluation

ленивое вычисление

здесь "выичсление" - процесс, а не объект

lightweight formal method

облегченный формальный метод

least fixed point

наименьшая неподвижная точка

list comprehension

выделение списка, абстракция списка

плод долгих дискуссий (по аксиоме выделения) -- DenisMoskvin
Абстракция-то откуда?? -- DenisMoskvin
Термин есть в переводе Филда-Харрисона, конструкция очень близка к абстракции множеств --- Victor Nazarov

logical framework

логическая конструкция (?)

as in Edinburgh Logical Framework

model checker

программа проверки моделей

naming context

контекст именования

natural semantics

естественная семантика

operational semantics

операционная семантика

partial function

частичная функция

есть возражения? -- IvanTarasov

pattern matching

сопоставление с образцом

есть вариант короче?
Вообще этот устоявшийся

pattern guard

охрана шаблона, может защита c образцом?,

не уверен -- IvanVeselov

persistence

persistent (ephemeral) data structure

phantom type

фантомный тип

polymorphic lambda-calculus

полиморфное лямбда-исчисление

polymorphic type inference

полиморфный вывод типов

product

произведение

даже для типов?

proof carrying code

код, содержащий доказательство

properly tail recursive

pure type systems

чистые системы типов

ramified theory of types

ветвящаяся теория типов

reduction

редукция

referential transparency

прозрачность по ссылкам

как-то непонятно -- IvanTarasov
тоже не нравится, может быть свободная цитируемость --- VictorNazarov

region inference

вывод регионов

row variables

переменные строк (???)

run-time monitoring

мониторинг исполнения

section

сечение

semantic domain

семантический домен

или все-таки "область"? -- YuraBronnikov

sharing

разделение

разделение? --- VictorNazarov
согласен -- DimitriTimofeev

shortcut fusion

сокращение слиянием? -- DenisMoskvin

simply typed lambda calculus

простое типизированное лямбда-исчисление

small step/big step operational semantics

операционная семантика с малым/большим шагом (???)

Коряво это. small step я бы назвал "пошаговой", но тогда не могу придумать соответствующего термина для big step -- YuraBronnikov

static typing

статическая типизация

strict/non-strict

строгий/нестрогий

другие варианты?

strict/non-strict semantics

нестрогая семантика звучит слишком нестрого

strong typing

сильная типизация

часто встречается строгая типизация, но это довольно невнятный термин -- DimitriTimofeev
Строгая, по-моему, более распространенный термин. А нечеткий он и в оригинале. -- OlegAvdeev

structural operational semantics

структурная операционная семантика

stuck evaluation, stuck term

вычисление в тупике, тупиковый терм

subtyping

наследование

sum

сумма

даже для типов?

suspended computation

отложенное вычисление

здесь "вычисление" - объект, а не процесс

suspension

хм. см. suspended computation

term rewriting

переписывание/трансформация термов

?

termination proof

доказательство гарантии завершения

then/else part

истинная/ложная ветви (условного выражения)

thunk

отложенное вычисление

переходник - вроде общепринято? -- DenisMoskvin
мне понравились „санки“ в Женином докладе, но использовать я бы такой перевод не стал -- IvanTarasov Отложенное вычисление (см. http://en.wikipedia.org/wiki/Thunk) Еще мог-бы быть "вектор вызова функции" - DmitryGolubovsky (Такого слова "thunk" в англ. даже Merriam-webster не знает...;)
Я за "отложенное вычисление" --- VictorNazarov
Согласен, исправил -- DenisMoskvin

total function

тотальная функция

есть возражения? -- IvanTarasov, может полная функция --- VictorNazarov

transition function

функция переходов

translucent types

полупрозрачные типы

trapped run-time error

диагностируемая ошибка времени выполнения

tuple

кортеж

tying the knot

затягивание узла

затягивание лучше, чем зывязывание, да?

type class

класс типов

type soundness

По крайней мере так sound/soundness переводится в книжках по мат. логике, напр. Чёрч А. Введение в математическую логику (1960) -- OlegAvdeev
А как тогда sound type system? soundness proof? Мне кажется, "корректность" лучше --- YuraBronnikov
Да, устоявшегося термина не видно. Вот еще тут и тут переводится как семантическая непротиворечивость, причем в первом случае речь идет именно о системах типов. -- OlegAvdeev

type safety

типовая безопасность

???

type variable

тИповая переменная

обратите внимание на ударение

typed lambda-calculus

типизированное лямбла-исчисление

unit type

единичный тип

или, всё-таки, единичный? -- DenisMoskvin
скорее, единичный -- IvanTarasov
в нем ровно один элемент кроме bottom (см.)
исправил пустой на единичный -- DenisMoskvin

universal polymorphism

универсальный полиморфизм

weak head normal form

слабая заголовочная нормальная форма

с weak вопросов, думаю, не возникнет, а вот hnf... (см.)
по переводу Филда и Харрисона -- DimitriTimofeev

well founded

вполне обоснованный

variable capture

захват переменной