Barendregt, Henk

Henk Barendregt ( Hendrik Pieter Barendregt , Niderl .  Hendrik Pieter Barendregt ; syntynyt 18. joulukuuta 1947 ) on hollantilainen matemaatikko ja loogikko , λ - laskun ja tyyppiteorian tutkija , λ - kuution kirjoittaja . Professori, matematiikan ja informatiikan perusteiden osaston johtaja Nijmegenin yliopistossa .

Elämäkerta

Syntynyt vuonna 1947 Amsterdamissa . Vuosina 1952-1965 hän opiskeli Montessori-järjestelmää käyttävissä oppilaitoksissa . Vuonna 1967 hän valmistui Utrechtin yliopistosta matemaattisen logiikan tutkinnon ja maisterin tutkinnon. Vuonna 1971 hän puolusti Dirk van Dalenin ( hollantilainen  Dirk van Dalen ) ja Georg Kreiselin ( saksa:  Georg Kreisel ) ohjauksessa tohtorin väitöskirjaansa λ-laskennan ja kombinatorisen logiikan laajennettavista malleista .

Väitöskirjansa puolustamisen jälkeen hän työskenteli tutkijana Stanfordin yliopistossa vuosina 1971-1972 . Vuosina 1972-1986 hän toimi professorina Utrechtin yliopistossa . Vuodesta 1986 - professori Nijmegenin yliopistossa , matematiikan ja informatiikan perusteiden osaston johtaja. Eri aikoina hän työskenteli kutsutehtävissä Darmstadtin teknillisessä yliopistossa , ETH Zürichissä , Carnegie Mellonin yliopistossa , Kioton yliopistossa ja Sienan yliopistossa .

Hän pitää buddhalaisuudesta ja meditaatiosta , julkaisee meditaatiosta artikkeleita psykologisissa ja populaaritieteellisissä aikakauslehdissä [2] .

Tieteellinen ja toimituksellinen työ

Tulokset 1970-luvun alusta ovat λ-laskennan normaalimuodoista ja kombinatorisen logiikan toteutettavuudesta . 1970-luvun toisen puoliskon teokset ovat omistettu λ-laskennan mallien kysymyksiin. Hän saavutti mainetta vuonna 1981 julkaistuaan monografian "Lambda Calculus. Sen syntaksi ja semantiikka”, joka painettiin kahdesti uudelleen ja käännettiin venäjäksi ja kiinaksi ja joka mainittiin perusteokseksi kirjoittamattomasta λ-laskusta [3] .

1980-luvulla hän opiskeli kysymyksiä automaattisesta todistuksesta ja matemaattisen todistuksen suhdetta λ-laskennasta ja tyyppiteoriasta (myöhemmin käsitteellistettiin Curry-Howard-isomorfismiksi ). Vuonna 1986 Nijmegenin yliopistoon siirtymisen jälkeen hän järjesti ryhmän, joka käsittelee matematiikan formalisointia, ideologisesti jatkaen Automath- projektin Nicholas de Bruyne puitteissa tehtyä työtä . 1980-luvun jälkipuoliskolla hän opiskeli λ-laskennan kirjoitettuja versioita kiinnittäen erityistä huomiota niiden välisiin suhteisiin; Vuonna 1991 hän ehdotti λ-kuutiota  , graafista tulkintaa kahdeksasta eri tyyppisestä λ-laskusta, joka saavutti suosiota sekä logiikkojen että tietojenkäsittelytieteen ja ohjelmointikielten perusteiden asiantuntijoiden keskuudessa .

Toimituslautakuntien jäsen lehdissä Information and Computation , Journal of Functional Programming , Journal of Logic and Computation , Logical Methods in Computer Science .

Palkinnot ja yhteisöt

Euroopan Akatemian jäsen ( 1992). Alankomaiden kuninkaallisen tiedeakatemian akateemikko ( 1997).

Vuonna 2002 hänelle myönnettiin Alankomaiden leijonan ritari (ritarikunnan ritari). Samana vuonna hän sai Spinoza-palkinnon  , tärkeän palkinnon Alankomaiden hallituksen tieteelliseltä tutkimusorganisaatiolta ( hollanti.  Nederlandse Organisatie voor Wetenschappelijk Onderzoek ).

Bibliografia

• Henk Barendregt. Lambda-laskenta. Sen syntaksi ja  semantiikka . - Amsterdam: Pohjois-Hollanti, 1981. - 622 s. — (Studies in Logic and the Foundations of Mathematics, osa 103). - ISBN 0-444-87508-5 .  — perusmonografia λ-laskusta, uusintapainos kahdesti (1984, 2012), käännetty kiinan (1990) ja venäjän (1985) kielille: Barendregt, Henk. Lambda-laskenta. Sen syntaksi ja semantiikka . — M .: Mir , 1985. — 606 s. - 4800 kappaletta. (Venäjän kieli)
• Henk Barendregt, Wil Dekkers, Richard Statman. Lambda -laskenta tyypeillä  . - Cambridge : Cambridge University Press , 2010. - 703 s. - (Logiikan näkökulmat). — ISBN 9780521766142 .  - kattava esitys kirjoitetun λ-laskennan muunnelmista , erilaisista laajennuksista ja sovelluksista, jotka on suunniteltu jatkoksi kirjalle “Lambda Calculus. Sen syntaksi ja semantiikka". Uusittu vuonna 2013.

Tärkeimmät julkaisut

• Henk Barendregt. Kombinatorinen logiikka ja valinnan aksiooma  (englanniksi)  // Indagationes Mathematicae. - 1973. - Voi. 3 , ei. 76 . - s. 203-221 .
• Henk Barendregt. Globaali esitys rekursiivisista funktioista λ-laskennassa  (englanniksi)  // Theoretical Computer Science . - 1976. - Ei. 3.2 _ - s. 225-242 .
• Barendregt H. Typeless λ-calculus // Matemaattisen logiikan hakuteos. / Toimittanut J. Barwise. — M .: Nauka, 1983. — T. 4: Todistusteoria. - S. 278-318.
• Henk Barendregt, Adrian Rezus. Semantics for Classical Automath ja siihen liittyvät järjestelmät  (englanniksi)  // Information and Control . - 1983. - Voi. 59 . - s. 127-147 .
• Henk Barendregt. Lambdalaskimet tyypeillä  (englanniksi)  // S. Abramsky, Dov M. Gabbay ja TSE Maibaum (toimittajat) Handbook of Logic in Computer Science. - Oxford : Oxford University Press , 1992. - Voi. 2: Taustaa: Laskennalliset rakenteet . — s. 117–309 . — ISBN 0-19-853761-1 .  — julkaisu, jossa λ-kuutio esiteltiin ensimmäistä kertaa.

Muistiinpanot

1. ↑ http://www.cs.ru.nl/barendregt60/essays/preliminary/prelims.pdf
2. ↑ Henk Barendregt. Curriculum vitae  (englanniksi) (25. syyskuuta 2011). Haettu 9. maaliskuuta 2014. Arkistoitu alkuperäisestä 9. maaliskuuta 2014.
3. ↑ Benjamin Pierce. Tyypit ohjelmointikielillä / Per. englannista: G. Bronnikov, A. Ott. - Dobrosvet , 2011. - S. 76. - 656 s. — ISBN 978-5-7913-0082-9 .

Linkit

• cs.ru.nl/~henk/ - Nijmegenin yliopiston matematiikan ja informatiikan perusteiden tiedekunnan virallinen verkkosivusto - Henk Barendregtin sivu

Temaattiset sivustot	Matemaattinen sukututkimus ORCID zbMATH Avoinna
Bibliografisissa luetteloissa 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