Disclaimer: All content has been generated automatically by a program running on the titles of publications extracted from people's webpages. Click here for details. ©2007 Advaith Siddharthan
 
Joe Hurd
 

Research

(Analysis last run in January 2008)

2005--2007: 'encryption algorithms'; 'functional correctness proofs'; 'proof pearl'; 'termination analysis'; 'embedding cryptol'; 'elliptic curve cryptography'; 'ARM verification'; 'probabilistic guarded commands'; 'chess endgame data assurance';

2000--2004: 'theorem prover'; 'theorem proving'; 'higher order logic'; 'formal verification'; 'native code'; 'probabilistic algorithms'; 'probabilistic termination'; 'miller-rabin probabilistic primality test'; 'predicate sets'; 'logic variables'; 'HOL theorem prover'; 'polytypism in theorem proving'; 'formal approach'; 'compiling HOL4'; 'lcf-style interface'; 'first-order proof tactics'; 'formal semantics'; 'fast normalisation'; 'congruence classes';

Related People
  • Mike Gordon [ TSG ][ ARG ]:
    • 'ARM verification'; 'automatic formal synthesis'; 'elliptic curve cryptography'; 'higher order logic'; 'theorem proving';
  • Larry Paulson [ Security ][ TSG ][ ARG ]:
    • 'formal verification'; 'interactive theorem proving'; 'proof pearl'; 'reflection theorem';
  • Anthony Fox [ ARG ]:
    • 'ARM verification'; 'HOL specification'; 'elliptic curve cryptography'; 'formal specification'; 'formal verification';
  • Scott Owens [ TSG ]:
    • 'automatic formal synthesis'; 'encryption algorithms'; 'higher order logic';
  • K Sparck Jones [ NLIP ]:
    • 'formal theories'; 'probabilistic models'; 'semantic web';
  • Mateja Jamnik [ AI ][ ARG ]:
    • 'proof planning'; 'theorem proving';
  • Hasan Amjad [ ARG ]:
    • 'theorem prover'; 'theorem proving';