Barendregt, Henk

Henk Barendregt ( Hendrik Pieter Barendregt , Niderl.  Hendrik Pieter Barendregt ; født 18. december 1947 ) er en hollandsk matematiker og logiker , forsker i λ-regning og typeteori , forfatter til λ-kuben . Professor, leder af Institut for Grundlag for Matematik og Informatik ved Universitetet i Nijmegen .

Biografi

Født i 1947 i Amsterdam . I 1952-1965 studerede han på uddannelsesinstitutioner ved hjælp af Montessori-systemet . I 1967 dimitterede han fra universitetet i Utrecht med en grad i matematisk logik og en kandidatgrad. I 1971 forsvarede han under vejledning af Dirk van Dalen ( hollandsk.  Dirk van Dalen ) og Georg Kreisel ( tysk:  Georg Kreisel ) sin doktorafhandling ( Ph.D. ) om ekstensionelle modeller af λ-regning og kombinatorisk logik .

Efter at have forsvaret sin afhandling arbejdede han som forsker ved Stanford University i 1971-1972 . Fra 1972 til 1986 havde han professorater ved universitetet i Utrecht . Siden 1986 - Professor ved Universitetet i Nijmegen , leder af Institut for Matematik og Informatik. På forskellige tidspunkter arbejdede han i inviterede stillinger ved Darmstadt University of Technology , ETH Zürich , Carnegie Mellon University , Kyoto University , Siena University .

Han er glad for buddhisme og meditation , udgiver artikler om meditation i psykologiske og populærvidenskabelige magasiner [2] .

Videnskabeligt og redaktionelt arbejde

Resultater fra begyndelsen af ​​1970'erne er på normale former i λ-regning og realiserbarhed i kombinatorisk logik . Værkerne i anden halvdel af 1970'erne er afsat til spørgsmål om modeller af λ-regningen. Han opnåede berømmelse i 1981 efter udgivelsen af ​​monografien "Lambda Calculus. Dens syntaks og semantik”, som to gange blev genoptrykt og oversat til russisk og kinesisk og noteret som et grundlæggende værk om den utyperede λ-regning [3] .

I 1980'erne studerede han spørgsmål om automatisk bevis og forholdet mellem matematisk bevis og λ-regning og typeteori (efterfølgende konceptualiseret som Curry-Howard isomorfisme ). I 1986, efter at have flyttet til universitetet i Nijmegen, organiserede han en gruppe, der beskæftiger sig med formalisering af matematik, og fortsatte ideologisk det arbejde, der blev udført inden for rammerne af Automath- projektet Nicholas de Bruyne . I anden halvdel af 1980'erne studerede han maskinskrevne versioner af λ-regningen med særlig opmærksomhed på forholdet mellem dem; I 1991 foreslog han λ-kuben  , en grafisk fortolkning af otte forskellige typer af maskinskrevne λ-regning, som vandt popularitet både blandt logikere og blandt specialister i grundlaget for datalogi og programmeringssprog .

Medlem af redaktionen for tidsskrifterne Information and Computation , Journal of Functional Programming , Journal of Logic and Computation , Logical Methods in Computer Science .

Priser og fællesskaber

Medlem af Det Europæiske Akademi (1992). Akademiker ved Royal Netherlands Academy of Sciences (1997).

I 2002 blev han tildelt Order of the Netherlands Lion (Ridder af Ordenen). Samme år modtog han Spinoza-prisen  , en stor pris fra den hollandske regerings Organisation for Scientific Research ( hollandsk.  Nederlandse Organisatie voor Wetenschappelijk Onderzoek ).

Bibliografi

• Henk Barendregt. Lambdaregningen. Dens syntaks og  semantik . - Amsterdam: Nordholland, 1981. - 622 s. — (Studies in Logic and the Foundations of Mathematics, bd. 103). - ISBN 0-444-87508-5 .  — grundlæggende monografi om λ-regning, genoptrykt to gange (1984, 2012), oversat til kinesisk (1990) og russisk (1985): Barendregt, Henk. Lambdaregning. Dens syntaks og semantik . — M .: Mir , 1985. — 606 s. - 4800 eksemplarer. (Russisk)
• Henk Barendregt, Wil Dekkers, Richard Statman. Lambdaregning med typer  . - Cambridge : Cambridge University Press , 2010. - 703 s. - (Perspektiver i logik). — ISBN 9780521766142 .  - en omfattende præsentation af varianter af den maskinskrevne λ-regning , forskellige udvidelser og anvendelser, udtænkt som en fortsættelse af bogen "Lambda Calculus. Dens syntaks og semantik". Genudgivet i 2013.

Større publikationer

• Henk Barendregt. Kombinationslogik og  valgaksiomet (engelsk)  // Indagationes Mathematicae. - 1973. - Bd. 3 , nr. 76 . - S. 203-221 .
• Henk Barendregt. En global repræsentation af de rekursive funktioner i λ-regningen  (engelsk)  // Theoretical Computer Science . - 1976. - Nej. 3.2 . - S. 225-242 .
• Barendregt H. Typeløs λ-regning // Opslagsbog om matematisk logik. / Redigeret af J. Barwise. — M. : Nauka, 1983. — T. 4: Theory of Proofs. - S. 278-318.
• Henk Barendregt, Adrian Rezus. Semantik for klassisk automatik og relaterede systemer  (engelsk)  // Information and Control . - 1983. - Bd. 59 . - S. 127-147 .
• Henk Barendregt. Lambdaregning med typer  (engelsk)  // S. Abramsky, Dov M. Gabbay og TSE Maibaum (redaktører) Handbook of Logic in Computer Science. - Oxford : Oxford University Press , 1992. - Vol. 2: Baggrund: Beregningsstrukturer . — S. 117–309 . — ISBN 0-19-853761-1 .  — publikationen, hvor λ-terningen blev introduceret for første gang.

Noter

1. ↑ http://www.cs.ru.nl/barendregt60/essays/preliminary/prelims.pdf
2. ↑ Henk Barendregt. Curriculum vitae  (engelsk) (25. september 2011). Hentet 9. marts 2014. Arkiveret fra originalen 9. marts 2014.
3. ↑ Benjamin Pierce. Typer i programmeringssprog / Pr. fra engelsk: G. Bronnikov, A. Ott. - Dobrosvet , 2011. - S. 76. - 656 s. — ISBN 978-5-7913-0082-9 .

Links

• cs.ru.nl/~henk/ - officiel hjemmeside for Faculty of Foundations of Mathematics and Informatics ved University of Nijmegen - side af Henk Barendregt

Tematiske steder	Matematisk genealogi ORCID zbMATH Åbn
I bibliografiske kataloger 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