The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.

A mizar mode for HOL

Authors	John Harrison
Editors
Type	misc
Year	1996
Citekey	`harrison1996mizar`

Published in	Lecture notes in computer science
Publisher	Springer Science+Business Media
Pages	203--220

DOI	10.1007/bfb0105406
OpenAlex	W1488189293

Landing page	https://doi.org/10.1007/bfb0105406

How it got here	agent via openalex
Added	2026-10-24 12:29 UTC
Not denied by	a person 2026-10-29 17:12 UTC

lncs what-one-proves-with

@misc{harrison1996mizar,
  title        = {A mizar mode for HOL},
  author       = {John Harrison},
  year         = {1996},
  journal      = {Lecture notes in computer science},
  publisher    = {Springer Science+Business Media},
  pages        = {203--220},
  doi          = {10.1007/bfb0105406},
}

This record lives at https://refs.drheap.org/harrison1996mizar/ and will keep doing so.

A mizar mode for HOL

The work

Where it appeared

Identifiers

Access

How it got here

Filed under

Cite it as