English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Michael Gordon was a pioneer in the field of interactive theorem proving andhardware verification. In the 1970s, he had the vision of formally verifyingsystem designs, proving their correctness using mathematics and logic. Hedemonstrated his ideas on real-world computer designs. His students extendedthe work to such diverse areas as the verification of floating-pointalgorithms, the verification of probabilistic algorithms and the verifiedtranslation of source code to correct machine code. He was elected to the RoyalSociety in 1994, and he continued to produce outstanding research untilretirement.  His achievements include his work at Edinburgh University helping to createEdinburgh LCF, the first interactive theorem prover of its kind, and the MLfamily of functional programming languages. He adopted higher-order logic as ageneral formalism for verification, showing that it could specify hardwaredesigns from the gate level right up to the processor level. It turned out tobe an ideal formalism for many problems in computer science and mathematics.His tools and techniques have exerted a huge influence across the field offormal verification.

Michael John Caldwell Gordon (FRS 1994), 28 February 1948 -- 22 August 2017