Мы как-то тоже делали cловарь терминов, правда там цель была не столько для перевода, сколько для выработки терминов для общения.

(Reply to this) (Thread)

Спасибо, хороший словарик.
Может быть, мне просто попробовать в него влиться?

(Reply to this) (Parent) (Thread)

конечно, было бы здорово!

Из замеченного в списке терминов (не претендую на правильность):

bounded quantification

ограниченная квантификация (в списке на сайте пропущена буква, наверняка опечатка, но на всякий случай, чтоб копи-пастом не разошлось)

featherweight Java

облегчённая Java (я не в курсе о чём речь, но может „легковесная“; хотя далее есть “lightweight formal method” и там уж точно „облегчённый” лучше)

simply typed lambda calculus

простое типизированное просто-типизированное лямбда-исчисление (simple vs. simply, наречие относится к “typed”, а не к “λ calculus”)

termination proof

доказательство гарантии завершения (присутствие сразу и слова „доказательство”, и „гарантии” мне кажется излишним. Может выкинуть „гарантии” (и, возможно, заменить „завершения” на „завершимости”)?)

trapped run-time error

диагностируемая ошибка времени выполнения (тут видимо нужен контекст, но меня смущает несоответствие “trapped” (прилагательное, от глагола прошедшего времени) и „диагностируемая” (прилагательное, от инфинитива (? — я не спец в русском). Я бы перевёл как „перехваченная/обнаруженная ошибка времени выполнения”.)

logical framework

логическая конструкция (вспоминая лекции по матану, там про подобные по смыслу вещи говорилось „аппарат”, соответственно „логический аппарат”)

well founded

вполне обоснованный („хорошо обоснованный”? нужен контекст)

(Reply to this) (Parent) (Thread)

Спасибо!
Вообще говоря, такое обсуждение, наверное, лучше уже в список рассылки. Поскольку Вас там пока нет, отвечаю здесь.

featherweight Java

Это название игрушечного языка программирования, который описывается в одной из глав (разумеется, основанного на Java). Мне кажется, "легковесная" в названии звучит неестественно.

simply typed lambda calculus

Формально Вы правы, но "просто-типизированное" через дефис уж больно громоздко по-русски. Поскольку из типизированных лямбда-исчислений это и вправду простейшее, а все остальные являются его расширениями, термин, хоть и не является точным переводом, в заблуждение не вводит.

termination proof

А вот здесь я, наоборот, буду защищать громоздкий вариант в угоду точности. "Доказательство завершения" -- это доказательство, что _конкретное_ вычисление завершается. "Доказательство завершимости" -- доказательство, что (может быть, и всякое) вычисоление _способно_ завершиться, то есть, _возможно_, завершается. Более короткого выражения, которое бы указывало, что _всякое_ вычисление _всегда_ завершается, я не нашел.

trapped run-time error

trapped здесь просто пассивное причастие, без привязки ко времени, и смысл выражения -- a type of error that is always being trapped.

logical framework

Вот здесь Вы, может быть, правы. Надо посмотреть, насколько хорошо "аппарат" ложится в текст (а также посмотреть во втором томе, где про этот самый Edinburgh framework подробнее рассказывается, насколько подходит по смыслу.

well founded

Это термин, который, безусловно, существует в русскоязычной логической литературе. Я попытался поискать по словарям и Википедии, а также вспомнить, как именно мне когда-то это понятие называл русский лектор, и, вроде бы, well ordering переводится как "полный порядок", а well-ordered set как "вполне упорядоченное множество". Но хотелось бы, чтобы какой-нибудь активно практикующий логик это подтвердил.

Сейчас я перегоню терминологию в ваш словарь, и, надеюсь, больше народу посмотрит и выскажет свое мнение.

(Reply to this) (Parent) (Thread)

Имеет тогда смысл после обновления нашего словаря кинуть объявление на гугл-группы SPbHUG и MskHUG, чтоб народ посмотрел, ну и заодно туда можно приглашение кинуть, так охват довольно большой получится.

(Reply to this) (Parent)