Barendregt, Henk

Henk Barendregt ( Hendrik Pieter Barendregt , Niderl.  Hendrik Pieter Barendregt ; narozen 18. prosince 1947 ) je holandský matematik a logik , výzkumník λ-kalkulu a teorie typů , autor λ-krychle . Profesor, vedoucí katedry základů matematiky a informatiky na univerzitě v Nijmegenu .

Životopis

Narozen v roce 1947 v Amsterdamu . V letech 1952-1965 studoval na vzdělávacích institucích systémem Montessori . V roce 1967 promoval na univerzitě v Utrechtu v oboru matematická logika a magisterský titul. V roce 1971 pod vedením Dirka van Dalena ( Nizozemština.  Dirk van Dalen ) a Georga Kreisela ( německy  Georg Kreisel ) obhájil doktorskou disertační práci ( Ph.D. ) o extenzních modelech λ-kalkulu a kombinatorické logice .

Po obhajobě disertační práce působil v letech 1971-1972 jako vědecký pracovník na Stanfordské univerzitě . Od roku 1972 do roku 1986 zastával profesury na univerzitě v Utrechtu . Od roku 1986 - profesor na univerzitě v Nijmegenu , vedoucí katedry základů matematiky a informatiky. V různých dobách pracoval na pozvaných pozicích na Darmstadt University of Technology , ETH Zurich , Carnegie Mellon University , Kyoto University , Siena University .

Má rád buddhismus a meditaci , publikuje články o meditaci v psychologických a populárně naučných časopisech [2] .

Vědecká a redakční práce

Výsledky z počátku 70. let se týkají normálních forem v λ-kalkulu a realizovatelnosti v kombinatorické logice . Práce druhé poloviny 70. let jsou věnovány otázkám modelů λ-kalkulu. Proslul v roce 1981 po vydání monografie „Lambda Calculus. Jeho syntaxe a sémantika“, která byla dvakrát přetištěna a přeložena do ruštiny a čínštiny a označena jako základní práce na netypovém λ-kalkulu [3] .

V 80. letech studoval otázky automatického důkazu a vztah matematického důkazu s λ-kalkulem a teorií typů (následně konceptualizována jako Curry-Howardův izomorfismus ). V roce 1986, po přestěhování na univerzitu v Nijmegenu, zorganizoval skupinu zabývající se formalizací matematiky, ideologicky navazující na práci, která byla prováděna v rámci projektu Automath Nicholas de Bruyne . Ve druhé polovině 80. let studoval strojové verze λ-kalkulu, se zvláštní pozorností na vztahy mezi nimi; V roce 1991 navrhl λ-cube  , grafickou interpretaci osmi různých typů typovaného λ-kalkulu, který si získal oblibu jak mezi logiky, tak mezi specialisty na základy informatiky a programovacích jazyků .

Člen redakčních rad časopisů Information and Computation , Journal of Functional Programming , Journal of Logic and Computation , Logical Methods in Computer Science .

Ocenění a komunity

Člen Evropské akademie (1992). Akademik Královské nizozemské akademie věd (1997).

V roce 2002 mu byl udělen Řád nizozemského lva (rytíř řádu). Ve stejném roce obdržel Spinozovu cenu  , hlavní ocenění nizozemské vládní Organizace pro vědecký výzkum ( holandský.  Nederlandse Organisatie voor Wetenschappelijk Onderzoek ).

Bibliografie

• Henk Barendregt. Lambda kalkul. Jeho syntaxe a  sémantika . - Amsterdam: Severní Holandsko, 1981. - 622 s. — (Studie z logiky a základů matematiky, sv. 103). - ISBN 0-444-87508-5 .  — základní monografie o λ-kalkulu, dvakrát přetištěná (1984, 2012), přeložená do čínštiny (1990) a ruštiny (1985): Barendregt, Henk. Lambda kalkul. Jeho syntaxe a sémantika . — M .: Mir , 1985. — 606 s. - 4800 výtisků. (Ruština)
• Henk Barendregt, Wil Dekkers, Richard Statman. Lambda kalkul s typy  . - Cambridge : Cambridge University Press , 2010. - 703 s. - (Perspektivy v logice). — ISBN 9780521766142 .  - ucelená prezentace variant typovaného λ-kalkulu , různých rozšíření a aplikací, koncipovaná jako pokračování knihy „Lambda kalkul. Jeho syntaxe a sémantika“. Znovu vydáno v roce 2013.

Hlavní publikace

• Henk Barendregt. Kombinační logika a axiom výběru  (anglicky)  // Indagationes Mathematicae. - 1973. - Sv. 3 , ne. 76 . - S. 203-221 .
• Henk Barendregt. Globální reprezentace rekurzivních funkcí v λ-kalkulu  (anglicky)  // Theoretical Computer Science . - 1976. - Ne. 3.2 . - str. 225-242 .
• Barendregt H. Beztypový λ-kalkul // Referenční kniha o matematické logice. / Edited by J. Barwise. — M. : Nauka, 1983. — T. 4: Teorie důkazů. - S. 278-318.
• Henk Barendregt, Adrian Rezus. Sémantika pro klasický automat a související systémy  (anglicky)  // Information and Control . - 1983. - Sv. 59 . - S. 127-147 .
• Henk Barendregt. Lambda calculi s typy  (anglicky)  // S. Abramsky, Dov M. Gabbay a TSE Maibaum (editoři) Handbook of Logic in Computer Science. - Oxford : Oxford University Press , 1992. - Sv. 2: Pozadí: Výpočtové struktury . — S. 117–309 . — ISBN 0-19-853761-1 .  — publikace, kde byla poprvé představena λ-krychle.

Poznámky

1. ↑ http://www.cs.ru.nl/barendregt60/essays/preliminary/prelims.pdf
2. ↑ Henk Barendregt. Curriculum vitae  (anglicky) (25. září 2011). Získáno 9. března 2014. Archivováno z originálu 9. března 2014.
3. ↑ Benjamin Pierce. Typy v programovacích jazycích / Per. z angličtiny: G. Bronnikov, A. Ott. - Dobrosvet , 2011. - S. 76. - 656 s. — ISBN 978-5-7913-0082-9 .

Odkazy

• cs.ru.nl/~henk/ - oficiální stránky Fakulty základů matematiky a informatiky Univerzity v Nijmegenu - stránka Henka Barendregta

Tematické stránky	Matematická genealogie ORCID zbMATH Otevřeno
V bibliografických katalozích BNF : 12482070f GND : 124647219 GTAA : 214816 ISNI : 0000 0001 0932 8983 J9U : 987007522461705171 LCCN : n80086451 NKC : ntk2013782542 NTA : 071630848 NUKAT : n98036420 SUDOC : 034022821 VIAF : 109291023 WorldCat VIAF : 109291023