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:
2011
2008
2007
2007
2006
20062005
2005
200320001996Wrote 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.