Генк Барендрегт

Народився 1947 року в Амстердамі. Протягом 1952—1965 років навчався в освітніх установах, що використовують систему Монтессорі. 1967 року закінчив Утрехтський університет за класом математичної логіки, отримавши ступінь магістра. 1971 року під керівництвом Дірка ван Далена і Георга Крайзеля захистив докторську дисертацію (Ph. D.) з екстенсіональних моделей λ-числення і комбінаторної логіки.

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

Захоплюється буддизмом і медитацією, публікує статті про медитацію в психологічних і науково-популярних журналах[5].

Результати початку 1970-х років стосуються нормальних форм у λ-численні і їх можливості бути реалізованими в комбінаторній логіці. Праці другої половини 1970-х років присвячені питанням моделей λ-числення. Став відомим 1981 році після виходу монографії «Лямбда-числення. Його синтаксис і семантика», яку двічі перевидано і перекладено російською і китайською мовами та вважають основною працею з безтипового λ-числення[6].

У 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 року відзначений орденом Нідерландського лева (лицар ордена). Того ж року відзначений премією Спінози від нідерландської урядової Організації наукових досліджень.

• Henk Barendregt. The Lambda Calculus. Its syntax and semantics. — Амстердам : North Holland, 1981. — 622 с. — (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 University Press, 2010. — 703 с. — (Perspectives in Logic) — ISBN 9780521766142. — об'ємний виклад варіантів типізованого λ-числення, різних розширень і застосувань; задумана як продовження книги «Лямбда-числення. Його синтаксис і семантика». Перевидано 2013 року.

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

• Сторінка Генка Барендрегта на сайті факультету основ математики та інформатики Університету Неймегена