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

Генк Барендрегт (Гендрік Пітер Барендрегт, нід. Hendrik Pieter Barendregt нар. 18 грудня 1947, Амстердам, Нідерланди) — нідерландський математик і логік, дослідник λ-числення і теорії типів, автор λ-куба. Професор, завідувач кафедри основ математики та інформатики Університету Неймегена.

Генк Барендрегт
Народився	18 грудня 1947(1947-12-18) (76 років) Амстердам, Нідерланди
Країна	Нідерланди
Діяльність	математик, інформатик, викладач університету
Alma mater	Утрехтський університет
Галузь	математична логіка і Основи математики
Заклад	Радбоуд університет Неймеген Радбоуд університет Неймеген Утрехтський університет
Науковий ступінь	доктор філософії
Науковий керівник	Дірк ван Даленd і Георг Крайзельd
Аспіранти, докторанти	Pieter Harteld Silvia Ghilezand Mariangiola Dezani-Ciancaglinid Bart Jacobsd Tonny Hurkensd Frank'a Waaldijkd Roelof Cornelis de Vrijerd Christiaan Peter Jozef Koymansd Bas Spittersd Jan Herman Geuversd Venanzio Caprettad Milad Niquid Adriana Beatriz Compagnonid Morten Heine Sorensend Erik Polld Jan Zwanenburgd Aline Klazina Honinghd Martijn Diederik Oostdijkd Gueorgui Ivanov Jojgovd Pieter Koopmand Sjaak Smetsersd Luis Cruz-Filiped Paula Gabriela Severid Steffen van Bakeld Milena Todovora Stefanovad Silvio Luigi Maria Valentinid Mark Pieter Jan Ruysd Jan Kuperd Erik Barendsend Marko van Eekelend
Членство	Нідерландська королівська академія наук Європейська академія
Нагороди	премія Спінозиd (2002)
Особ. сторінка	cs.ru.nl/~henk/
Генк Барендрегт у Вікісховищі

Біографія

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

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

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

Наукова і редакційна робота

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

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

Посилання

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