BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Harrison:John

Contributed to:

POPL 20112011
CAV 20082008
CADE 20072007
ECDL 20072007
IJCAR 20062006
SFM 20062006
CADE 20052005
FM 20052005
LICS 20032003
CADE 20002000
CADE 19961996

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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.