Барендрегт, Хенк

Родился в 1947 году в Амстердаме. В 1952—1965 годы учился в образовательных учреждениях, использующих систему Монтессори. В 1967 году окончил Утрехтский университет по классу математической логики, получив степень магистра. В 1971 году под руководством Дирка ван Далена (нидерл. Dirk van Dalen) и Георга Крайзеля (нем. Georg Kreisel) защитил докторскую диссертацию (Ph. D.) по экстенсиональным моделям λ-исчисления и комбинаторной логики.

После защиты диссертации в 1971—1972 годах работал исследователем в Стэнфордском университете. С 1972 по 1986 год занимал профессорские должности в Утрехтском университете. С 1986 года — профессор Университета Неймегена, заведующий кафедрой оснований математики и информатики. В разное время работал на приглашённых позициях в Дармштадтском техническом университете, Швейцарской высшей технической школе Цюриха, Университете Карнеги — Меллон, Киотском университете, Сиенском университете.

Увлекается буддизмом и медитацией, публикует статьи о медитации в психологических и научно-популярных журналах[3].

Результаты начала 1970-х годов относятся к нормальным формам в λ-исчислении и реализуемости в комбинаторной логике. Труды второй половины 1970-х годов посвящены вопросам моделей λ-исчисления. Известность получил в 1981 году после выхода монографии «Ламбда-исчисление. Его синтаксис и семантика», дважды переиздававшейся и переведённой на русский и китайский языки и отмечаемой как основополагающий труд по бестиповому λ-исчислению[4].

В 1980-е годы изучал вопросы автоматического доказательства и взаимосвязи математического доказательства с λ-исчислением и теорией типов (впоследствии концептуализированные как изоморфизм Карри — Ховарда). В 1986 году после перехода в Университет Неймегена организовал группу, занимающуюся вопросами формализации математики, идейно продолжающую работы, которые велись в рамках проекта Automath Николаса де Брёйна. Во второй половине 1980-х изучал типизированные варианты λ-исчисления, с особым вниманием к взаимосвязям между ними; в 1991 году предложил λ-куб — графическую интерпретацию восьми различных типов типизированного λ-исчисления, снискавшую популярность как в среде логиков, так и среди специалистов по основаниям информатики и языкам программирования.

Член редколлегий журналов Information and Computation, Journal of Functional Programming, Journal of Logic and Computation, Logical Methods in Computer Science.

Член Европейской академии (1992). Академик Нидерландской королевской академии наук (1997).

В 2002 году удостоен ордена Нидерландского льва (рыцарь ордена). В том же году получил Премию Спинозы — крупную премию от нидерландской правительственной Организации научных исследований (нидерл. Nederlandse Organisatie voor Wetenschappelijk Onderzoek).

• Henk Barendregt. The Lambda Calculus. Its syntax and semantics (англ.). — Amsterdam: North Holland, 1981. — 622 p. — (Studies in Logic and the Foundations of Mathematics, vol. 103). — ISBN 0-444-87508-5. — фундаментальная монография по λ-исчислению, дважды переиздавалась (1984, 2012), переведена на китайский (1990) и русский (1985) языки:

  Барендрегт, Хенк. Ламбда-исчисление. Его синтаксис и семантика (рус.). — М.: Мир, 1985. — 606 с. — 4800 экз.

• Henk Barendregt, Wil Dekkers, Richard Statman. Lambda Calculus With Types (англ.). — Cambridge: Cambridge University Press, 2010. — 703 p. — (Perspectives in Logic). — ISBN 9780521766142. — объемлющее изложение вариантов типизированного λ-исчисления, различных расширений и приложений, задуманная как продолжение книги «Ламбда-исчисление. Его синтаксис и семантика». Переиздавалась в 2013 году.

• Henk Barendregt. Combinatory logic and the axiom of choice (англ.) // Indagationes Mathematicae. — 1973. — Vol. 3, no. 76. — P. 203—221.
• Henk Barendregt. A global representation of the recursive functions in the λ-calculus (англ.) // Theoretical Computer Science. — 1976. — No. 3.2. — P. 225—242.
• Барендрегт Х. Бестиповое λ-исчисление // Справочная книга по математической логике. / Под редакцией Дж. Барвайса. — М.: Наука, 1983. — Т. 4: Теория доказательств. — С. 278—318.
• Henk Barendregt, Adrian Rezus. Semantics for classical Automath and related systems (англ.) // Information and Control. — 1983. — Vol. 59. — P. 127—147.
• Henk Barendregt. Lambda calculi with types (англ.) // S. Abramsky, Dov M. Gabbay, and T.S.E. Maibaum (editors) Handbook of Logic in Computer Science. — Oxford: Oxford University Press, 1992. — Vol. 2: Background: Computational Structures. — P. 117–309. — ISBN 0-19-853761-1. — публикация, где впервые введён λ-куб.

• cs.ru.nl/~henk/ — официальный сайт факультета оснований математики и информатики Университета Неймегена — страница Хенка Барендрегта