33:
342:
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
1034:
1024:
1004:
705:
515:
1009:
232:
386:
408:
275:
999:
628:
279:
1029:
220:
88:
1014:
688:
267:
426:
339:. The system has a wide variety of uses, from formalising pure mathematics to verification of industrial hardware.
1019:
771:
890:
379:"Michael JC Gordon FRS, Professor Emeritus of Computer Assisted Reasoning, 28 February 1948 – 22 August 2017"
363:
697:
417:
294:
179:
994:
885:
821:
413:"Michael JC Gordon FRS, Professor of Computer Assisted Reasoning (28 February 1948 – 22 August 2017)"
336:
500:
915:
875:
724:
632:
309:
247:
224:
133:
92:
520:
853:
681:
666:
335:. Its most outstanding feature is its high degree of programmability through the meta-language
283:
208:
456:(11 June 2018). "Michael John Caldwell Gordon (FRS 1994), 28 February 1948 – 22 August 2017".
865:
776:
513:
Paulson, Lawrence C (2018). "Michael John
Caldwell Gordon. 28 February 1948—22 August 2017".
487:
636:
989:
984:
943:
556:
8:
754:
259:
129:
475:
457:
332:
324:
184:
102:
948:
786:
744:
739:
674:
315:
He died in
Cambridge after a brief illness and is survived by his wife and two sons.
479:
938:
905:
806:
791:
766:
610:
467:
453:
430:
378:
158:
119:
895:
836:
826:
328:
614:
589:
146:
910:
870:
796:
749:
585:
212:
435:
412:
147:
Evaluation and denotation of pure LISP programs: a worked example in semantics
978:
953:
816:
734:
701:
629:"TPHOLS, conferences associated with theorem proving in higher-order logics"
359:
963:
880:
811:
719:
471:
407:
305:
251:
163:
32:
921:
859:
847:
760:
958:
841:
831:
729:
564:
228:
216:
900:
781:
597:
263:
243:
661:
534:
287:
200:
76:
57:
606:
462:
204:
696:
535:"Tools and Techniques for Verification of System Infrastructure"
1035:
Scientists of the
National Physical Laboratory (United Kingdom)
236:
140:
299:
Tools and
Techniques for Verification of System Infrastructure
196:
53:
239:
during the summer, gaining his first exposure to computers.
271:
1025:
Members of the
University of Cambridge Computer Laboratory
590:"In Memoriam: A tribute to five formal methods colleagues"
304:
Mike Gordon was married to Avra Cohn, a PhD student of
343:
to cover all theorem proving in higher-order logics.
516:
Biographical
Memoirs of Fellows of the Royal Society
327:. The HOL system is an environment for interactive
297:in 1994, and in 2008 a two-day research meeting on
183:(28 February 1948 – 22 August 2017) was a British
976:
282:from 1981, initially as a lecturer, promoted to
1005:Alumni of Gonville and Caius College, Cambridge
301:was held there in honour of his 60th birthday.
256:Evaluation and Denotation of Pure LISP Programs
231:. During his studies, in 1969 he worked at the
682:
373:
371:
387:Computer Laboratory, University of Cambridge
448:
446:
409:University of Cambridge Computer Laboratory
401:
254:, finishing in 1973 with a thesis entitled
689:
675:
368:
461:
434:
443:
312:, and they undertook research together.
280:Cambridge University Computer Laboratory
554:
548:
452:
977:
578:
1010:Alumni of the University of Edinburgh
670:
584:
89:Gonville and Caius College, Cambridge
215:. In 1966, he was accepted to study
13:
323:Gordon led the development of the
276:Artificial Intelligence Laboratory
14:
1046:
1000:People educated at Bedales School
655:
427:Springer International Publishing
557:"Sad news regarding Mike Gordon"
555:Kalvala, Sara (22 August 2017).
31:
621:
527:
521:doi.org/10.1098/rsbm.2018.0019
507:
353:
1:
364:Mathematics Genealogy Project
346:
1030:Fellows of the Royal Society
278:there. Gordon worked at the
233:National Physical Laboratory
176:Michael John Caldwell Gordon
7:
1015:English computer scientists
949:Isaak Markovich Khalatnikov
615:10.13140/RG.2.2.13481.62560
418:Formal Aspects of Computing
295:Fellow of the Royal Society
10:
1051:
561:HOL theorem-proving system
221:Gonville and Caius College
16:British computer scientist
931:
712:
436:10.1007/s00165-017-0438-y
169:
157:
139:
125:
115:
108:
98:
84:
65:
39:
30:
23:
195:Mike Gordon was born in
761:Henry Marshall Charlton
633:University of Cambridge
318:
310:University of Edinburgh
248:University of Edinburgh
242:Gordon studied for his
225:University of Cambridge
190:
134:University of Cambridge
93:University of Edinburgh
495:Cite journal requires
472:10.1098/rsbm.2018.0019
209:Dartington Hall School
1020:Formal methods people
922:James Gordon Williams
866:Andrew Clennel Palmer
777:Nicholas Barry Davies
662:Mike Gordon home page
227:, but transferred to
944:Friedrich Hirzebruch
802:Michael J. C. Gordon
454:Paulson, Lawrence C.
360:Michael J. C. Gordon
258:. He was invited to
25:Michael J. C. Gordon
848:Robert Michael Moor
755:Anthony Butterworth
411:(27 October 2017).
260:Stanford University
130:Stanford University
860:John Forster Nixon
586:Bowen, Jonathan P.
333:higher-order logic
325:HOL theorem prover
270:, the inventor of
185:computer scientist
103:HOL theorem prover
995:People from Ripon
972:
971:
891:David Sherrington
787:George Efstathiou
745:Geoffrey Boxshall
740:Richard Borcherds
293:He was elected a
274:, to work in his
173:
172:
110:Scientific career
1042:
939:F. Albert Cotton
906:Richard Treisman
807:Dennis Greenland
792:John Edwin Field
767:Anthony Cheetham
691:
684:
677:
668:
667:
649:
648:
646:
644:
635:. Archived from
625:
619:
618:
594:
582:
576:
575:
573:
571:
552:
546:
545:
543:
541:
531:
525:
511:
505:
504:
498:
493:
491:
483:
465:
450:
441:
440:
438:
405:
399:
398:
396:
394:
375:
366:
357:
250:, supervised by
182:
159:Doctoral advisor
153:
120:Computer Science
72:
50:28 February 1948
49:
47:
35:
21:
20:
1050:
1049:
1045:
1044:
1043:
1041:
1040:
1039:
975:
974:
973:
968:
927:
896:Fraser Stoddart
837:Peter McCullagh
827:David MacLennan
708:
695:
658:
653:
652:
642:
640:
627:
626:
622:
592:
583:
579:
569:
567:
553:
549:
539:
537:
533:
532:
528:
524:
512:
508:
496:
494:
485:
484:
451:
444:
406:
402:
392:
390:
377:
376:
369:
358:
354:
349:
329:theorem proving
321:
193:
178:
151:
132:
91:
85:Alma mater
80:
74:
70:
61:
51:
45:
43:
26:
17:
12:
11:
5:
1048:
1038:
1037:
1032:
1027:
1022:
1017:
1012:
1007:
1002:
997:
992:
987:
970:
969:
967:
966:
961:
956:
951:
946:
941:
935:
933:
929:
928:
926:
925:
918:
913:
911:Scott Tremaine
908:
903:
898:
893:
888:
886:Derek Robinson
883:
878:
873:
871:David Pettifor
868:
863:
856:
851:
844:
839:
834:
829:
824:
822:Andrew Lumsden
819:
814:
809:
804:
799:
797:Graham Fleming
794:
789:
784:
779:
774:
769:
764:
757:
752:
750:Jeremy Brockes
747:
742:
737:
732:
727:
722:
716:
714:
710:
709:
694:
693:
686:
679:
671:
665:
664:
657:
656:External links
654:
651:
650:
620:
577:
547:
526:
506:
497:|journal=
442:
400:
367:
351:
350:
348:
345:
320:
317:
213:Bedales School
207:. He attended
192:
189:
171:
170:
167:
166:
161:
155:
154:
143:
137:
136:
127:
123:
122:
117:
113:
112:
106:
105:
100:
99:Known for
96:
95:
86:
82:
81:
75:
73:(aged 69)
69:22 August 2017
67:
63:
62:
52:
41:
37:
36:
28:
27:
24:
15:
9:
6:
4:
3:
2:
1047:
1036:
1033:
1031:
1028:
1026:
1023:
1021:
1018:
1016:
1013:
1011:
1008:
1006:
1003:
1001:
998:
996:
993:
991:
988:
986:
983:
982:
980:
965:
962:
960:
957:
955:
954:Hugh McDevitt
952:
950:
947:
945:
942:
940:
937:
936:
934:
930:
924:
923:
919:
917:
914:
912:
909:
907:
904:
902:
899:
897:
894:
892:
889:
887:
884:
882:
879:
877:
874:
872:
869:
867:
864:
862:
861:
857:
855:
852:
850:
849:
845:
843:
840:
838:
835:
833:
830:
828:
825:
823:
820:
818:
817:Brian Launder
815:
813:
810:
808:
805:
803:
800:
798:
795:
793:
790:
788:
785:
783:
780:
778:
775:
773:
772:Julian Davies
770:
768:
765:
763:
762:
758:
756:
753:
751:
748:
746:
743:
741:
738:
736:
735:Timothy Bliss
733:
731:
728:
726:
725:Raymond Baker
723:
721:
718:
717:
715:
711:
707:
703:
702:Royal Society
699:
692:
687:
685:
680:
678:
673:
672:
669:
663:
660:
659:
639:on 7 May 2008
638:
634:
630:
624:
616:
612:
608:
604:
600:
599:
591:
588:(June 2020).
587:
581:
566:
562:
558:
551:
536:
530:
522:
518:
517:
510:
502:
489:
481:
477:
473:
469:
464:
459:
455:
449:
447:
437:
432:
428:
424:
420:
419:
414:
410:
404:
388:
384:
380:
374:
372:
365:
361:
356:
352:
344:
340:
338:
334:
330:
326:
316:
313:
311:
307:
302:
300:
296:
291:
289:
285:
281:
277:
273:
269:
268:John McCarthy
265:
261:
257:
253:
249:
245:
240:
238:
234:
230:
226:
222:
218:
214:
210:
206:
202:
198:
188:
186:
181:
177:
168:
165:
162:
160:
156:
149:
148:
144:
142:
138:
135:
131:
128:
124:
121:
118:
114:
111:
107:
104:
101:
97:
94:
90:
87:
83:
78:
68:
64:
59:
55:
42:
38:
34:
29:
22:
19:
964:Bert Sakmann
920:
881:Brian Ridley
858:
854:Peter Morris
846:
812:Kurt Lambeck
801:
759:
720:David Aldous
641:. Retrieved
637:the original
623:
602:
596:
580:
568:. Retrieved
560:
550:
538:. Retrieved
529:
514:
509:
488:cite journal
422:
416:
403:
391:. Retrieved
382:
355:
341:
322:
314:
306:Robin Milner
303:
298:
292:
286:in 1988 and
255:
252:Rod Burstall
241:
194:
175:
174:
164:Rod Burstall
145:
126:Institutions
109:
71:(2017-08-22)
18:
990:2017 deaths
985:1948 births
959:Erwin Neher
876:Tony Pawson
842:Dusa McDuff
832:Tak Wah Mak
730:Nick Barton
570:2 September
565:SourceForge
393:2 September
229:mathematics
217:engineering
979:Categories
901:John Tooze
782:Guy Dodson
643:28 January
598:FACS FACTS
540:14 January
463:1806.04002
383:Obituaries
347:References
264:California
244:PhD degree
46:1948-02-28
916:Bob White
609:: 13–29.
290:in 1996.
288:Professor
201:Yorkshire
79:, England
77:Cambridge
60:, England
58:Yorkshire
704:elected
607:BCS-FACS
480:47017843
932:Foreign
713:Fellows
706:in 1994
700:of the
698:Fellows
429:: 933.
362:at the
308:at the
205:England
631:. UK:
478:
389:. 2017
385:. UK:
284:Reader
237:London
152:(1973)
150:
141:Thesis
116:Fields
605:(1).
593:(PDF)
476:S2CID
458:arXiv
425:(6).
331:in a
197:Ripon
54:Ripon
645:2014
603:2020
572:2017
542:2023
501:help
395:2017
319:Work
272:LISP
211:and
191:Life
66:Died
40:Born
611:doi
468:doi
431:doi
266:by
262:in
246:at
235:in
219:at
180:FRS
981::
601:.
595:.
563:.
559:.
523:.
519:.
492::
490:}}
486:{{
474:.
466:.
445:^
423:29
421:.
415:.
381:.
370:^
337:ML
223:,
203:,
199:,
187:.
56:,
690:e
683:t
676:v
647:.
617:.
613::
574:.
544:.
503:)
499:(
482:.
470::
460::
439:.
433::
397:.
48:)
44:(
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
