마이클 J. C. 고든

Michael J. C. Gordon
마이클 J. C. 고든
ProfessorMichaelJCGordon.jpg
태어난(1948-02-28)28 1948년 2월
죽은2017년 8월 22일 (2017-08-22) (69)
국적영국의
시민권영국
모교케임브리지 곤빌 카이우스 칼리지
에든버러 대학교
로 알려져 있다.HOL 정리 프로베라
과학 경력
필드컴퓨터 사이언스
기관스탠퍼드 대학교
케임브리지 대학교
논문순수 LISP 프로그램의 평가 및 변위: 의미론적 사례 (1973)
박사학위 자문위원로드 버스타올[1]

마이클 콜드웰 고든 FRS(1948년 2월 28일 ~ 2017년 8월 22일)는 영국의 대표적인 컴퓨터 과학자였다.[2][3]

인생

마이크 고든은 영국 요크셔리폰에서 태어났다.[4]그는 다트링턴학교베데일스 학교에 다녔다.1966년 케임브리지 대학 곤빌과 카이우스 칼리지에서 공학을 공부하기 위해 합격했으나 수학으로 편입되었다.연구 기간 동안, 1969년에 그는 여름에 런던의 국립 물리 연구소에서 일했고, 컴퓨터에 처음으로 노출되었다.

고든은 로드 버스타가 감독하는 에든버러 대학에서 박사학위를 위해 공부했고 1973년에 '순수 LISP 프로그램의 평가와 평가 폄하'라는 논문으로 끝마쳤다.그는 LISP의 창시자인 존 매카시로부터 캘리포니아에 있는 스탠포드 대학에 초청되어 그곳에서 인공지능 연구소에서 일하게 되었다.고든은 1981년부터 케임브리지 대학 컴퓨터 연구소에서 강사로 일했으며, 처음에는 1988년에 리더로, 1996년에는 교수로 승진했다.

1994년 왕립학회 회원으로 선출되었으며,[5] 2008년에는 그의 60세 생일을 기념하여 이틀간 시스템 인프라 검증 도구와 기법에 관한 연구 회의가 그곳에서 열렸다.[6]

마이크 고든은 에든버러 대학로빈 밀너의 박사과정 학생인 Avra Cohn과 결혼하여 함께 연구에 착수했다.[4]

그는 잠시 병을 앓다가 케임브리지에서 사망했고 아내와 두 아들을 남겨 두고 있다.[2][7][8]

고든은 홀 정리 프로베론의 개발을 이끌었다.HOL 시스템은 보다 고차원의 논리로 증명할 수 있는 인터랙티브 정리 환경이다.메타언어 ML을 통한 프로그램화 가능성이 높다는 점이 가장 두드러진 특징이다. 순수수학 공식화부터 산업용 하드웨어 검증까지 다양한 활용도를 갖췄다.

HOL 시스템 TPHOLs에 관한 국제회의가 잇따라 열렸다.[9]처음 3개는 공개 절차가 없는 비공식 사용자 회의였다.현재 전통은 이전 회의 장소와는 다른 대륙에서 연례 회의를 하는 것이다.1996년부터는 범위가 확대되어 고차 로직으로 증명되는 모든 정리를 포괄하게 되었다.

참조

  1. ^ 수학 계보 프로젝트 마이클 J. C. 고든
  2. ^ a b "Michael JC Gordon FRS, Professor Emeritus of Computer Assisted Reasoning, 28 February 1948 – 22 August 2017". Obituaries. UK: Computer Laboratory, University of Cambridge. 2017. Retrieved 2 September 2017.
  3. ^ University of Cambridge Computer Laboratory (27 October 2017). "Michael JC Gordon FRS, Professor of Computer Assisted Reasoning (28 February 1948 – 22 August 2017)". Formal Aspects of Computing. Springer International Publishing. 29 (6): 933. doi:10.1007/s00165-017-0438-y.
  4. ^ a b Paulson, Lawrence C. (11 June 2018). "Michael John Caldwell Gordon (FRS 1994), 28 February 1948 – 22 August 2017". arXiv:1806.04002. doi:10.1098/rsbm.2018.0019. S2CID 47017843. {{cite journal}}:Cite 저널은 필요로 한다. journal=(도움말)
  5. ^ 폴슨, 로렌스 C(2018)."마이클 존 콜드웰 고든.1948년 2월 28일—2017년 8월 22일."왕립 학회동료들의 전기적 회고록. doi.org/10.1098/rsbm.2018.0019.
  6. ^ "Tools and Techniques for Verification of System Infrastructure". Retrieved 28 January 2014.
  7. ^ Kalvala, Sara (22 August 2017). "Sad news regarding Mike Gordon". HOL theorem-proving system. SourceForge. Retrieved 2 September 2017.
  8. ^ Bowen, Jonathan P. (June 2020). "In Memoriam: A tribute to five formal methods colleagues" (PDF). FACS FACTS. BCS-FACS. 2020 (1): 13–29. doi:10.13140/RG.2.2.13481.62560.
  9. ^ "TPHOLS, conferences associated with theorem proving in higher-order logics". UK: University of Cambridge. Archived from the original on 7 May 2008. Retrieved 28 January 2014.

외부 링크