Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Британдық компьютерлік ғалым Майкл Джон Колдуэлл Гордон (28 ақпан 1948 – 22 тамыз 2017) – британдық компьютер ғалымы.
British computer scientist
Michael John Caldwell Gordon (28 February 1948 – 22 August 2017) was a British computer scientist.
Өмір
Майк Гордон Англияның Йоркшир графтығындағы Рипон қаласында дүниеге келген. Ол Дартингтон Холл мектебінде және Беделс мектебінде білім алған. 1966 жылы Кембридж университетінің Гонвилл және Каиус колледжінде инженерлік мамандықты оқуға қабылданды, бірақ математикаға ауысты. Оқу кезінде 1969 жылы жазғы демалысында Лондондағы Ұлттық физикалық зертханада жұмыс істеді, осылайша алғаш рет компьютермен танысты. Гордон Род Бурсталлдың жетекшілігімен Эдинбург университетінде докторлық диссертациясын 1973 жылы "Таза LISP бағдарламаларының бағалауы және мағынасын беруі" тақырыбында қорғады. LISP-тің авторы Джон Маккарти оны Калифорниядағы Стэнфорд университетіне шақырды, онда ол оның Жасанды интеллект зертханасында жұмыс істеді. Гордон 1981 жылдан бастап Кембридж университетінің Компьютерлік зертханасында жұмыс істеді, бастапқыда лектор болып, 1988 жылы оқырман, ал 1996 жылы профессор атағын алды. 1994 жылы Корольдік қоғамның мүшесі болып сайланды, ал 2008 жылы оның 60 жылдығына арналған жүйелік инфрақұрылымды тексеру құралдары мен әдістері тақырыбында екі күндік ғылыми конференция өткізілді. Майк Гордон Эдинбург университетінде Робин Милнердің докторанты Авра Конға үйленді және олар бірлесіп зерттеу жұмыстарын жүргізді.
Mike Gordon was born in Ripon, Yorkshire, England. He attended Dartington Hall School and Bedales School. In 1966, he was accepted to study engineering at Gonville and Caius College, University of Cambridge, but transferred to mathematics. During his studies, in 1969 he worked at the National Physical Laboratory in London during the summer, gaining his first exposure to computers. Gordon studied for his PhD degree at University of Edinburgh, supervised by Rod Burstall, finishing in 1973 with a thesis entitled Evaluation and Denotation of Pure LISP Programs. He was invited to Stanford University in California by John McCarthy, the inventor of LISP, to work in his Artificial Intelligence Laboratory there. Gordon worked at the Cambridge University Computer Laboratory from 1981, initially as a lecturer, promoted to Reader in 1988 and Professor in 1996. He was elected a Fellow of the Royal Society in 1994, and in 2008 a two day research meeting on Tools and Techniques for Verification of System Infrastructure was held there in honour of his 60th birthday. Mike Gordon was married to Avra Cohn, a PhD student of Robin Milner at the University of Edinburgh, and they undertook research together.
Жұмыс
Гордон HOL теоремасын әзірлеуге жетекшілік етті. HOL жүйесі – жоғары тәртіп логикасында интерактивті теоремаларды дәлелдеу ортасы. Оның ең ерекше қасиеті – мета-тіл ML арқылы жоғары бағдарламалану мүмкіндігі. Жүйенің қолданылу саласы кең: таза математиканы формалдаудан бастап, өнеркәсіптік аппаратты тексеруге дейін. HOL жүйесі бойынша халықаралық конференциялар сериясы өткізілді, олар TPHOLs деп аталады. Алғашқы үш конференция ресми емес пайдаланушылар жиыны болды және олардың материалдары жарияланбады. Қазіргі дәстүр бойынша жыл сайынғы конференция өткен жиынның орнынан басқа континентте өтеді. 1996 жылдан бастап, жоғары тәртіп логикасындағы теоремаларды дәлелдеудің барлық түрлерін қамтитын аясы кеңейтілді.
Gordon led the development of the HOL theorem prover. The HOL system is an environment for interactive theorem proving in a higher order logic. Its most outstanding feature is its high degree of programmability through the meta language ML. The system has a wide variety of uses, from formalising pure mathematics to verification of industrial hardware. There has been a series of international conferences on the HOL system, TPHOLs. The first three were informal users' meetings with no published proceedings. The tradition now is for an annual conference in a continent different from the location of the previous meeting. From 1996, the scope broadened to cover all theorem proving in higher order logics.