`Travelled to:`

1 × Canada

1 × Estonia

1 × Germany

1 × Italy

1 × United Kingdom

5 × USA

`Collaborated with:`

∅ S.McLaughlin F.Corubolo P.B.Watry A.D.Gordon R.Harper A.Jeffrey P.Sewell

`Talks about:`

verif (7) theorem (3) prove (3) proof (3) use (3) formal (2) point (2) float (2) elementari (1) distribut (1)

## Person: John Harrison

### DBLP: Harrison:John

### Contributed to:

### Wrote 11 papers:

- POPL-2011-GordonHHJS #concurrent #verification
- Robin Milner 1934--2010: verification, languages, and concurrency (ADG, RH, JH, AJ, PS), pp. 473–474.
- CAV-2008-Harrison #proving #theorem proving #verification
- Theorem Proving for Verification (JH), pp. 11–18.
- CADE-2007-Harrison #automation #proving #using
- Automating Elementary Number-Theoretic Proofs Using Gröbner Bases (JH), pp. 51–66.
- ECDL-2007-CoruboloWH #collaboration #distributed #independence #research
- Location and Format Independent Distributed Annotations for Collaborative Research (FC, PBW, JH), pp. 495–498.
- IJCAR-2006-Harrison #self #towards
- Towards Self-verification of HOL Light (JH), pp. 177–191.
- SFM-2006-Harrison #float #proving #theorem proving #using #verification
- Floating-Point Verification Using Theorem Proving (JH), pp. 211–242.
- CADE-2005-McLaughlinH
- A Proof-Producing Decision Procedure for Real Arithmetic (SM, JH), pp. 295–314.
- FM-2005-Harrison #float #verification
- Floating-Point Verification (JH), pp. 529–532.
- LICS-2003-Harrison #verification
- Formal Verification at Intel (JH), p. 45–?.
- CADE-2000-Harrison #proving #theorem proving #using #verification
- High-Level Verification Using Theorem Proving and Formalized Mathematics (JH), pp. 1–6.
- CADE-1996-Harrison #optimisation #proving
- Optimizing Proof Search in Model Elimination (JH), pp. 313–327.