hol-biblio.bib
@INPROCEEDINGS{TosuperHT,
AUTHOR = {M. Aagaard and M. E. Leeser and P. J. Windley},
TITLE = {Toward a Super Duper Hardware Tactic},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {399--412},
URL = {ftp://lal.cs.byu.edu/pub/HOL/lal-papers/superduper.ps.gz}
}
@INPROCEEDINGS{DomTheo,
AUTHOR = {S. Agerholm},
TITLE = {Domain Theory in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {295--310}
}
@TECHREPORT{FormMod,
AUTHOR = {S. Agerholm},
TITLE = {Formalising a Model of the lambda-calculus in {HOL}-ST},
NUMBER = {354},
INSTITUTION = {University of Cambridge Computer Laboratory},
YEAR = {1994}
}
@TECHREPORT{HOLReas,
AUTHOR = {S. Agerholm},
TITLE = {A {HOL} Basis for Reasoning about Functional Programs},
NUMBER = {BRICS Technical Report RS-94-44},
INSTITUTION = {Department of Computer Science, University of Aarhus},
MONTH = {December},
YEAR = {1994},
URL = {http://www.daimi.aau.dk:80/BRICS/RS/94/44/BRICS-RS-94-44/BRICS-RS-94-44.html}
}
@ARTICLE{LCFEx,
AUTHOR = {S.Agerholm},
TITLE = {{LCF} Examples in {HOL}},
JOURNAL = {The Computer Journal},
VOLUME = {38},
NUMBER = {2},
MONTH = {July},
YEAR = {1995},
PAGES = {121--130},
URL = {http://www.oup.co.uk/oup/smj/journals/ed/titles/computer_journal/docs/journal_contents/Volume_38_Number_2/38.2.ps/ager{HOL}m.ps}
}
@INPROCEEDINGS{LExinHol,
AUTHOR = {S.Agerholm},
TITLE = {{LCF} Examples in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {1--16}
}
@INPROCEEDINGS{MechProgVHOL,
AUTHOR = {S. Agerholm},
TITLE = {Mechanizing Program Verification in {HOL}},
BOOKTITLE = {Proceedings of the 1991 International Workshop on the {HOL} Theorem
Proving System and its Applications, {D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levitt and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {208--222}
}
@TECHREPORT{Mechprog,
AUTHOR = {S.Agerholm},
TITLE = {Mechanizing Program Verification in {HOL}},
NUMBER = {DAIMI Report Number IR-111},
INSTITUTION = {Department of Computer Science, University of Aarhus},
MONTH = {April},
YEAR = {1992}
}
@INPROCEEDINGS{NonprimRF,
AUTHOR = {S.Agerholm},
TITLE = {Non-primitive Recursive Function Definition},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah, {S}eptember 1995:
Proceedings},
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {17--31},
URL = {http://www.daimi.aau.dk:80/BRICS/RS/95/36/BRICS-RS-95-36/BRICS-RS-95-36.html}
}
@INPROCEEDINGS{CompHOLALF,
AUTHOR = {S.Agerholm and I. Beylin and P. Dybjer},
TITLE = {A Comparison of {HOL} and {ALF} Formalizations of a Categorical
Coherence Theorem},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International Conference,
{T}urku, {F}inland, {A}ugust 1996: Proceedings},
EDITOR = {J. von Wright and J. Grundy and J. Harrison},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1125},
PUBLISHER = {Springer-Verlag},
YEAR = {1996},
PAGES = {17--32}
}
@INPROCEEDINGS{ExperZF,
AUTHOR = {S. Agerholm and M. Gordon},
TITLE = {Experiments with {ZF} Set Theory in {HOL} and {I}sabelle},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah, {S}eptember 1995:
Proceedings},
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {32--45},
URL = {http://www.daimi.aau.dk:80/BRICS/RS/95/37/BRICS-RS-95-37/BRICS-RS-95-37.html}
}
@TECHREPORT{AutoMCFR,
AUTHOR = {S. Agerholm and H. Skj{\o}dt},
TITLE = {Automating A Model Checker For Recursive Modal Assertions In {HOL}},
NUMBER = {DAIMI Report Number IR-92},
INSTITUTION = {Department of Computer Science, University of Aarhus},
MONTH = {January},
YEAR = {1990}
}
@INPROCEEDINGS{Mechpi,
AUTHOR = {O. A{\"{\i}}t Mohamed},
TITLE = {Mechanizing a pi-calculus equivalence in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah, {S}eptember 1995:
Proceedings},
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {1--16}
}
@PHDTHESIS{Theopical,
AUTHOR = {O. A{\"{\i}}t Mohamed},
TITLE = {The theory of the pi-calcul in {HOL}},
SCHOOL = {Henri Poincare University},
MONTH = {July},
YEAR = {1996}
}
@PROCEEDINGS{HOL95Int,
EDITOR = {J. Alves-Foss},
TITLE = {{HOL}-95: International Workshop on Higher Order Logic Theorem
Proving and its Applications: {B}-Track: Short Presentations,
{A}spen {G}rove, {U}tah, {S}eptember, 1995},
YEAR = {1995},
URL = {http://lal.cs.byu.edu/lal/HOL95/Bprocs/indexB.html}
}
@INPROCEEDINGS{ModNonDetS,
AUTHOR = {J. Alves-Foss},
TITLE = {Modelling Non-Deterministic Systems in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {295--304}
}
@INPROCEEDINGS{MechVer,
AUTHOR = {J. Alves-Foss and K. Levitt},
TITLE = {Mechanical Verification of Secure Distributed Systems in Higher Order Logic},
BOOKTITLE = {Proceedings of the 1991 International Workshop on the {HOL} Theorem
Proving System and its Applications, {D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levitt and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {263--278}
}
@INPROCEEDINGS{SecDistSys,
AUTHOR = {J. Alves-Foss and K. Levitt},
TITLE = {Verification of Secure Distributed Systems in Higher Order Logic: A
Modular Approach Using Generic Components},
BOOKTITLE = {Proceedings of the 1991 {IEEE} Computer Society Symposium on
Research in Security and Privacy; {O}akland, {C}alifornia, {M}ay 1991},
YEAR = {1991},
PAGES = {122--135},
URL = {http://seclab.cs.ucdavis.edu/papers/fl91.abs}
}
@INPROCEEDINGS{HOLUNITY,
AUTHOR = {F. Andersen and U. Binau and K. Nyblad and K. D. Petersen and
J. S. Pettersson},
TITLE = {The {HOL}-{UNITY} verification system},
BOOKTITLE = {{TAPSOFT}'95: Theory and Practice of Software Development:
6th International Conference: Proceedings},
EDITOR = {P. D. Mosses and M. Nielsen and M. I. Schwartzbach},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {915},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {795--796}
}
@INPROCEEDINGS{RecBoo,
AUTHOR = {F. Andersen and K. D. Petersen},
TITLE = {Recursive Boolean Functions in {HOL}},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem
Proving System and its Applications, {D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levitt and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {367--377}
}
@INPROCEEDINGS{GraphTool,
AUTHOR = {F. Andersen and K. D. Petersen and J. S. Pettersson},
TITLE = {A Graphical Tool for Proving {UNITY} Progress},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {17--32}
}
@INPROCEEDINGS{ProgVer,
AUTHOR = {F. Andersen and K. D. Petersen and J. S. Pettersson},
TITLE = {Program Verification using {{HOL}-UNITY}},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {1--15}
}
@PHDTHESIS{FormHardVer,
AUTHOR = {C. M. Angelo},
TITLE = {Formal Hardware Verification in a Silicon Compilation
Environment by means of Theorem Proving},
SCHOOL = {Katholieke Universiteit Leuven},
YEAR = {February, 1994},
URL = {http://www.lsi.usp.br/~catia/phd.html}
}
@INPROCEEDINGS{DegForm,
AUTHOR = {C. M. Angelo and L. Claesen and H. De Man},
TITLE = {Degrees of Formality in Shallow Embedding Hardware
Description Languages in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {89--100},
URL = {http://www.lsi.usp.br/~HOL/papers-ps/HOL93.can.html}
}
@INPROCEEDINGS{FormSemDef,
AUTHOR = {C. M. Angelo and L. Claesen and H. De Man},
TITLE = {The Formal Semantics Definition of a Multi-Rate
{DSP} Specification Language in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {375--394}
}
@INCOLLECTION{MethProvC,
AUTHOR = {C. M. Angelo and L. Claesen and H. De Man},
TITLE = {A Methodology for Proving Correctness of Parameterized Hardware
Modules in {HOL}},
BOOKTITLE = {Tenth International Symposium on Computer Hardware Description
Languages and their Applications, {CHDL}'91: {M}arseille, {F}rance},
EDITOR = {D. Borrione and R. Waxman},
PUBLISHER = {North-Holland},
YEAR = {1991},
PAGES = {63--82}
}
@ARTICLE{ModMulti,
AUTHOR = {C. M. Angelo and L. Claesen and H. De Man},
TITLE = {Modeling Multi-rate {DSP} Specification Semantics
for Formal Transformational Design in {HOL}},
JOURNAL = {Formal Methods in System Design},
VOLUME = {5},
NUMBER = {1/2},
MONTH = {July},
YEAR = {1994},
PAGES = {61--94},
URL = {http://www.lsi.usp.br/~HOL/papers-ps/dsp94.kl.html}
}
@INPROCEEDINGS{ReasCLS,
AUTHOR = {C. M. Angelo and L. Claesen and H. De Man},
TITLE = {Reasoning about a Class of Linear Systems of Equations in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {33--48},
URL = {http://www.lsi.usp.br/~HOL/papers-ps/HOL94.mt.html}
}
@ARTICLE{CompHOL,
AUTHOR = {C. M. Angelo and D. Verkest and L. Claesen and H. De Man},
TITLE = {On the Comparison of {HOL} and {B}oyer-{M}oore for Formal Hardware Verification},
JOURNAL = {Formal Methods in System Design},
VOLUME = {2},
NUMBER = {1},
MONTH = {February},
YEAR = {1993},
PAGES = {45--72},
URL = {http://www.lsi.usp.br/~HOL/papers-ps/HOLxbm93.kl.html}
}
@INPROCEEDINGS{ForHarVer,
AUTHOR = {C. M. Angelo and D. Verkest and L. Claesen and H. De Man},
TITLE = {Formal Hardware Verification in {HOL} and in Boyer-Moore:
A Comparative Analysis},
BOOKTITLE = {Proceedings of the 1991 International Workshop on the {HOL} Theorem
Proving System and its Applications, {D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levitt and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {340-347}
}
@INCOLLECTION{SynopCompHOL,
AUTHOR = {C. M. Angelo and D. Verkest and L. Claesen and H. De Man},
TITLE = {A Synopsis on the Comparison of {HOL} and {B}oyer-{M}oore for Formal
Hardware Verification},
BOOKTITLE = {Advanced Research Workshop on Correct Hardware Design Methodologies},
EDITOR = {P. Prinetto and P. Camurati},
PUBLISHER = {North-Holland},
YEAR = {1991},
PAGES = {421--426}
}
@INPROCEEDINGS{LinkTheoP,
AUTHOR = {M. Archer and G. Fink and L. Yang},
TITLE = {Linking Other Theorem Provers to {HOL} Using {PM}: Proof Manager},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {{N}orth-Holland},
YEAR = {1993},
PAGES = {539-548}
}
@PROCEEDINGS{Proc1991,
EDITOR = {M. Archer and J. J. Joyce and K. N. Levitt and P. J. Windley},
TITLE = {Proceedings of the 1991 International Workshop on the {HOL}
Theorem Proving System and its Applications, {D}avis, {A}ugust 1991},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992}
}
@INPROCEEDINGS{RepICLHOL,
AUTHOR = {R. D. Arthan},
TITLE = {A Report on {ICL} {HOL}},
BOOKTITLE = {Proceedings of the 1991 International Workshop on {HOL} Theorem
Proving System and its Applications, {D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levitt and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {280-283}
}
@TECHREPORT{FormSpec,
AUTHOR = {R. D. Arthan},
TITLE = {A Formal Specification of {HOL}},
NUMBER = {DS/FMU/IED/SPC001},
INSTITUTION = {ICL Defence Systems},
MONTH = {April},
YEAR = {1990}
}
@INPROCEEDINGS{PredTransHOL,
AUTHOR = {R. J. R. Back and J. von Wright},
TITLE = {Predicate Transformers and Higher Order Logic},
BOOKTITLE = {Semantics: Foundations and Applications: {REX} Workshop,
{B}eekbergen, {J}une 1992},
EDITOR = {J. W. de Bakker and W.-P. de Roever and G. Rozenberg},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {666},
PUBLISHER = {Springer-Verlag},
YEAR = {1993},
PAGES = {1--20}
}
@ARTICLE{RefConFH,
AUTHOR = {R. J. R. Back and J. von Wright},
TITLE = {Refinement Concepts Formalised in Higher Order Logic},
JOURNAL = {Formal Aspects of Computing},
VOLUME = {2},
NUMBER = {3},
MONTH = {July-September},
YEAR = {1990},
PAGES = {247--272}
}
@INPROCEEDINGS{IndApp,
AUTHOR = {S. Bainbridge and A. Camilleri and R. Fleming},
TITLE = {Industrial Application of Theorem Proving to System
Level Design},
BOOKTITLE = {Proceedings of the 1991 International Workshop on the {HOL} Theorem
Proving System and its Applications, {D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levitt and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {130-142}
}
@INPROCEEDINGS{TheProvITS,
AUTHOR = {S. Bainbridge and A. Camilleri and R. Fleming},
TITLE = {Theorem Proving as an Industrial Tool for System Level Design},
BOOKTITLE = {Theorem Provers in Circuit Design: Proceedings of the
{IFIP TC10/WG} 10.2 International Conference, {N}ijmegen, {J}une 1992},
EDITOR = {V. Stavridou and T. F. Melham and R. T. Boute},
SERIES = {IFIP Transactions A-10},
PUBLISHER = {North-Holland},
YEAR = {1992},
PAGES = {253--274},
URL = {http://www.dcs.glasgow.ac.uk/~tfm/TPCD.html}
}
@INPROCEEDINGS{ReasPet,
AUTHOR = {E. de Barros Lucena},
TITLE = {Reasoning about Petri Nets in {HOL}},
BOOKTITLE = {Proceedings of the 1991 International Workshop on the {HOL} Theorem
Proving System and its Applications, {Davis}, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levitt and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {384-394}
}
@INPROCEEDINGS{AbstSig,
AUTHOR = {R. H. Beers and P. J. Windley},
TITLE = {Abstracting Signals: The waveform Library},
BOOKTITLE = {Supplementary Proceedings of the 9th International Conference on
Theorem Proving in Higher Order Logics: {TPHOL}s'96},
EDITOR = {J. von Wright and J. Grundy and J. Harrison},
SERIES = {TUCS General Publication},
NUMBER = {1},
PUBLISHER = {Turku Centre for Computer Science},
MONTH = {August},
YEAR = {1996},
PAGES = {1--13},
URL = {http://www.abo.fi/~jharriso/supp-root.html}
}
@INPROCEEDINGS{VerSECDH,
AUTHOR = {G. Birtwistle and B. Graham},
TITLE = {Verifying {SECD} in {HOL}},
BOOKTITLE = {Formal Methods for {VLSI} Design: {IFIP WG}10.2},
EDITOR = {J. Staunstrup},
SERIES = {Lecture Notes},
PUBLISHER = {North-Holland},
YEAR = {1990},
PAGES = {129--177}
}
@UNPUBLISHED{IntroHardV,
AUTHOR = {G. Birtwistle and B. Graham and S.-K. Chin},
TITLE = {An Introduction to Hardware Verification in Higher Order Logic},
NOTE = {Published electronically},
MONTH = {August},
YEAR = {1994},
URL = {http://lal.cs.byu.edu/lal/HOLdoc/birtwistle/all/all.html}
}
@INPROCEEDINGS{VerifySECDinHOL,
AUTHOR = {G. Birtwistle and B. Graham and T. Simpson and K. Slind
and M. Williams and S. Williams},
TITLE = {Verifying an {SECD} chip in {HOL}},
BOOKTITLE = {Proceedings of the IFIP WG 10.2/WG 10.5 International Workshop
on Applied Formal Methods for Correct VLSI Design},
YEAR = {1990},
PUBLISHER = {North Holland},
PAGES = {369--378}
}
@INPROCEEDINGS{VerSECD,
AUTHOR = {G. Birtwistle and B. Graham and T. Simpson and K. Slind and M. Williams
and S. Williams},
TITLE = {Verifying an {SECD} Chip in {HOL}},
BOOKTITLE = {Formal {VLSI} Correctness Verification: {VLSI} Design Methods-{II}:
Proceedings of the {IFIP WG 10.2/WG1} 0.5 International Workshop
on Applied Formal Methods for {VLSI} Design, {B}elgium, {N}ovember 1989},
EDITOR = {L. J. M. Claesen},
PUBLISHER = {North-Holland},
YEAR = {1990},
PAGES = {369--378}
}
@INPROCEEDINGS{ProofToNetlist,
AUTHOR = {G. Birtwistle and M. Hermann and T. Simpson and K. Slind},
TITLE = {From formal proof to netlist},
BOOKTITLE = {Proceedings of the Canadian Conference on VLSI},
YEAR = {1989},
ADDRESS = {Vancouver, British Columbia, Canada},
PAGES = {217--224}
}
@INPROCEEDINGS{AutoSynth,
AUTHOR = {P. E. Black and P. J. Windley},
TITLE = {Automatically Synthesized Term Denotation Predicates: A Proof Aid},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah, {S}eptember 1995:
Proceedings},
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {46--57},
URL = {http://lal.cs.byu.edu/people/black/Papers/HOL95.ps}
}
@INPROCEEDINGS{ForVeSec,
AUTHOR = {P. E. Black and P. J. Windley},
TITLE = {Formal Verification of Secure Programs in the Presence of Side Effects},
BOOKTITLE = {Proceedings of the Thirty-first {H}awai'i International Conference on
System Sciences ({HICSS}-31)},
EDITOR = {R. H. Sprague, Jr.},
VOLUME = {III},
PUBLISHER = {IEEE Computer Science Press},
YEAR = {1998},
PAGES = {327--334}
}
@INPROCEEDINGS{InfRuProgL,
AUTHOR = {P. E. Black and P. J. Windley},
TITLE = {Inference Rules for Programming Languages with Side Effects in Expressions},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International Conference,
{T}urku, {F}inland, {A}ugust 1996: Proceedings},
EDITOR = {J. von Wright and J. Grundy and J. Harrison},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1125},
PUBLISHER = {Springer-Verlag},
YEAR = {1996},
PAGES = {51--60}
}
@INPROCEEDINGS{VerResSoft,
AUTHOR = {P. E. Black and P. J. Windley},
TITLE = {Verifying Resilient Software},
BOOKTITLE = {Proceedings of the Thirty-first {H}awai'i International Conference on
System Sciences ({HICSS}-31)},
EDITOR = {R. H. Sprague, Jr.},
VOLUME = {III},
PUBLISHER = {IEEE Computer Science Press},
YEAR = {1998},
PAGES = {262-266}
}
@INPROCEEDINGS{RepICL,
AUTHOR = {K. Blackburn},
TITLE = {A Report on {ICL} {HOL}},
BOOKTITLE = {Automated Deduction - {CADE}--11: 11th International
Conference, Proceedings},
EDITOR = {D. Kapur},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {607},
PUBLISHER = {Springer-Verlag},
YEAR = {1992},
PAGES = {743--747}
}
@INPROCEEDINGS{OnRefSM,
AUTHOR = {J.-P. Bodeviex and M. Filali},
TITLE = {On the refinement of symmetric memory protocols},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah, {S}eptember 1995:
Proceedings},
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {58--74}
}
@INPROCEEDINGS{Theomem,
AUTHOR = {J-P. Bodeviex and M. Filali and P. Roche},
TITLE = {Towards a {HOL} theory of memory},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {49--64}
}
@INPROCEEDINGS{BoyMoAut,
AUTHOR = {R. Boulton},
TITLE = {{B}oyer-{M}oore Automation for the {HOL} System},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {133--142}
}
@INPROCEEDINGS{CombDecP,
AUTHOR = {R. Boulton},
TITLE = {Combining Decision Procedures in the {HOL} System},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah, {S}eptember 1995:
Proceedings},
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {75--89},
URL = {http://www.cl.cam.ac.uk/users/rjb/papers/comb-dec-proc.dvi.gz}
}
@TECHREPORT{EffinFE,
AUTHOR = {R. J. Boulton},
TITLE = {Efficiency in a Fully-Expansive Theorem Prover},
NUMBER = {337},
INSTITUTION = {University of Cambridge Computer Laboratory},
MONTH = {May},
YEAR = {1994},
URL = {http://www.cl.cam.ac.uk/users/rjb/phd/index.html}
}
@INPROCEEDINGS{LazyApp,
AUTHOR = {R. Boulton},
TITLE = {A Lazy Approach to Full-Expansive Theorem Proving},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {19--38}
}
@ARTICLE{LazyTech,
AUTHOR = {R. J. Boulton},
TITLE = {Lazy Techniques for Fully Expansive Theorem Proving},
JOURNAL = {Formal Methods in System Design},
VOLUME = {3},
NUMBER = {1--2},
MONTH = {August},
YEAR = {1993},
PAGES = {25--47}
}
@TECHREPORT{OnETPF,
AUTHOR = {R. J. Boulton},
TITLE = {On Efficiency in Theorem Provers which Fully Expand Proofs
into Primitive Inferences},
NUMBER = {248},
INSTITUTION = {University of Cambridge Computer Laboratory},
MONTH = {February},
YEAR = {1992},
URL = {http://www.cl.cam.ac.uk/ftp/papers/reports/TR248-rjb-efficiency-primitive-inferences.dvi.gz}
}
@INPROCEEDINGS{RestFoHOR,
AUTHOR = {R. Boulton},
TITLE = {A Restricted Form of Higher-Order Rewriting Applied to
an {HDL} Semantics},
BOOKTITLE = {Rewriting Techniques and Applications: 6th International
Conference: Proceedings},
EDITOR = {J. Hsiang},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {914},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {309--323}
}
@INPROCEEDINGS{ExpEmbHDL,
AUTHOR = {R. Boulton and A. Gordon and M. Gordon and J. Harrison and J. Herbert
and J. Van Tassel},
TITLE = {Experience with Embedding Hardware Description Languages in {HOL}},
BOOKTITLE = {Theorem Provers in Circuit Design: Proceedings of the
{IFIP TC10/WG} 10.2 International Conference, {N}ijmegen, {J}une 1992},
EDITOR = {V. Stavridou and T. F. Melham and R. T. Boute},
SERIES = {IFIP Transactions A-10},
PUBLISHER = {North-Holland},
YEAR = {1992},
PAGES = {129--156},
URL = {ftp://ftp.cl.cam.ac.uk/hvg/papers/EmbeddingPaper.ps.gz}
}
@UNPUBLISHED{ProcVLSIDes,
AUTHOR = {R. Boulton and M. Gordon and J. Herbert and J. Van Tassel},
TITLE = {The {HOL} Verification of {ELLA} Designs},
NOTE = {Appeared in the Unpublished Proceedings of the International
Workshop on Formal Methods in {VLSI} Design, {M}iami,
{F}lorida {J}anuary 1991},
YEAR = {1991},
URL = {http://www.cl.cam.ac.uk/ftp/papers/reports/TR199-rjb-mjcg-jmjh-jvt-HOL-verification-ELLA.ps.gz}
}
@INPROCEEDINGS{AutoDerIndMut,
AUTHOR = {R. Boulton and K. Slind},
TITLE = {Automatic Derivation and Application of Induction
Schemes for Mutually Recursive Functions},
BOOKTITLE = {Computational Logic: First International Conference,
{CL2000}, London, UK, July 2000: Proceedings},
PUBLISHER = {Springer-Verlag},
VOLUME = {1861},
PAGES = {629--643},
EDITOR = {J. Lloyd and V. Dahl and U. Furbach and M. Kerber and
K.-K. Lau and C. Palamidessi and L. {Moniz Pereira} and
Y. Sagiv and P. J. Stuckey},
YEAR = {2000}
}
@INPROCEEDINGS{InterfaceClamHOL,
AUTHOR = {R. Boulton and K. Slind and A. Bundy and M. Gordon},
TITLE = {An interface between {C}lam and {HOL}},
EDITOR = {J. Grundy and M. Newey},
BOOKTITLE = {Theorem Proving in Higher Order Logics, 11th
International Conference, {TPHOLs'98}, Canberra: Proceedings},
YEAR = {1998},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1479},
PAGES = {87--104}
}
@BOOK{TVerSys,
EDITOR = {J. Bowen},
TITLE = {Towards Verified Systems},
SERIES = {Real-Time Safety Critical Systems Series},
VOLUME = {2},
PUBLISHER = {Elsevier},
YEAR = {1994}
}
@ARTICLE{ShalEmb,
AUTHOR = {J. P. Bowen and M. J. C. Gordon},
TITLE = {A Shallow Embedding of {Z} in {HOL}},
JOURNAL = {Information and Software Technology},
VOLUME = {37},
NUMBER = {5--6},
MONTH = {May/June},
YEAR = {1995},
PAGES = {269--276},
URL = {ftp://ftp.comlab.ox.ac.uk/pub/Documents/techpapers/Jonathan.Bowen/zHOL-ist.ps}
}
@INCOLLECTION{ZHOL,
AUTHOR = {J. P. Bowen and M. J. C. Gordon},
TITLE = {{Z} and {HOL}},
BOOKTITLE = {{Z} User Workshop, {C}ambridge 1994},
EDITOR = {J. P. Bowen and J. A. Hall},
SERIES = {Workshops in Computing Series},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {141--167},
URL = {file://ftp.comlab.ox.ac.uk/pub/Documents/techpapers/Jonathan.Bowen/zHOL.ps.Z}
}
@INPROCEEDINGS{DecCPA,
AUTHOR = {S. H. Brackin},
TITLE = {Deciding Cryptographic Protocol Adequacy with {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah, {S}eptember 1995:
Proceedings},
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {90--105}
}
@INPROCEEDINGS{DecCryptP,
AUTHOR = {S. H. Brackin},
TITLE = {Deciding Cryptographic Protocol Adequacy with {HOL}: The Implementation},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International Conference,
{T}urku, {F}inland, {A}ugust 1996: Proceedings},
EDITOR = {J. von Wright and J. Grundy and J. Harrison},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1125},
PUBLISHER = {Springer-Verlag},
YEAR = {1996},
PAGES = {61--76}
}
@INPROCEEDINGS{ProvTS,
AUTHOR = {S. H. Brackin},
TITLE = {Providing Tractable Security Analyses in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {65--80}
}
@INPROCEEDINGS{ServPro,
AUTHOR = {S. H. Brackin and S.-K. Chin},
TITLE = {Server-Process Restrictiveness in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {450--463}
}
@INPROCEEDINGS{RefCalc,
AUTHOR = {Michael Butler and Jim Grundy and Thomas L{\aa}ngbacka
and Rimvydas Ruksenas and
Joakim {von Wright}},
EDITOR = {Lindsay Groves and Steve Reeves},
BOOKTITLE = {Formal Methods Pacific'97: Proceedings of FMP'97},
TITLE = {The Refinement Calculator: Proof Support for
Program Refinement},
PUBLISHER = {Springer-Verlag},
ADDRESS = {Wellington, New Zealand},
PAGES = {40--61},
MONTH = JUL,
YEAR = {1997},
SERIES = {Discrete Mathematics \& Theoretical Computer Science}
}
@INPROCEEDINGS{ProgDerRC,
AUTHOR = {M. Butler and T. L{\aa}ngbacka},
TITLE = {Program Derivation Using the Refinement Calculator},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International Conference,
{T}urku, {F}inland, {A}ugust 1996: Proceedings},
EDITOR = {J. von Wright and J. Grundy and J. Harrison},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1125},
PUBLISHER = {Springer-Verlag},
YEAR = {1996},
PAGES = {93--108}
}
@TECHREPORT{ExBeDeHOL,
AUTHOR = {A. J. Camilleri},
TITLE = {Executing Behavioural Definitions in Higher Order Logic},
NUMBER = {140},
INSTITUTION = {University of Cambridge Computer Laboratory},
MONTH = {February},
YEAR = {1988}
}
@INPROCEEDINGS{HOLMechCSP,
AUTHOR = {A. J. Camilleri},
TITLE = {A Higher Order Logic Mechanization of the {CSP} Failure-Divergence Semantics},
BOOKTITLE = {{IV} Higher Order Workshop, {B}anff 1990: Proceedings},
EDITOR = {G. Birtwistle},
PUBLISHER = {Springer-Verlag},
YEAR = {1991},
PAGES = {123--150}
}
@ARTICLE{MechCSPTT,
AUTHOR = {A. J. Camilleri},
TITLE = {Mechanizing {CSP} Trace Theory in Higher Order Logic},
JOURNAL = {{IEEE} Transactions on Software Engineering},
VOLUME = {16},
NUMBER = {9},
MONTH = {September},
YEAR = {1990},
PAGES = {993--1004}
}
@INPROCEEDINGS{ReasCSPvia,
AUTHOR = {A. J. Camilleri},
TITLE = {Reasoning in {CSP} via the {HOL} Theorem Prover},
BOOKTITLE = {Next Decade in Information Technology: Proceedings of the 5th {J}erusalem
Conference on Information Technology, {I}srael, 22--25 {O}ctober 1990},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1990},
PAGES = {173--183}
}
@ARTICLE{SimHarSpec,
AUTHOR = {A. J. Camilleri},
TITLE = {Simulating Hardware Specifications within a Theorem-Proving
Framework},
JOURNAL = {International Journal of Computer Aided {VLSI} Design},
VOLUME = {2},
YEAR = {1990},
PAGES = {315--337}
}
@INPROCEEDINGS{SimasVerHOL,
AUTHOR = {A. J. Camilleri},
TITLE = {Simulation as an aid to Verification using the {HOL} Theorem Prover},
BOOKTITLE = {Design Methodologies for {VLSI} and Computer Architecture: Proceedings
of the {IFIP} {TC}-10 International Working Conference, {P}isa, {I}taly,
19--21 {S}eptember 1988},
EDITOR = {D. Edwards},
PUBLISHER = {North-Holland},
YEAR = {1989},
PAGES = {147--168}
}
@INPROCEEDINGS{HaVeHOLF,
AUTHOR = {A. Camilleri and M. Gordon and T. Melham},
TITLE = {Hardware Verification using Higher-Order Logic},
BOOKTITLE = {From {HDL} Descriptions to Guaranteed Correct Circuit
Designs: Proceedings of the {IFIP WG} 10.2 Working Conference,
{S}eptember 1986},
EDITOR = {D. Borrione},
PUBLISHER = {North-Holland},
YEAR = {1987},
PAGES = {43--67}
}
@INPROCEEDINGS{CoInAut,
AUTHOR = {A. Camilleri and P. Inverardi and M. Nesi},
TITLE = {Combining Interaction and Automation in Process Algebra Verification},
BOOKTITLE = {{TAPSOFT}'91: Proceedings of the International Joint Conference on Theory
and Practice of Software Development, {B}righton, 8--12 {A}pril 1991},
EDITOR = {S. Abramsky and T. Maibaum},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {494},
PUBLISHER = {Springer-Verlag},
YEAR = {1991},
PAGES = {283--296}
}
@TECHREPORT{ReasIndDef,
AUTHOR = {J. Camilleri and T. Melham},
TITLE = {Reasoning with Inductively Defined Relations
in the {HOL} Theorem Prover},
NUMBER = {265},
INSTITUTION = {University of Cambridge Computer Laboratory},
MONTH = {August},
YEAR = {1992},
URL = {ftp://ftp.dcs.glasgow.ac.uk/pub/users/tfm/Papers/TR265.ps}
}
@INPROCEEDINGS{SymAnim,
AUTHOR = {J. Camilleri and V. Zammit},
TITLE = {Symbolic Animation as a Proof Tool},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {113--127}
}
@TECHREPORT{FoVeHRTS,
AUTHOR = {R. M. Cardell-Oliver},
TITLE = {The Formal Verification of Hard Real-Time Systems},
NUMBER = {255},
INSTITUTION = {University of Cambridge Computer Laboratory},
MONTH = {May},
YEAR = {1992}
}
@INCOLLECTION{HTTDHOL,
AUTHOR = {R. Cardell-Oliver},
TITLE = {{HTTD}s and {HOL}},
BOOKTITLE = {Formal development of Reactive Systems: Case Study Production Cell},
EDITOR = {C. Lewerentz and T. Lindner},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {891},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {261--276},
URL = {ftp://hp1.essex.ac.uk/pub/csc/technical-reports/CSM-214.ps.Z}
}
@INPROCEEDINGS{ProtVer,
AUTHOR = {R. Cardell-Oliver},
TITLE = {On the use of the {HOL} system for Protocol Verification},
BOOKTITLE = {Proceedings of the 1991 International Workshop on the {HOL} Theorem
Proving System and its Applications, {Davis}, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levitt and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {59-62}
}
@TECHREPORT{LinkNotT,
AUTHOR = {R. M. Cardell-Oliver and R. Hale},
TITLE = {Linking Notations and Theories in a Proof Tool},
NUMBER = {CSM-245},
INSTITUTION = {Department of Computer Science, University of Essex},
MONTH = {August},
YEAR = {1995},
URL = {ftp://hp1.essex.ac.uk/pub/csc/technical-reports/CSM-245.ps.Z}
}
@INPROCEEDINGS{EmbTTS,
AUTHOR = {R. Cardell-Oliver and R. Hale and J. Herbert},
TITLE = {An Embedding of Timed Transition Systems in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {263--278}
}
@TECHREPORT{ThProvAMC,
AUTHOR = {R. Cardel-Oliver and C. Southon},
TITLE = {Theorem Proving Abstraction of Model Checking},
NUMBER = {CSM-253},
INSTITUTION = {Department of Computer Science, University of Essex},
MONTH = {October},
YEAR = {1995},
URL = {ftp://hp1.essex.ac.uk/pub/csc/technical-reports/CSM-253.ps.Z}
}
@UNPUBLISHED{DataRout,
AUTHOR = {V. A. Carre{\~{n}}o},
TITLE = {Definition and Partial Verification of Data Routing Circuit in HOL},
MONTH = {July},
YEAR = {1991},
URL = {http://shemesh.larc.nasa.gov/fm/ftp/larc/vac/data_router.ps}
}
@PHDTHESIS{TransAsser,
AUTHOR = {V. A. Carre{\~{n}}o},
TITLE = {Transition Assertions: A Higher-Order Logic Based Method
for the Specification and Verfication of Real-Time Systems},
SCHOOL = {University of Cambridge Computer Laboratory},
YEAR = {1997},
URL = {http://shemesh.larc.nasa.gov/ftp/larc/vac/diss.ps.gz}
}
@TECHREPORT{TransAM,
AUTHOR = {V. A. Carre{\~{n}}o},
TITLE = {The Transition Assertions Specification Method},
NUMBER = {279},
INSTITUTION = {Computer Laboratory, University of Cambridge},
MONTH = {January},
YEAR = {1993},
URL = {http://shemesh.larc.nasa.gov/fm/ftp/larc/vac/transition_assertions.ps}
}
@INPROCEEDINGS{VerinHOL,
AUTHOR = {V. A. Carre{\~{n}}o},
TITLE = {Verification in Higher Order Logic of Mutual Exclusion Algorithm},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {501--513}
}
@INPROCEEDINGS{SpeIEEE,
AUTHOR = {V. A. Carre\~o and P. S. Miner},
TITLE = {Specification of the {IEEE}-854 Floating-Point Standard in
{HOL} and {PVS}},
BOOKTITLE = {{HOL}-95: International Workshop on Higher Order Logic Theorem
Proving and its Applications: {B}-Track: Short Presentations,
{A}spen {G}rove, {U}tah, {S}eptember, 1995},
EDITOR = {J. Alves-Foss},
YEAR = {1995},
PAGES = {1--16},
URL = {http://lal.cs.byu.edu/lal/HOL95/Bprocs/carreno.ps}
}
@INPROCEEDINGS{CoEnVigor,
AUTHOR = {S.-K. Chin},
TITLE = {Combining Engineering Vigor with Mathematical Rigor},
BOOKTITLE = {Hardware Specification, Verification and Synthesis: Mathematical
Aspects: Mathematical Sciences Institute Workshop, {C}ornell, {J}uly 1989},
EDITOR = {M. Leeser and G. Brown},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {408},
PUBLISHER = {Springer-Verlag},
YEAR = {1990},
PAGES = {152--176}
}
@ARTICLE{VerFunGSB,
AUTHOR = {S.-K. Chin},
TITLE = {Verified Functions for Generating Signed-Binary Arithmetic
Hardware},
JOURNAL = {IEEE Transactions on Computer-Aided Design of Integrated
Circuits and Systems},
VOLUME = {11},
NUMBER = {12},
MONTH = {December},
YEAR = {1992},
PAGES = {1529--1558}
}
@INPROCEEDINGS{VerSynFNA,
AUTHOR = {S.-K. Chin},
TITLE = {Verified Synthesis Functions for Negabinary Arithmetic Hardware},
BOOKTITLE = {Formal {VLSI} Correctness Verification: {VLSI} Design Methods-{II}:
Proceedings of the {IFIP WG 10.2/WG1} 0.5 International Workshop
on Applied Formal Methods for {VLSI} Design, {B}elgium, {N}ovember 1989},
EDITOR = {L. J. M. Claesen},
PUBLISHER = {North-Holland},
YEAR = {1990},
PAGES = {187-196}
}
@INPROCEEDINGS{VerAriH,
AUTHOR = {S.-K. Chin},
TITLE = {Verifying Arithmetic Hardware in Higher-Order Logic},
BOOKTITLE = {Proceedings of the 1991 International Workshop on the {HOL} Theorem
Proving System and its Applications, {D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levitt and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {22-31}
}
@INPROCEEDINGS{ImVerFinS,
AUTHOR = {S.-K. Chin and G. Birtwistle},
TITLE = {Implementing and Verifying Finite-State Machines Using
Types in Higher-Order Logic},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {121--129}
}
@INPROCEEDINGS{TheoUG,
AUTHOR = {C.-T. Chou},
TITLE = {A Formal Theory of Undirected Graphs in Higher-Order Logic},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {144--157},
URL = {ftp://ftp.cs.ucla.edu/pub/chou/graph.ps}
}
@ARTICLE{MVerDAHOL,
AUTHOR = {C.-T. Chou},
TITLE = {Mechanical Verification of Distributed Algorithms in Higher-Order Logic},
JOURNAL = {The Computer Journal},
VOLUME = {38},
NUMBER = {2},
MONTH = {July},
YEAR = {1995},
PAGES = {152--161},
URL = {http://www.oup.co.uk/oup/smj/journals/ed/titles/computer_journal/docs/journal_contents/Volume_38_Number_2/38.2.ps/chou.ps}
}
@INPROCEEDINGS{VerDA,
AUTHOR = {C.-T. Chou},
TITLE = {Mechanical Verification of Distributed Algorithms in Higher-Order Logic},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {158--176}
}
@INPROCEEDINGS{NoteIntTP,
AUTHOR = {C.-T. Chou},
TITLE = {Note on Interactive Theorem Proving with Theorem Continuation
Functions},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {59--69},
URL = {ftp://ftp.cs.ucla.edu/pub/chou/cont.ps}
}
@INPROCEEDINGS{PredTemp,
AUTHOR = {C.-T. Chou},
TITLE = {Predicates, Temporal Logic, and Simulations},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {310--323}
}
@INPROCEEDINGS{SeqFor,
AUTHOR = {C.-T. Chou},
TITLE = {Sequent Formulation of a Logic of Predicates in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {{IFIP} Transactions {A}-20},
PUBLISHER = {{N}orth-Holland},
YEAR = {1993},
PAGES = {71--80},
URL = {ftp://ftp.cs.ucla.edu/pub/chou/pred.ps}
}
@INPROCEEDINGS{FoVeriPart,
AUTHOR = {C.-T. Chou and D. Peled},
TITLE = {Formal Verification of a Partial-Order Reduction Technique
for Model Checking},
BOOKTITLE = {Tools and Algorithms for the Construction and
Analysis of Systems: Second International Workshop, {TACAS}'96:
{P}assau, {M}arch 27--29 1996: Proceedings},
EDITOR = {T. Margaria and B. Steffen},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1055},
PUBLISHER = {Springer-Verlag},
YEAR = {1996},
PAGES = {241--257}
}
@PROCEEDINGS{HOLApp,
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
TITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993}
}
@PHDTHESIS{ResfroVPM,
AUTHOR = {M. L. Coe},
TITLE = {Results from Verifying a Pipelined Microprocessor},
SCHOOL = {University of Idaho},
MONTH = {October},
YEAR = {1994},
URL = {ftp://lal.cs.byu.edu/pub/HOL/lal-papers/coe.thesis.ps.gz}
}
@INCOLLECTION{CorrProVip,
AUTHOR = {A. Cohn},
TITLE = {Correctness Properties of the Viper Block Model: The Second Level},
BOOKTITLE = {Current Trends in Hardware Verification and Automated Theorem Proving},
EDITOR = {G. Birtwistle and P. A. Subrahmanyam},
PUBLISHER = {Springer-Verlag},
YEAR = {1989},
PAGES = {1--91}
}
@INCOLLECTION{ViperFirst,
AUTHOR = {A. Cohn},
TITLE = {A Proof of Correctness of the {VIPER} Microprocessor: The First Level},
BOOKTITLE = {Current Trends in Hardware Verification and Automated Theorem Proving},
EDITOR = {G. Birtwistle and P. A. Subrahmanyam},
PUBLISHER = {Springer-Verlag},
YEAR = {1989},
PAGES = {27--71}
}
@ARTICLE{NotProHV,
AUTHOR = {A. Cohn},
TITLE = {The Notion of Proof in Hardware Verification},
JOURNAL = {Journal of Automated Reasoning},
VOLUME = {5},
NUMBER = {2},
MONTH = {June},
YEAR = {1989},
PAGES = {127--139}
}
@INCOLLECTION{Ameprooco,
AUTHOR = {A. Cohn and M. Gordon},
TITLE = {A mechanized proof of correctness of a simple counter},
BOOKTITLE = {Theoretical Foundations of {VLSI} Design},
EDITOR = {K. McEvoy and J. V. Tucker},
SERIES = {Cambridge Tracts in Theoretical Computer Science},
NUMBER = {10},
PUBLISHER = {Cambridge University Press},
YEAR = {1990},
PAGES = {65--96}
}
@INPROCEEDINGS{ProoTooR,
AUTHOR = {G. Collins},
TITLE = {A Proof Tool for Reasoning About Functional Programs},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International Conference,
{T}urku, {F}inland, {A}ugust 1996: Proceedings},
EDITOR = {J. von Wright and J. Grundy and J. Harrison},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1125},
PUBLISHER = {Springer-Verlag},
YEAR = {1996},
PAGES = {109--124}
}
@MASTERSTHESIS{SupForReaAS,
AUTHOR = {G. Collins},
TITLE = {Supporting Formal Reasoning About Standard {ML}},
SCHOOL = {University of Edinburgh},
MONTH = {November},
YEAR = {1994},
URL = {http://www.dcs.gla.ac.uk/~grmc/Papers/dissertation.ps.Z}
}
@INPROCEEDINGS{TheoFin,
AUTHOR = {G. Collins and D. Syme},
TITLE = {A Theory of Finite Maps},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah, {S}eptember 1995:
Proceedings},
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {122--137},
URL = {http://www.dcs.glasgow.ac.uk/~grmc/Papers/fmap.ps}
}
@TECHREPORT{SuppFor,
AUTHOR = {G. Collins and S. Gilmore},
TITLE = {Supporting Formal Reasoning about Standard {ML}},
NUMBER = {LFCS report ECS-LFCS-94-310},
INSTITUTION = {Department of Computer Science, University of Edinburgh},
MONTH = {November},
YEAR = {1994},
URL = {http://www.dcs.ed.ac.uk/lfcsreps/EXPORT/94/ECS-LFCS-94-310/index.html}
}
@ARTICLE{RevIntro,
AUTHOR = {I. Craig},
TITLE = {Review of Introduction to {HOL}, edited by {M}. {G}ordon and
{T}. {M}elham ({C}ambridge University Press), 1993},
JOURNAL = {The Computer Journal},
VOLUME = {36},
NUMBER = {6},
YEAR = {1993},
PAGES = {601}
}
@ARTICLE{IrrBehP,
AUTHOR = {W. J. Cullyer and W. J. Scales},
TITLE = {Irregularities in the Behaviour of the 68020 Processor},
JOURNAL = {High Integrity Systems},
VOLUME = {1},
NUMBER = {3},
YEAR = {1995},
PAGES = {301--311}
}
@ARTICLE{AppForMet,
AUTHOR = {W. J. Cullyer and W. Wong},
TITLE = {Application of Formal Methods to Railway Signalling - a Case Study},
JOURNAL = {IEE Computing and Control Engineering Journal},
VOLUME = {4},
NUMBER = {1},
MONTH = {February},
YEAR = {1993},
PAGES = {15--22}
}
@INCOLLECTION{ComCorInOut,
AUTHOR = {P. Curzon},
TITLE = {Compiler Correctness and Input/Output},
BOOKTITLE = {Dependable Computing for Critical Applications 3},
EDITOR = {C. E. Landwehr and B. Randell and L. Simoncini},
SERIES = {Dependable Computing and Fault-Tolerant Systems series},
VOLUME = {8},
PUBLISHER = {Springer Verlag},
YEAR = {1993},
PAGES = {189--209},
URL = {http://www.cl.cam.ac.uk/users/pc/dcca92.html}
}
@ARTICLE{DerCorP,
AUTHOR = {P. Curzon},
TITLE = {Deriving Correctness Properties of Compiled Code},
JOURNAL = {Formal Methods in System Design},
VOLUME = {3},
NUMBER = {1--2},
MONTH = {August},
YEAR = {1993},
PAGES = {83--115}
}
@INPROCEEDINGS{DerCorPCC,
AUTHOR = {P. Curzon},
TITLE = {Deriving Correctness Properties of Compiled Code},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {327--346},
URL = {http://www.cl.cam.ac.uk/users/pc/hug92.html}
}
@INPROCEEDINGS{ForVeATNet,
AUTHOR = {P. Curzon},
TITLE = {The Formal Verification of an {ATM} Network},
BOOKTITLE = {Proceedings of the 13th Annual {ACM} Symposium on Principles
of Distributed Computing},
PUBLISHER = {ACM Press},
YEAR = {1994},
PAGES = {392},
URL = {http://www.cl.cam.ac.uk/users/pc/podc94.html}
}
@INPROCEEDINGS{ExpeFoVNC,
AUTHOR = {P. Curzon},
TITLE = {Experiences Formally Verifying a Network Component},
BOOKTITLE = {Proceedings of the 9th Annual {IEEE} Conference on Computer Assurance},
PUBLISHER = {IEEE Press},
YEAR = {1994},
PAGES = {183--193},
URL = {http://www.cl.cam.ac.uk/users/pc/comp94.html}
}
@TECHREPORT{FVerofFATM,
AUTHOR = {P. Curzon},
TITLE = {The Formal Verification of the Fairisle {ATM} Switching Element},
NUMBER = {329},
INSTITUTION = {Computer Laboratory, University of Cambridge},
MONTH = {March},
YEAR = {1994},
URL = {http://www.cl.cam.ac.uk/users/pc/el2tr94.html}
}
@TECHREPORT{FVofFATM,
AUTHOR = {P. Curzon},
TITLE = {The Formal Verification of the Fairisle {ATM} Switching Element: an Overview},
NUMBER = {328},
INSTITUTION = {Computer Laboratory, University of Cambridge},
MONTH = {March},
YEAR = {1994},
URL = {http://www.cl.cam.ac.uk/users/pc/el1tr94.html}
}
@INPROCEEDINGS{ImPrMaRe,
AUTHOR = {P. Curzon},
TITLE = {The Importance of Proof Maintenance and Reengineering},
BOOKTITLE = {{HOL}-95: International Workshop on Higher Order Logic Theorem
Proving and its Applications: {B}-Track: Short Presentations,
{A}spen {G}rove, {U}tah, {S}eptember, 1995},
EDITOR = {J. Alves-Foss},
YEAR = {1995},
PAGES = {17--31},
URL = {http://www.cl.cam.ac.uk/users/pc/hugm95.html}
}
@TECHREPORT{OfWhatUse,
AUTHOR = {P. Curzon},
TITLE = {Of What Use is a Verified Compiler Specification?},
NUMBER = {274},
INSTITUTION = {Computer Laboratory, University of Cambridge},
MONTH = {November},
YEAR = {1992},
URL = {http://www.cl.cam.ac.uk/users/pc/whytr92.html}
}
@INPROCEEDINGS{ProbEncWiM,
AUTHOR = {P. Curzon},
TITLE = {Problems Encountered with the Machine-assisted Proof of Hardware},
BOOKTITLE = {Correct Hardware Design and Verification Methods},
EDITOR = {P. E. Camurati and H. Eveking},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {987},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {56--70},
URL = {http://www.cl.cam.ac.uk/users/pc/charme95.html}
}
@INPROCEEDINGS{AProLoVS,
AUTHOR = {P. Curzon},
TITLE = {A Programming Logic for a Verified Structured Assembly Language},
BOOKTITLE = {Logic Programming and Automated Reasoning:International
Conference, {LPAR}'92: {S}t. {P}etersburg, 1992},
EDITOR = {A. Voronkov},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {624},
PUBLISHER = {Springer-Verlag},
YEAR = {1992},
PAGES = {403--408},
URL = {http://www.cl.cam.ac.uk/users/pc/lpar92.html}
}
@ARTICLE{TraDeCF,
AUTHOR = {P. Curzon},
TITLE = {Tracking Design Changes with Formal Machine-Checked Proof},
JOURNAL = {The Computer Journal},
VOLUME = {38},
NUMBER = {2},
MONTH = {July},
YEAR = {1995},
PAGES = {91--100},
URL = {http://www.oup.co.uk/oup/smj/journals/ed/titles/computer_journal/docs/journal_contents/Volume_38_Number_2/38.2.ps/curzon.ps}
}
@INPROCEEDINGS{TracDC,
AUTHOR = {P. Curzon},
TITLE = {Tracking Design Changes with Formal Verification},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {177--192},
URL = {http://www.cl.cam.ac.uk/users/pc/hugtrk94.html}
}
@INPROCEEDINGS{VerCompSA,
AUTHOR = {P. Curzon},
TITLE = {Verified Compiler for a Structured Assembly Language},
BOOKTITLE = {Proceedings of the 1991 International Workshop on the {HOL} Theorem
Proving System and its Applications, {D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levitt and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {253-262},
URL = {http://www.cl.cam.ac.uk/users/pc/hug91.html}
}
@TECHREPORT{VerVistI,
AUTHOR = {P. Curzon},
TITLE = {A Verified Vista Implementation},
NUMBER = {311},
INSTITUTION = {Computer Laboratory, University of Cambridge},
MONTH = {September},
YEAR = {1993},
URL = {http://www.cl.cam.ac.uk/users/pc/fintr93.html}
}
@INPROCEEDINGS{VirtTheo,
AUTHOR = {P. Curzon},
TITLE = {Virtual Theories},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah, {S}eptember 1995:
Proceedings},
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {138--153},
URL = {http://www.cl.cam.ac.uk/users/pc/hugvt95.html}
}
@INPROCEEDINGS{CaStDP,
AUTHOR = {P. Curzon and I. M. Leslie},
TITLE = {A Case Study on Design for Provability},
BOOKTITLE = {Proceedings of the First International Conference on Engineering
of Complex Computer Systems},
PUBLISHER = {IEEE Press},
YEAR = {November 1995},
PAGES = {59--62},
URL = {http://www.cl.cam.ac.uk/users/pc/iceccs95.html}
}
@INPROCEEDINGS{ConStVer,
AUTHOR = {P. Curzon and I. Leslie and M. Gordon},
TITLE = {Conclusions from a Study to Verify a Real Network Component},
BOOKTITLE = {Automated Reasoning: Bridging the Gap Between Theory and Practice;
Proceedings},
EDITOR = {A. Ireland},
YEAR = {April 1995},
URL = {http://www.cl.cam.ac.uk/users/pc/war95.html}
}
@INPROCEEDINGS{TheLiHOLB,
AUTHOR = {P. Curzon and W. Wong},
TITLE = {A Theory of Lists for {HOL} Based on Higher-Order Functions},
BOOKTITLE = {Supplementary Proceedings of the 7th International Workshop on Higher
Order Logic Theorem Proving and its Applications},
EDITOR = {T. F. Melham and J. Camilleri},
PUBLISHER = {University of Malta, Valletta},
YEAR = {1994},
URL = {ftp://ftp.dcs.glasgow.ac.uk/pub/hug94/curzon.ps.gz}
}
@INPROCEEDINGS{SemanS,
AUTHOR = {N. Day and J. J. Joyce},
TITLE = {The Semantics of Statecharts in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {338--351}
}
@INCOLLECTION{ForValIntC,
AUTHOR = {I. S. Dhingra},
TITLE = {Formal Validation of an Integrated Circuit Design Style},
BOOKTITLE = {Current Trends in Hardware Verification and Automated Theorem Proving},
EDITOR = {G. Birtwistle and P. A. Subrahmanyam},
PUBLISHER = {Springer-Verlag},
YEAR = {1989},
PAGES = {293--321}
}
@TECHREPORT{ForIntCirDS,
AUTHOR = {I. S. Dhingra},
TITLE = {Formalising an Integrated Circuit Design Style in
Higher Order Logic},
NUMBER = {151},
INSTITUTION = {Computer Laboratory, University of Cambridge},
MONTH = {November},
YEAR = {1988}
}
@INPROCEEDINGS{ImpIssEEHL,
AUTHOR = {D. Eisenbiegler and C. Blumenr{\"{o}}hr and R. Kumar},
TITLE = {Implementation Issues About the Embedding of Existing
High Level Synthesis Algorithms in {HOL}},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International Conference,
{T}urku, {F}inland, {A}ugust 1996: Proceedings},
EDITOR = {J. von Wright and J. Grundy and J. Harrison},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1125},
PUBLISHER = {Springer-Verlag},
YEAR = {1996},
PAGES = {157--172}
}
@INPROCEEDINGS{AutomTheo,
AUTHOR = {D. Eisenbiegler and R. Kumar},
TITLE = {An Automata Theory Dedicated towards Formal Circuit Synthesis},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah, {S}eptember 1995:
Proceedings},
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {154--169}
}
@INPROCEEDINGS{EvTechPVP,
AUTHOR = {D. Eisenbiegler and R. Kumar},
TITLE = {Evaluation Techniques as a Part of the Verification Process},
BOOKTITLE = {Supplementary Proceedings of the 7th International Workshop on Higher
Order Logic Theorem Proving and its Applications},
EDITOR = {T. F. Melham and J. Camilleri},
PUBLISHER = {University of Malta, Valletta},
YEAR = {1994},
URL = {ftp://ftp.dcs.glasgow.ac.uk/pub/hug94/eisenbiegler.ps.gz}
}
@INPROCEEDINGS{FuncApp,
AUTHOR = {D. Eisenbiegler and K. Schneider and R. Kumar},
TITLE = {A Functional Approach to Formalizing Regular Hardware Structures},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {101--114},
URL = {http://goethe.ira.uka.de/hvg/techreports/SFB358-C2-14-93.ps.gz}
}
@INPROCEEDINGS{PMaMP,
AUTHOR = {G. Fink and M. Archer and L. Yang},
TITLE = {PM: A Proof Manager for {HOL} and Other Provers},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {286--304}
}
@INPROCEEDINGS{WeakSys,
AUTHOR = {T. Forster},
TITLE = {Weak Systems of Set Theory Related to {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {193--204},
URL = {ftp://ftp.dcs.glasgow.ac.uk/pub/hug94/forster.ps.gz}
}
@INPROCEEDINGS{AnInInL,
AUTHOR = {D. A. Fura and A. K. Somani},
TITLE = {An Interpreter Interface Language: From Its Formal
Embedding in Higher-Order Logic to Its Role in
Better Simulation Practices},
BOOKTITLE = {Supplementary Proceedings of the 7th International Workshop on Higher
Order Logic Theorem Proving and its Applications},
EDITOR = {T. F. Melham and J. Camilleri},
PUBLISHER = {University of Malta, Valletta},
YEAR = {1994},
URL = {ftp://ftp.dcs.glasgow.ac.uk/pub/hug94/fura.ps.gz}
}
@INPROCEEDINGS{IntSem,
AUTHOR = {D. A. Fura and A. K. Somani},
TITLE = {Intervel-Semantic Component Models and the Efficient
Verification of Transaction-Level Circuit Behavior},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {205--220}
}
@INPROCEEDINGS{AbsTech,
AUTHOR = {D. A. Fura and P. J. Windley and A. K. Somani},
TITLE = {Abstraction Techniques for Modeling Real-World Interface Chips},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {267--280}
}
@INPROCEEDINGS{AnHOLTheo,
AUTHOR = {J. W. Gambles and P. J. Windley},
TITLE = {An {HOL} Theory for Logic States with Indeterminate Strengths},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {96--103}
}
@INPROCEEDINGS{ImRealTP,
AUTHOR = {R. Gerber and E. L. Gunter and I. Lee},
TITLE = {Implementing a Real-Time Process Algebra in {HOL}},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {144--154}
}
@INPROCEEDINGS{TheForDefSyn,
AUTHOR = {A. Gordon},
TITLE = {The Formal Definition of a Synchronous Hardware-Description
Language in Higher Order Logic},
BOOKTITLE = {1992 IEEE International Conference on Computer Design: {VLSI} in
Computers {\&} Processors},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {531--534},
URL = {ftp://ftp.cl.cam.ac.uk/papers/adg/iccd92.dvi.gz}
}
@INPROCEEDINGS{MechNam,
AUTHOR = {A. Gordon},
TITLE = {A Mechanisation of Name-carrying Syntax up to Alpha-conversion},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {413--425},
URL = {ftp://ftp.cl.cam.ac.uk/papers/adg/hug93.dvi.gz}
}
@TECHREPORT{MeDeSH,
AUTHOR = {A. Gordon},
TITLE = {A Mechanised Definition of {SILAGE} in {HOL}},
NUMBER = {287},
INSTITUTION = {Computer Laboratory, University of Cambridge},
MONTH = {February},
YEAR = {1993},
URL = {ftp://ftp.cl.cam.ac.uk/papers/adg/TR287-adg-silage.dvi.gz}
}
@INPROCEEDINGS{FiveAx,
AUTHOR = {A. D. Gordon and T. Melham},
TITLE = {Five Axioms of Alpha-Conversion},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International Conference,
{T}urku, {F}inland, {A}ugust 1996: Proceedings},
EDITOR = {J. von Wright and J. Grundy and J. Harrison},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1125},
PUBLISHER = {Springer-Verlag},
YEAR = {1996},
PAGES = {173--190}
}
@TECHREPORT{HOLMachOF,
AUTHOR = {M. Gordon},
TITLE = {{HOL}: A Machine Oriented Formulation of Higher Order Logic},
NUMBER = {68},
INSTITUTION = {Computer Laboratory, University of Cambridge},
MONTH = {July},
YEAR = {1985}
}
@INCOLLECTION{HOLProGenS,
AUTHOR = {M. J. C. Gordon},
TITLE = {{HOL}: A Proof Generating System for Higher-Order Logic},
BOOKTITLE = {Current Trends in Hardware Verification and Automated Theorem Proving},
EDITOR = {G. Birtwistle and P. A. Subrahmanyam},
PUBLISHER = {Springer-Verlag},
YEAR = {1989},
PAGES = {73-128}
}
@INPROCEEDINGS{IntrotoHOL,
AUTHOR = {M. Gordon},
TITLE = {Introduction to the {HOL} System},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {2--3}
}
@INCOLLECTION{AMechHoLo,
AUTHOR = {M. Gordon},
TITLE = {A Mechanized Hoare Logic of State Transitions},
BOOKTITLE = {A Classical Mind: Essays in Honour of C. A. R. Hoare},
EDITOR = {A. W. Roscoe },
PUBLISHER = {Prentice-Hall},
YEAR = {1994},
PAGES = {143--159},
URL = {http://www.cl.cam.ac.uk/ftp/hvg/papers/HoareLogicPaper.ps.gz}
}
@INCOLLECTION{MecProLoHO,
AUTHOR = {M. J. C. Gordon},
TITLE = {Mechanizing Programming Logics in Higher Order Logic},
BOOKTITLE = {Current Trends in Hardware Verification and Automated Theorem Proving},
EDITOR = {G. Birtwistle and P. A. Subrahmanyam},
PUBLISHER = {Springer-Verlag},
YEAR = {1989},
PAGES = {387--439},
URL = {ftp://ftp.cl.cam.ac.uk/hvg/papers/Banffpaper.dvi.gz}
}
@TECHREPORT{MerHOLST,
AUTHOR = {M. J. C. Gordon},
TITLE = {Merging {HOL} with Set Theory: preliminary experiments},
NUMBER = {353},
INSTITUTION = {Computer Laboratory, University of Cambridge},
YEAR = {1994},
URL = {http://www.cl.cam.ac.uk/users/mjcg/papers/HOLst/HOLst.ps.gz}
}
@INPROCEEDINGS{SemChallVer,
AUTHOR = {M. Gordon},
TITLE = {The Semantic Challenge of Verilog {HDL}},
BOOKTITLE = {Proceedings, Tenth Annual {IEEE} Symposium on Logic in Computer Science},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1995},
PAGES = {136--145},
URL = {http://www.cl.cam.ac.uk/ftp/hvg/papers/Verilog.ps.gz}
}
@INPROCEEDINGS{SetTheoHOL,
AUTHOR = {M. Gordon},
TITLE = {Set Theory, Higher Order Logic or Both?},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International Conference,
{T}urku, {F}inland, {A}ugust 1996: Proceedings},
EDITOR = {J. von Wright and J. Grundy and J. Harrison},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1125},
PUBLISHER = {Springer-Verlag},
YEAR = {1996},
PAGES = {191--201}
}
@INCOLLECTION{StTrAs,
AUTHOR = {M. J. C. Gordon},
TITLE = {State Transition Assertions: A Case Study},
BOOKTITLE = {Towards Verified Systems},
EDITOR = {J. Bowen},
SERIES = {Real-Time Safety Critical Systems Series},
VOLUME = {2},
PUBLISHER = {Elsevier},
YEAR = {1994},
PAGES = {93-113}
}
@INPROCEEDINGS{Avertiman,
AUTHOR = {M. J. C. Gordon},
TITLE = {A verifier and timing analyser for simple imperative programs (abstract)},
BOOKTITLE = {Computer Aided Verification: 5th International Conference,
{CAV}'93: {E}lounda, {G}reece: Proceedings},
EDITOR = {C. Courcoubetis},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {697},
PUBLISHER = {Springer-Verlag},
YEAR = {1993},
PAGES = {320}
}
@INPROCEEDINGS{WhyHOLisGoFo,
AUTHOR = {M. Gordon},
TITLE = {Why Higher-Order Logic is a Good Formalism for Specifying and
Verifying Hardware},
BOOKTITLE = {Formal Aspects of {VLSI} Design Proceedings of the
1985 {E}dinburgh Conference on {VLSI}},
EDITOR = {G. J. Milne and P. A. Subrahmanyam},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {North-Holland},
YEAR = {1986},
PAGES = {153--177}
}
@INPROCEEDINGS{FoVeCL,
AUTHOR = {M. Gordon and P. Loewenstein and M. Shahaf},
TITLE = {Formal Verification of a Cell Library: a case study in technology
transfer},
BOOKTITLE = {Formal {VLSI} Correctness Verification: {VLSI} Design Methods-{II}:
Proceedings of the {IFIP WG 10.2/WG1} 0.5 International Workshop
on Applied Formal Methods for {VLSI} Design, {B}elgium, {N}ovember 1989},
EDITOR = {L. J. M. Claesen},
PUBLISHER = {North-Holland},
YEAR = {1990},
PAGES = {409--417}
}
@BOOK{IntrotoHAT,
EDITOR = {M. J. C. Gordon and T. F. Melham},
TITLE = {Introduction to {HOL}: A theorem proving environment for
higher order logic},
PUBLISHER = {Cambridge University Press},
YEAR = {1993},
URL = {http://www.dcs.glasgow.ac.uk/~tfm/HOLbook.html}
}
@INCOLLECTION{HOLLOSys,
AUTHOR = {M. J. C. Gordon and A. M. Pitts},
TITLE = {The {HOL} Logic and System},
BOOKTITLE = {Towards Verified Systems},
EDITOR = {J. Bowen},
SERIES = {Real-Time Safety Critical Systems Series},
VOLUME = {2},
PUBLISHER = {Elsevier},
YEAR = {1994},
PAGES = {49--70}
}
@INPROCEEDINGS{InterpNODEN,
AUTHOR = {B. T. Graham},
TITLE = {An Interpretation of {NODEN} in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {221--234}
}
@MASTERSTHESIS{SECDDesVer,
AUTHOR = {B. T. Graham},
TITLE = {{SECD}: The Design and Verification of a Functional
Microprocessor},
SCHOOL = {Department of Computer Science, University of Calgary},
MONTH = {June},
YEAR = {1990}
}
@BOOK{TheSECD,
AUTHOR = {B. T. Graham},
TITLE = {The {SECD} Microprocessor: A Verification Case Study},
PUBLISHER = {Kluwer},
YEAR = {1992}
}
@INPROCEEDINGS{ForDesSECD,
AUTHOR = {B. Graham and G. Birtwistle},
TITLE = {Formalising the Design of an {SECD} chip},
BOOKTITLE = {Hardware Specification, Verification and Synthesis: Mathematical
Aspects: Mathematical Sciences Institute Workshop,
{C}ornell, {J}uly 1989},
EDITOR = {M. Leeser and G. Brown},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {408},
PUBLISHER = {Springer-Verlag},
YEAR = {1990},
PAGES = {40--66}
}
@INPROCEEDINGS{AlPrAss,
AUTHOR = {R. Groenboom and C. Hendriks and I. Polak and J. Terlouw and J. T. Udding},
TITLE = {Algebraic Proof Assistants in {HOL}},
BOOKTITLE = {Mathematics of Program Construction: Third International
Conference, {MPC}'95: {K}loster {I}rsee, {J}uly 1995:
Proceedings},
EDITOR = {B. M{\"{o}}ller},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {947},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {304--321},
URL = {http://www.cs.rug.nl/~indra/APA.dvi.Z}
}
@TECHREPORT{MethProgRe,
AUTHOR = {J. Grundy},
TITLE = {A Method of Program Refinement},
NUMBER = {318},
INSTITUTION = {Computer Laboratory, University of Cambridge},
MONTH = {November},
YEAR = {1993},
URL = {http://www.abo.fi/~jgrundy/thesis/thesis.html}
}
@INPROCEEDINGS{WinInfinHOLS,
AUTHOR = {J. Grundy},
TITLE = {Window Inference in the {HOL} System},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {177--189},
URL = {http://www.abo.fi/~jgrundy/hug91/hug91.html}
}
@INPROCEEDINGS{WinInfToo,
AUTHOR = {J. Grundy},
TITLE = {A Window Inference Tool for Refinement},
BOOKTITLE = {Proceedings of the 5th Refinement Workshop},
EDITOR = {C. B. Jones and B. T. Denvir and Roger C. F. Shaw},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {947},
PUBLISHER = {Springer-Verlag},
YEAR = {1992},
PAGES = {240--254},
URL = {http://www.abo.fi/~jgrundy/rw92/rw92.html}
}
@INPROCEEDINGS{RecHol,
AUTHOR = {Jim Grundy and Thomas L{\aa}ngbacka},
EDITOR = {Michael Johnson},
BOOKTITLE = {Algebraic Methodology and Software Technology:
6th International Conference, AMAST'97},
TITLE = {Recording {HOL} Proofs in a Structured Browsable Format},
VOLUME = {1349},
PUBLISHER = {Springer-Verlag},
ADDRESS = {Sydney, Australia},
PAGES = {567--571},
MONTH = DEC,
YEAR = {1997},
SERIES = {Lecture Notes in Computer Science}
}
@TECHREPORT{ToBrowR,
AUTHOR = {J. Grundy and T. L{{\aa}}ngbacka},
TITLE = {Towards a Browsable Record of {HOL} Proofs},
NUMBER = {7},
INSTITUTION = {Turku Centre for Computer Science},
MONTH = {May},
YEAR = {1996},
URL = {http://www.abo.fi/~jgrundy/tucstr7/tucstr7.html}
}
@PROCEEDINGS{BroadClass,
AUTHOR = {E. L. Gunter},
TITLE = {A Broader Class of Trees for Recursive Type Definitions for {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {141--154}
}
@TECHREPORT{DoAlginST,
AUTHOR = {E. L. Gunter},
TITLE = {Doing Algebra in Simple Type Theory},
NUMBER = {MS-CIS-89-38},
INSTITUTION = {Department of Computer and Information Science,
Moore School of Engineering,University of Pennsylvania},
MONTH = {June},
YEAR = {1989},
NOTE = {Distributed with the {HOL} system in Training/studies/int\_mod/doing\_alg\_paper}
}
@INPROCEEDINGS{WhyWe,
AUTHOR = {E. L. Gunter},
TITLE = {Why We Can't have {SML} Style datatype Declarations in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {561--568}
}
@INPROCEEDINGS{InterfHOL,
AUTHOR = {E. L. Gunter and L. Libkin},
TITLE = {Interfacing {HOL}90 with a Functional Database Query Language},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah, {S}eptember 1995:
Proceedings},
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {170--185},
URL = {http://www.cl.cam.ac.uk/users/pc/hugvt95.html}
}
@INPROCEEDINGS{ProbSolvT,
AUTHOR = {M. Hagiya and H. Tanaka and M. Yamamoto and S. Nishizaki},
TITLE = {Problem Solving with Tactics},
BOOKTITLE = {Supplementary Proceedings of the 9th International Conference on
Theorem Proving in Higher Order Logics: {TPHOL}s'96},
EDITOR = {J. von Wright and J. Grundy and J. Harrison},
SERIES = {TUCS General Publication},
NUMBER = {1},
PUBLISHER = {Turku Centre for Computer Science},
MONTH = {August},
YEAR = {1996},
PAGES = {31--43},
URL = {http://www.abo.fi/~jharriso/supp-root.html}
}
@INCOLLECTION{ProCompi,
AUTHOR = {R. W. S. Hale},
TITLE = {Program Compilation},
BOOKTITLE = {Towards Verified Systems},
EDITOR = {J. Bowen},
SERIES = {Real-Time Safety Critical Systems Series},
VOLUME = {2},
PUBLISHER = {Elsevier},
YEAR = {1994},
PAGES = {131-146}
}
@INPROCEEDINGS{ReaAbSo,
AUTHOR = {R. Hale},
TITLE = {Reasoning about Software},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {52--58}
}
@ARTICLE{EmbTTSinHOL,
AUTHOR = {R. Hale and R. Cardell-Oliver and J. Herbert},
TITLE = {An Embedding of Timed Transition Systems in {HOL}},
JOURNAL = {Formal Methods in System Design},
VOLUME = {3},
NUMBER = {1--2},
MONTH = {August},
YEAR = {1993},
PAGES = {151--174}
}
@INCOLLECTION{TiTraS,
AUTHOR = {R. W. S. Hale and R. M. Cardell-Oliver and J. M. J. Herbert},
TITLE = {Timed Transition Systems},
BOOKTITLE = {Towards Verified Systems},
EDITOR = {J. Bowen},
SERIES = {Real-Time Safety Critical Systems Series},
VOLUME = {2},
PUBLISHER = {Elsevier},
YEAR = {1994},
PAGES = {71--90}
}
@INCOLLECTION{ReaTiPr,
AUTHOR = {R. W. S. Hale and H. Jifeng},
TITLE = {A Real-time Programming Language},
BOOKTITLE = {Towards Verified Systems},
EDITOR = {J. Bowen},
SERIES = {Real-Time Safety Critical Systems Series},
VOLUME = {2},
PUBLISHER = {Elsevier},
YEAR = {1994},
PAGES = {115--130}
}
@INPROCEEDINGS{SimMicFS,
AUTHOR = {K. M. Hall and P. J. Windley},
TITLE = {Simulating Microprocessors from Formal Specifications},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {507--525}
}
@ARTICLE{ExplGraPP,
AUTHOR = {W. A. Halang and B. Kr{\"{a}}mer and L. Trybus},
TITLE = {Exploiting a Graphical Programming Paradigm to
Facilitate Rigorous Verification of Embedded Software},
JOURNAL = {The Computer Journal},
VOLUME = {38},
NUMBER = {4},
YEAR = {1995},
PAGES = {301--309}
}
@ARTICLE{BiDeDi,
AUTHOR = {J. Harrison},
TITLE = {Binary Decision Diagrams as a {HOL} Derived Rule},
JOURNAL = {The Computer Journal},
VOLUME = {38},
NUMBER = {2},
MONTH = {July},
YEAR = {1995},
PAGES = {162--170},
URL = {http://www.oup.co.uk/oup/smj/journals/ed/titles/computer_journal/docs/journal_contents/Volume_38_Number_2/38.2.ps/harrison.ps}
}
@INPROCEEDINGS{BinDD,
AUTHOR = {J. Harrison},
TITLE = {Binary Decision Diagrams as a {HOL} Derived Rule},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {254--268}
}
@ARTICLE{ConstRN,
AUTHOR = {J. Harrison},
TITLE = {Constructing the Real Numbers in {HOL}},
JOURNAL = {Formal Methods in System Design},
VOLUME = {5},
NUMBER = {1--2},
MONTH = {July},
YEAR = {1994},
PAGES = {35--59},
URL = {http://www.cl.cam.ac.uk/users/jrh/papers/reals1.ps.gz}
}
@INPROCEEDINGS{ConRN,
AUTHOR = {J. Harrison},
TITLE = {Constructing the real numbers in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {145--164}
}
@INPROCEEDINGS{FiProoChe,
AUTHOR = {J. Harrison},
TITLE = {Finding proofs and checking proofs},
BOOKTITLE = {{ECAI}96: 12th European Conference on Artificial Intelligence,
Workshop on Representation of Mathematical Knowledge: Proceedings},
EDITOR = {H. Stoyan and K. Homann and S. Jacob and M. Kerber},
PUBLISHER = {Budapest},
YEAR = {1996},
URL = {http://www.cl.cam.ac.uk/users/jrh/papers/finding.html}
}
@INPROCEEDINGS{FloatPV,
AUTHOR = {J. Harrison},
TITLE = {Floating Point Verification in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah, {S}eptember 1995:
Proceedings},
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {186--199},
URL = {http://www.cl.cam.ac.uk/users/jrh/papers/fp.dvi.gz}
}
@PROCEEDINGS{DecPro,
AUTHOR = {J. Harrison},
TITLE = {A {HOL} Decision Procedure for Elementary Real Algebra},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {426--436},
URL = {http://www.cl.cam.ac.uk/users/jrh/papers/decision.dvi.gz}
}
@INPROCEEDINGS{IndDef,
AUTHOR = {J. Harrison},
TITLE = {Inductive Definitions: automation and applications},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah, {S}eptember 1995:
Proceedings},
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {200--213},
URL = {http://www.cl.cam.ac.uk/users/jrh/papers/ind.dvi.gz}
}
@TECHREPORT{MetaRefTP,
AUTHOR = {J. Harrison},
TITLE = {Metatheory and Reflection in Theorem Proving: A Survey and Critique},
NUMBER = {CRC-53},
INSTITUTION = {SRI International, Cambridge Computer Science Research Centre},
MONTH = {February},
YEAR = {1995},
URL = {http://www.cl.cam.ac.uk/users/jrh/papers/reflect.dvi.gz}
}
@INPROCEEDINGS{MizarMode,
AUTHOR = {J. Harrison},
TITLE = {A Mizar Mode for {HOL}},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International Conference,
{T}urku, {F}inland, {A}ugust 1996: Proceedings},
EDITOR = {J. von Wright and J. Grundy and J. Harrison},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1125},
PUBLISHER = {Springer-Verlag},
YEAR = {1996},
PAGES = {203--220}
}
@INPROCEEDINGS{MathMecLo,
AUTHOR = {J. Harrison},
TITLE = {Pure Mathematics in a Mechanized Logic},
BOOKTITLE = {Proceedings of the {F}innish Artificial Intelligence
Society Symposium: Logic, Mathematics and the Computer},
EDITOR = {C. Gefwert and P. Orponen and J. Sepp{\"{a}}nen},
SERIES = {Suomen Teko{\"{a}}lyseuran julkaisuja},
VOLUME = {14},
PUBLISHER = {Finnish Artificial Intelligence Society},
YEAR = {1996},
PAGES = {153--169},
URL = {http://www.cl.cam.ac.uk/users/jrh/papers/fais.html}
}
@INPROCEEDINGS{SAlgo,
AUTHOR = {J. Harrison},
TITLE = {{S}t{{\aa}}lmarck's Algorithm as a {HOL} Derived Rule},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International Conference,
{T}urku, {F}inland, {A}ugust 1996: Proceedings},
EDITOR = {J. von Wright and J. Grundy and J. Harrison},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1125},
PUBLISHER = {Springer-Verlag},
YEAR = {1996},
PAGES = {221--234}
}
@TECHREPORT{TProRN,
AUTHOR = {J. Harrison},
TITLE = {Theorem Proving with the Real Numbers},
NUMBER = {408},
INSTITUTION = {University of Cambridge Computer Laboratory},
YEAR = {1996},
URL = {http://www.cl.cam.ac.uk/users/jrh/papers/thesis.html}
}
@INPROCEEDINGS{RefVerHOL,
AUTHOR = {J. Harrison and K. Slind},
TITLE = {A Reference Version of {HOL}},
BOOKTITLE = {Proceedings of the 7th International Workshop on Higher
Order Logic Theorem Proving and its Applications},
EDITOR = {T. F. Melham and J. Camilleri},
PUBLISHER = {University of Malta, Valletta},
YEAR = {1994},
URL = {ftp://ftp.dcs.glasgow.ac.uk/pub/hug94/harrison.ps.gz}
}
@INPROCEEDINGS{ExHOL,
AUTHOR = {J. Harrison and L. Th{\'{e}}ry},
TITLE = {Extending the {HOL} Theorem Prover with a Computer Algebra
System to Reason About the Reals},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {174--184},
URL = {http://www.cl.cam.ac.uk/users/jrh/papers/maple.ps.gz}
}
@INPROCEEDINGS{ReaARea,
AUTHOR = {J. Harrison and L. Th{\'{e}}ry},
TITLE = {Reasoning About the Reals: the marriage of {HOL} and Maple},
BOOKTITLE = {Logic Programming and Automated Reasoning: 4th International
Conference, {S}t. {P}etersburg: Proceedings},
EDITOR = {A. Voronkov},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {698},
PUBLISHER = {Springer-Verlag},
YEAR = {1993},
PAGES = {351--353},
URL = {http://www.cl.cam.ac.uk/users/jrh/papers/marriage.ps.gz}
}
@INPROCEEDINGS{MeSeHOL,
AUTHOR = {W. L. Harrison},
TITLE = {Mechanizing Security in {HOL}},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {63--66}
}
@INPROCEEDINGS{HOLMechAS,
AUTHOR = {W. L. Harrison and M. A. Archer and K. N. Levitt},
TITLE = {A {HOL} Mechanization of The Axiomatic Semantics of a
Simple Distributed Programming Language},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {347--359}
}
@INPROCEEDINGS{ToAppCPV,
AUTHOR = {M. R. Heckman and C. Zhang and B. R. Becker and D. Peticolas and K. N. Levitt
and R. A. Olsson},
TITLE = {Towards Applying the Composition Principle to Verify a
Microkernel Operating System},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International Conference,
{T}urku, {F}inland, {A}ugust 1996: Proceedings},
EDITOR = {J. von Wright and J. Grundy and J. Harrison},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1125},
PUBLISHER = {Springer-Verlag},
YEAR = {1996},
PAGES = {235--250}
}
@ARTICLE{ReIHOL,
AUTHOR = {L. Henschen},
TITLE = {Review of Introduction to {HOL}, edited by {M}. {G}ordon
and {T}. {M}elham (Cambridge University Press, 1993},
JOURNAL = {Computing Reviews},
VOLUME = {35},
NUMBER = {8},
MONTH = {August},
YEAR = {1994},
PAGES = {400--401}
}
@PHDTHESIS{AppForMeDS,
AUTHOR = {J. M. J. Herbert},
TITLE = {Application of Formal Methods to Digital System Design},
SCHOOL = {University of Cambridge Computer Laboratory},
YEAR = {1986}
}
@INPROCEEDINGS{DealWTC,
AUTHOR = {J. Herbert},
TITLE = {Dealing With Temporal Complexity in Hardware Verification},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {13--21}
}
@INPROCEEDINGS{ForReaTF,
AUTHOR = {J. Herbert},
TITLE = {Formal Reasoning about the Timing and Function of Basic
Memory Devices},
BOOKTITLE = {Formal {VLSI} Correctness Verification: {VLSI} Design Methods-{II}:
Proceedings of the {IFIP WG 10.2/WG1} 0.5 International Workshop
on Applied Formal Methods for {VLSI} Design, {B}elgium, {N}ovember 1989},
EDITOR = {L. J. M. Claesen},
PUBLISHER = {North-Holland},
YEAR = {1990},
PAGES = {379--298}
}
@INCOLLECTION{AFraMi,
AUTHOR = {J. M. J. Herbert},
TITLE = {A Framework for Microprocessor Design},
BOOKTITLE = {Towards Verified Systems},
EDITOR = {J. Bowen},
SERIES = {Real-Time Safety Critical Systems Series},
VOLUME = {2},
PUBLISHER = {Elsevier},
YEAR = {1994},
PAGES = {149--165}
}
@INPROCEEDINGS{IncDFV,
AUTHOR = {J. Herbert},
TITLE = {Incremental Design and Formal Verification of Microcoded Microprocessors},
BOOKTITLE = {Theorem Provers in Circuit Design: Proceedings of the
{IFIP TC10/WG} 10.2 International Conference, {N}ijmegen, {J}une 1992},
EDITOR = {V. Stavridou and T. F. Melham and R. T. Boute},
SERIES = {IFIP Transactions A-10},
PUBLISHER = {North-Holland},
YEAR = {1992},
PAGES = {157--174},
URL = {http://www.cam.sri.com/tr/crc027/abstract.html}
}
@PHDTHESIS{TTTP,
AUTHOR = {P. V. Homeier},
TITLE = {Trustworthy Tools for Trustworthy Programs:
A Mechanically Verified Verification Condition
Generator for the Total Correctness of Procedures},
SCHOOL = {University of California Los Angeles},
MONTH = {June},
YEAR = {1995},
URL = {http://www.cs.ucla.edu/csd-grads-gs2/homeier/html/phd.html}
}
@INPROCEEDINGS{TrTTP,
AUTHOR = {P. V. Homeier and D. F. Martin},
TITLE = {Trustworthy Tools for Trustworthy Programs: Automatic Verification of
Mutually Recursive Procedures},
BOOKTITLE = {Supplementary Proceedings of the 7th International Workshop on Higher
Order Logic Theorem Proving and its Applications},
EDITOR = {T. F. Melham and J. Camilleri},
PUBLISHER = {University of Malta, Valletta},
YEAR = {1994},
URL = {ftp://ftp.dcs.glasgow.ac.uk/pub/hug94/homeier.ps.gz}
}
@INPROCEEDINGS{TrustTool,
AUTHOR = {P. V. Homeier and D. F. Martin},
TITLE = {Trustworthy Tools for Trustworthy Programs: A Verified Verification
Condition Generator},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {269--284},
URL = {ftp://ftp.cs.ucla.edu/pub/homeier/papers/vvcg.ps.Z}
}
@ARTICLE{VerVerCon,
AUTHOR = {P. V. Homeier and D. F. Martin},
TITLE = {A Verified Verification Condition Generator},
JOURNAL = {The Computer Journal},
VOLUME = {38},
NUMBER = {2},
MONTH = {July},
YEAR = {1995},
PAGES = {131--141},
URL = {http://www.oup.co.uk/oup/smj/journals/ed/titles/computer_journal/docs/journal_contents/Volume_38_Number_2/38.2.ps/martin.ps}
}
@INPROCEEDINGS{ImpMath,
AUTHOR = {D. J. Howe},
TITLE = {Importing Mathematics from {HOL} into {N}uprl},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International Conference,
{T}urku, {F}inland, {A}ugust 1996: Proceedings},
EDITOR = {J. von Wright and J. Grundy and J. Harrison},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1125},
PUBLISHER = {Springer-Verlag},
YEAR = {1996},
PAGES = {267--281}
}
@PHDTHESIS{MachAssR,
AUTHOR = {M. A. Hutchins},
TITLE = {Machine Assisted Reasoning about Standard {ML} Using {HOL}},
SCHOOL = {Australian National University},
MONTH = {November},
YEAR = {1990}
}
@ARTICLE{RevInHOL,
AUTHOR = {G. Hutton},
TITLE = {Review of Introduction to {HOL}, edited by {M}. {G}ordon and
{T}. {M}elham ({C}ambridge University Press, 1993)},
JOURNAL = {Journal of Functional Programming},
VOLUME = {4},
NUMBER = {4},
MONTH = {October},
YEAR = {1994},
PAGES = {557--559}
}
@INPROCEEDINGS{ProAlgforISA,
AUTHOR = {S. Ikram and S.-K. Chin},
TITLE = {A Process Algebra for Instruction-Set Architecture Design},
BOOKTITLE = {{HOL}-95: International Workshop on Higher Order Logic Theorem
Proving and its Applications: {B}-Track: Short Presentations,
{A}spen {G}rove, {U}tah, {S}eptember, 1995},
EDITOR = {J. Alves-Foss},
YEAR = {1995},
PAGES = {33--44},
URL = {http://lal.cs.byu.edu/lal/{HOL}95/Bprocs/ikram.ps}
}
@INPROCEEDINGS{TranDepTT,
AUTHOR = {B. Jacobs and T. Melham},
TITLE = {Translating Dependent Type Theory into Higher Order Logic},
BOOKTITLE = {Typed Lambda Calculi and Applications: Proceedings of the
International Conference, {U}trecht, {M}arch 1993},
EDITOR = {M. Bezem and J. F. Groote},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {664},
PUBLISHER = {Springer-Verlag},
YEAR = {1993},
PAGES = {209--229},
URL = {ftp://ftp.dcs.glasgow.ac.uk/pub/users/tfm/Papers/DTTinHOL.ps}
}
@PHDTHESIS{RepAbTh,
AUTHOR = {M. D. Jones},
TITLE = {Representing Abstract Theories using Predicate Types},
SCHOOL = {Brigham Young University},
MONTH = {June},
YEAR = {1997},
URL = {http://www.cs.utah.edu/~mjones/papers/byu.thesis.ps.gz}
}
@INPROCEEDINGS{ToFrameDES,
AUTHOR = {M. D. Jones and T. N. Larson and P. J. Windley},
TITLE = {Toward {GHDL\_EVAL}: A Framework for Deeply Embedding Simple {HDL}s
in {HOL}},
BOOKTITLE = {Supplementary Proceedings of the 9th International Conference on
Theorem Proving in Higher Order Logics: {TPHOL}s'96},
EDITOR = {J. von Wright and J. Grundy and J. Harrison},
SERIES = {TUCS General Publication},
NUMBER = {1},
PUBLISHER = {Turku Centre for Computer Science},
MONTH = {August},
YEAR = {1996},
PAGES = {45--56},
URL = {http://www.abo.fi/~jharriso/supp-root.html}
}
@INCOLLECTION{FoVerImpMi,
AUTHOR = {J. J. Joyce},
TITLE = {Formal Verification and Implementation of a Microprocessor},
BOOKTITLE = {Current Trends in Hardware Verification and Automated Theorem Proving},
EDITOR = {G. Birtwistle and P. A. Subrahmanyam},
PUBLISHER = {Springer-Verlag},
YEAR = {1989},
PAGES = {129-157}
}
@INPROCEEDINGS{GenSpeDig,
AUTHOR = {J. J. Joyce},
TITLE = {Generic Specification of Digital Hardware},
BOOKTITLE = {Designing Correct Circuits: {S}eptember 1990, {O}xford},
EDITOR = {G. Jones and M. Sheeran},
SERIES = {Workshops in Computing Series},
PUBLISHER = {Springer-Verlag},
YEAR = {1991},
PAGES = {68--91}
}
@TECHREPORT{MulLevVerM,
AUTHOR = {J. J. Joyce},
TITLE = {Multi-Level Verification of Microprocessor-Based Systems},
NUMBER = {195},
INSTITUTION = {University of Cambridge Computer Laboratory},
MONTH = {May},
YEAR = {1990}
}
@INPROCEEDINGS{ToVeSyLVS,
AUTHOR = {J. J. Joyce},
TITLE = {Totally Verified Systems: Linking Verified Software to
Verified Hardware},
BOOKTITLE = {Hardware Specification, Verification and Synthesis: Mathematical
Aspects: Mathematical Sciences Institute Workshop, {C}ornell, {J}uly 1989},
EDITOR = {M. Leeser and G. Brown},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {408},
PUBLISHER = {Springer-Verlag},
YEAR = {1990},
PAGES = {177--201}
}
@PROCEEDINGS{HOLTPA,
EDITOR = {J. J. Joyce and C.-J. H. Seger},
TITLE = {Higher Order Logic Theorem Proving and its Applications: 6th
International Workshop, {HUG}'93, {V}ancouver, {B.C}.,
{A}ugust 11--13 1993: Proceedings},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994}
}
@INPROCEEDINGS{HOLVos,
AUTHOR = {J. Joyce and C. Seger},
TITLE = {The {HOL}-Voss System: Model-Checking inside a General-Purpose
Theorem-Prover},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {185--198}
}
@ARTICLE{AFSP,
AUTHOR = {S. Kalvala},
TITLE = {Annotations in Formal Specifications and Proofs},
JOURNAL = {Formal Methods in System Design},
VOLUME = {5},
NUMBER = {1--2},
MONTH = {July},
YEAR = {1994},
PAGES = {119--144}
}
@INPROCEEDINGS{DevIntforH,
AUTHOR = {S. Kalvala},
TITLE = {Developing an Interface for {HOL}},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {305--317}
}
@INPROCEEDINGS{HOLArWor,
AUTHOR = {S. Kalvala},
TITLE = {{HOL} Around the World},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {4--12}
}
@INPROCEEDINGS{ImpUseA,
AUTHOR = {S. Kalvala and M. Archer and K. Levitt},
TITLE = {Implementation and Use of Annotations in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {407--426}
}
@INPROCEEDINGS{ForVerSer,
AUTHOR = {J. D. Kim and S.-K. Chin},
TITLE = {Formal Verification of Serial Pipeline Multipliers},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah, {S}eptember 1995:
Proceedings},
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {229--244}
}
@INPROCEEDINGS{EmHaVeCDF,
AUTHOR = {T. Kropf and R. Kumar and K. Schneider},
TITLE = {Embedding Hardware Verification within a Commercial Design
Framework},
BOOKTITLE = {Correct Hardware Design and Verification Methods:
{IFIP WG}10.2 Advanced Research Working Conference: Proceedings},
EDITOR = {G. J. Milne and L. Pierre},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {683},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {242--257},
URL = {http://goethe.ira.uka.de/hvg/techreports/SFB358-C2-6-93.ps.gz}
}
@INPROCEEDINGS{AForFra,
AUTHOR = {T. Kropf and K. Schneider and R. Kumar},
TITLE = {A Formal Framework for High Level Synthesis},
BOOKTITLE = {Theorem Provers in Circuit Design: Theory, Practice and
Experience: Proceedings},
EDITOR = {R. Kumar and T. Kropf},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {901},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {223--238},
URL = {http://goethe.ira.uka.de/hvg/techreports/SFB358-C2-5-94.ps.gz}
}
@INPROCEEDINGS{FirstStTAH,
AUTHOR = {R. Kumar and T. Kropf and K. Schneider},
TITLE = {First Steps Towards Automating Hardware Proofs in {HOL}},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {190--193}
}
@INPROCEEDINGS{InaFirOA,
AUTHOR = {R. Kumar and T. Kropf and K. Schneider},
TITLE = {Integrating a First-Order Automatic Prover in the {HOL} Environment},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {170--176}
}
@ARTICLE{StructAHP,
AUTHOR = {R. Kumar and K. Schneider and T. Kropf},
TITLE = {Structuring and Automating Hardware Proofs in a Higher-Order
Theorem-Proving Environment},
JOURNAL = {Formal Methods in System Design},
VOLUME = {2},
NUMBER = {2},
MONTH = {April},
YEAR = {1993},
PAGES = {165--223}
}
@INPROCEEDINGS{UslatTheo,
AUTHOR = {L. Laibinis},
TITLE = {Using Lattice Theory in Higher Order Logic},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International Conference,
{T}urku, {F}inland, {A}ugust 1996: Proceedings},
EDITOR = {J. von Wright and J. Grundy and J. Harrison},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1125},
PUBLISHER = {Springer-Verlag},
YEAR = {1996},
PAGES = {315--330}
}
@INPROCEEDINGS{HOLForm,
AUTHOR = {T. L{{\aa}}ngbacka},
TITLE = {A {HOL} Formalisation of the Temporal Logic of Actions},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {332--345}
}
@INPROCEEDINGS{TkWinHOL,
AUTHOR = {T. L{{\aa}}ngbacka and R. Ruksenas and J. von Wright},
TITLE = {{T}k{W}in{HOL}: A Tool for Window Inference in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah, {S}eptember 1995:
Proceedings},
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {245--260}
}
@ARTICLE{EngAppFDS,
AUTHOR = {M. Larsson},
TITLE = {An Engineering Approach to Formal Digital System Design},
JOURNAL = {The Computer Journal},
VOLUME = {38},
NUMBER = {2},
MONTH = {July},
YEAR = {1995},
PAGES = {101--110},
URL = {http://www.oup.co.uk/oup/smj/journals/ed/titles/computer_journal/docs/journal_contents/Volume_38_Number_2/38.2.ps/larsson.ps}
}
@INPROCEEDINGS{EngApp,
AUTHOR = {M. Larsson},
TITLE = {An Engineering Approach to Formal Digital System Design},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {300--315}
}
@INPROCEEDINGS{ImpResHLS,
AUTHOR = {M. Larsson},
TITLE = {Improving the Result of High-Level Synthesis Using
Interactive Transformational Design},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International Conference,
{T}urku, {F}inland, {A}ugust 1996: Proceedings},
EDITOR = {J. von Wright and J. Grundy and J. Harrison},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1125},
PUBLISHER = {Springer-Verlag},
YEAR = {1996},
PAGES = {299--314}
}
@PHDTHESIS{TransApptoFo,
AUTHOR = {M. Larsson},
TITLE = {A Transformational Approach to Formal Digital System Design},
SCHOOL = {Department of Computer and Information Science, Link{\"{o}}ping University},
MONTH = {May},
YEAR = {1993},
NOTE = {Licentiate of Engineering Dissertation, Thesis number 378}
}
@INPROCEEDINGS{AHOLEmbSP,
AUTHOR = {M. Larsson and A. D. Gordon},
TITLE = {A {HOL} Embedding of a Small Parallel {HDL}},
BOOKTITLE = {{HOL}-95: International Workshop on Higher Order Logic Theorem
Proving and its Applications: {B}-Track: Short Presentations,
{A}spen {G}rove, {U}tah, {S}eptember, 1995},
EDITOR = {J. Alves-Foss},
YEAR = {1995},
PAGES = {45--60},
URL = {http://lal.cs.byu.edu/lal/HOL95/Bprocs/larsson.ps}
}
@ARTICLE{ForTheSim,
AUTHOR = {P. Loewenstein},
TITLE = {A Formal Theory of Simulations Between Infinite Automata},
JOURNAL = {Formal Methods in System Design},
VOLUME = {August},
YEAR = {1993},
PAGES = {35--59},
URL = {117--149}
}
@INPROCEEDINGS{FormTheoSBI,
AUTHOR = {P. Loewenstein},
TITLE = {A Formal Theory of Simulations Between Infinite Automata},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {{IFIP} Transactions {A}-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {227--246}
}
@INPROCEEDINGS{ForVerCPA,
AUTHOR = {P. Loewenstein},
TITLE = {Formal Verification of Counterflow Pipeline Architecture},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah, {S}eptember 1995:
Proceedings},
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {261--276},
URL = {http://www.sunlabs.com/techrep/1996/abstract-53.html}
}
@INPROCEEDINGS{LearnUH,
AUTHOR = {P. Loewenstein},
TITLE = {Learning to use {HOL}},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {67--74}
}
@INPROCEEDINGS{ReStMachH,
AUTHOR = {P. Loewenstein},
TITLE = {Reasoning about State Machines in Higher-Order Logic},
BOOKTITLE = {Hardware Specification, Verification and Synthesis: Mathematical
Aspects: Mathematical Sciences Institute Workshop, {C}ornell, {J}uly 1989},
EDITOR = {M. Leeser and G. Brown},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {408},
PUBLISHER = {Springer-Verlag},
YEAR = {1990},
PAGES = {67--89}
}
@INPROCEEDINGS{TempTranSM,
AUTHOR = {P. Loewenstein},
TITLE = {Temporal Transformation of State Machines Using Higher Order Logic},
BOOKTITLE = {Formal {VLSI} Correctness Verification: {VLSI} Design Methods-{II}:
Proceedings of the {IFIP WG 10.2/WG1} 0.5 International Workshop
on Applied Formal Methods for {VLSI} Design, {B}elgium, {N}ovember 1989},
EDITOR = {L. J. M. Claesen},
PUBLISHER = {North-Holland},
YEAR = {1990},
PAGES = {171--186}
}
@ARTICLE{VerMultCP,
AUTHOR = {P. Loewenstein and D. L. Dill},
TITLE = {Verification of a Multiprocessor Cache Protocol using
Simulation Relations and Higher-Order Logic},
JOURNAL = {Formal Methods in System Design},
VOLUME = {1},
NUMBER = {4},
MONTH = {December},
YEAR = {1992},
PAGES = {355--383}
}
@INPROCEEDINGS{VerofMuCa,
AUTHOR = {P. Loewenstein and D. L. Dill},
TITLE = {Verification of a Multiprocessor Cache Protocol using
Simulation Relations and Higher-Order Logic},
BOOKTITLE = {Computer-Aided Verifiction: 2nd International Conference,
{CAV}'90: {N}ew {B}runswick, 1990: Proceedings},
EDITOR = {E. M. Clarke and R. P. Kurshan},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {531},
PUBLISHER = {Springer-Verlag},
YEAR = {1991},
PAGES = {302--311}
}
@INPROCEEDINGS{GenDesAR,
AUTHOR = {J.-Y. Lu and S.-K. Chin},
TITLE = {Generating Designs Using an Algorithmic Register Transfer Language
with Formal Semantics},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {316--331}
}
@INPROCEEDINGS{LinkHOL,
AUTHOR = {J.-Y. Lu and S.-K. Chin},
TITLE = {Linking Higher Order Logic to a {VLSI CAD} System},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {199--212}
}
@INPROCEEDINGS{MacAbMic,
AUTHOR = {M. McAllister},
TITLE = {Machine Abstraction in Microprocessor Specification},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {211--224}
}
@ARTICLE{FangsVI,
AUTHOR = {D. MacKenzie},
TITLE = {The fangs of the {VIPER}},
JOURNAL = {Nature},
VOLUME = {352},
MONTH = {August},
YEAR = {1991},
PAGES = {467--468}
}
@ARTICLE{StudMLM,
AUTHOR = {S. Maharaj and E. Gunter},
TITLE = {Studying the {ML} Module System in {HOL}},
JOURNAL = {The Computer Journal},
VOLUME = {38},
NUMBER = {2},
MONTH = {July},
YEAR = {1995},
PAGES = {142--151},
URL = {http://www.oup.co.uk/oup/smj/journals/ed/titles/computer_journal/docs/journal_contents/Volume_38_Number_2/38.2.ps/gunter.ps}
}
@INPROCEEDINGS{StudML,
AUTHOR = {S. Maharaj and E. Gunter},
TITLE = {Studying the {ML} Module System in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {346--361}
}
@INPROCEEDINGS{CaseSCC,
AUTHOR = {D. F. Martin and R. J. Toal},
TITLE = {Case Studies in Compiler Correctness Using {HOL}},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {242--252}
}
@INCOLLECTION{AbMeHV,
AUTHOR = {T. Melham},
TITLE = {Abstraction Mechanisms for Hardware Verification},
BOOKTITLE = {{VLSI} Specification, Verification and Synthesis},
EDITOR = {G. Birtwistle and P. A. Subrahmanyam},
PUBLISHER = {Kluwer},
YEAR = {1988},
PAGES = {267--291}
}
@INCOLLECTION{AuReTyD,
AUTHOR = {T. F. Melham},
TITLE = {Automating Recursive Type Definitions in Higher Order Logic},
BOOKTITLE = {Current Trends in Hardware Verification and Automated Theorem Proving},
EDITOR = {G. Birtwistle and P. A. Subrahmanyam},
PUBLISHER = {Springer-Verlag},
YEAR = {1989},
PAGES = {341-386},
URL = {ftp://ftp.dcs.glasgow.ac.uk/pub/users/tfm/Papers/TR146.ps.gz}
}
@TECHREPORT{ForAbMechHV,
AUTHOR = {T. F. Melham},
TITLE = {Formalizing Abstraction Mechanisms for Hardware Verification in
Higher Order Logic},
NUMBER = {201},
INSTITUTION = {University of Cambridge Computer Laboratory},
MONTH = {August},
YEAR = {1990}
}
@BOOK{HOLandHaV,
AUTHOR = {T. Melham},
TITLE = {Higher Order Logic and Hardware Verification},
SERIES = {Cambridge Tracts in Theoretical Computer Science},
VOLUME = {31},
PUBLISHER = {Cambridge University Press},
YEAR = {1993},
URL = {http://www.dcs.glasgow.ac.uk/~tfm/HVbook.html}
}
@ARTICLE{HOLLogEx,
AUTHOR = {T. F. Melham},
TITLE = {The {HOL} Logic Extended with Quantification over Type Variables},
JOURNAL = {Formal Methods in System Design},
VOLUME = {3},
NUMBER = {1--2},
MONTH = {August},
YEAR = {1992},
PAGES = {7--24},
URL = {ftp://ftp.dcs.glasgow.ac.uk/pub/users/tfm/Papers/TypeQuant.ps.gz}
}
@ARTICLE{MechThePi,
AUTHOR = {T. F. Melham},
TITLE = {A Mechanized Theory of the Pi-calculus in {HOL}},
JOURNAL = {Nordic Journal of Computing},
VOLUME = {1},
NUMBER = {1},
MONTH = {Spring},
YEAR = {1994},
PAGES = {50--76},
URL = {ftp://ftp.dcs.glasgow.ac.uk/pub/users/tfm/Papers/PIin{HOL}.ps.gz}
}
@INPROCEEDINGS{PacIndRel,
AUTHOR = {T. F. Melham},
TITLE = {A Package for Inductive Relation Definitions in {HOL}},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {350--357},
URL = {ftp://ftp.dcs.glasgow.ac.uk/pub/users/tfm/Papers/IndDefs.ps.gz}
}
@INPROCEEDINGS{URecTyp,
AUTHOR = {T. F. Melham},
TITLE = {Using Recursive Types to Reason about Hardware in Higher Order Logic},
BOOKTITLE = {The Fusion of Hardware Design and Verification: Proceedings of
the {IFIP WG} 10.2 Working Conference, {G}lasgow, {J}uly 1988},
EDITOR = {J. Staunstrup},
PUBLISHER = {North-Holland},
PAGES = {27--50},
YEAR = {1988},
URL = {ftp://ftp.dcs.glasgow.ac.uk/pub/users/tfm/Papers/TR135.ps.gz}
}
@PROCEEDINGS{HOLTP94,
EDITOR = {T. F. Melham and J. Camilleri},
TITLE = {Higher Order Logic Theorem Proving and Its Applications:
7th International Workshop, {V}alletta, {M}alta, {S}eptember 1994:
Proceedings},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
URL = {http://www.dcs.gla.ac.uk/~tfm/Papers,LNCS859.ps}
}
@PROCEEDINGS{SuppPr7,
EDITOR = {T. F. Melham and J. Camilleri},
TITLE = {Supplementary Proceedings of the 7th International Workshop
on Higher Order Logic Theorem Proving and its Applications},
PUBLISHER = {University of Malta, Valletta},
YEAR = {1994},
URL = {ftp://ftp.dcs.glasgow.ac.uk/~hug94/sproc.html}
}
@ARTICLE{TaggedUD,
AUTHOR = {S. W. Moore and B. T. Graham},
TITLE = {Tagged Up/Down Sorter-A Hardware Priority Queue},
JOURNAL = {The Computer Journal},
VOLUME = {38},
NUMBER = {9},
YEAR = {1996},
PAGES = {695--703}
}
@INPROCEEDINGS{SafeRail,
AUTHOR = {M. J. Morley},
TITLE = {Safety in Railway Signalling Data: A Behavioural Analysis},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {464--474}
}
@INPROCEEDINGS{MechaTheAu,
AUTHOR = {Munna and J. Alves-Foss},
TITLE = {Mechanizing a Theory of Authentication in Higher Order Logic},
BOOKTITLE = {{HOL}-95: International Workshop on Higher Order Logic Theorem
Proving and its Applications: {B}-Track: Short Presentations,
{A}spen {G}rove, {U}tah, {S}eptember, 1995},
EDITOR = {J. Alves-Foss},
YEAR = {1995},
PAGES = {61--72},
URL = {http://lal.cs.byu.edu/lal/HOL95/Bprocs/munna.ps}
}
@INPROCEEDINGS{UHOLPAP,
AUTHOR = {M. Mutz},
TITLE = {Using the {HOL} Prove Assistant for proving
the Correctness of Term Rewriting Rules reducing
Terms of Sequential Behaviour},
BOOKTITLE = {Computer Aided Verification: 3rd International
Workshop, {CAV}'91; {A}alborg, 1991: Proceedings},
EDITOR = {K. G. Larsen and A. Skou},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {575},
PUBLISHER = {Springer-Verlag},
YEAR = {1991},
PAGES = {277--287}
}
@INPROCEEDINGS{ForModLogCCS,
AUTHOR = {M. Nesi},
TITLE = {Formalizing a Modal Logic for CCS in the {HOL} Theorem Prover},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {279--294}
}
@INPROCEEDINGS{MeMoLo,
AUTHOR = {M. Nesi},
TITLE = {Mechanising a Modal Logic for Value-Passing Agents in {HOL}},
BOOKTITLE = {Proceedings of {INFINITY}, International Workshop on
Verification of Infinite State Systems,
{A}ugust 30--31, 1996, {P}isa, {I}taly},
EDITOR = {B. Steffen and T. Margaria},
YEAR = {1996},
PAGES = {139--148},
NOTE = {Technical Report MIP-9614, Universitat Passau}
}
@INPROCEEDINGS{MePrInd,
AUTHOR = {M. Nesi},
TITLE = {Mechanizing a Proof by Induction of Process Algebra
Specifications in Higher Order Logic},
BOOKTITLE = {Computer Aided Verification: 3rd International
Workshop, {CAV}'91; {A}alborg, 1991: Proceedings},
EDITOR = {K. G. Larsen and A. Skou},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {575},
PUBLISHER = {Springer-Verlag},
YEAR = {1991},
PAGES = {288--298}
}
@INPROCEEDINGS{ValuePas,
AUTHOR = {M. Nesi},
TITLE = {Value-Passing CCS in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {352--365}
}
@INPROCEEDINGS{ProoBaC,
AUTHOR = {M. C. Newey},
TITLE = {Proof Based Computation},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {380--383}
}
@TECHREPORT{AbsDynSemC,
AUTHOR = {Michael Norrish},
TITLE = {An abstract dynamic semantics for {C}},
INSTITUTION = {Computer Laboratory, University of Cambridge},
YEAR = {1997},
NUMBER = {421},
MONTH = {May}
}
@PHDTHESIS{CFormHOL,
AUTHOR = {Michael Norrish},
TITLE = {{C} formalised in {HOL}},
SCHOOL = {Computer Laboratory, University of Cambridge},
YEAR = {1998}
}
@INPROCEEDINGS{DetExpC,
AUTHOR = {Michael Norrish},
TITLE = {Deterministic expressions in C},
BOOKTITLE = {Programming languages and systems,
8th European Symposium on Programming},
EDITOR = {S. Doaitse Swierstra},
VOLUME = {1576},
SERIES = {Lecture Notes in Computer Science},
YEAR = {1999},
PUBLISHER = {Springer-Verlag},
ADDRESS = {Amsterdam},
MONTH = {March},
PAGES = {147--161},
NOTES = {Held as part of the Joint European Conferences on Theory
and Practice of Software, ETAPS'99}
}
@INPROCEEDINGS{DerVerR,
AUTHOR = {M. Norrish},
TITLE = {Derivation of Verification Rules for {C} from Operational Definitions},
BOOKTITLE = {Supplementary Proceedings of the 9th International Conference on
Theorem Proving in Higher Order Logics: {TPHOL}s'96},
EDITOR = {J. von Wright and J. Grundy and J. Harrison},
SERIES = {TUCS General Publication},
NUMBER = {1},
PUBLISHER = {Turku Centre for Computer Science},
MONTH = {August},
YEAR = {1996},
PAGES = {69--75},
URL = {http://www.abo.fi/~jharriso/supp-root.html}
}
@INPROCEEDINGS{ToForVerFP,
AUTHOR = {J. Pan and K. N. Levitt and M. Archer and S. Kalvala},
TITLE = {Towards a Formal Verificrtion of a Floating Point
Coprocessor and its Composition with a Central Processing Unit},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {427--447}
}
@INPROCEEDINGS{Graphmod,
AUTHOR = {K. D. Petersen},
TITLE = {Graph model of {LAMBDA} in Higher Order Logic},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {16-28}
}
@INPROCEEDINGS{DefVerIntCo,
AUTHOR = {D. E. Peterson and S.-K. Chin},
TITLE = {Definition and Verification of Interrupt Correctness Properties},
BOOKTITLE = {{HOL}-95: International Workshop on Higher Order Logic Theorem
Proving and its Applications: {B}-Track: Short Presentations,
{A}spen {G}rove, {U}tah, {S}eptember, 1995},
EDITOR = {J. Alves-Foss},
YEAR = {1995},
PAGES = {74--88},
URL = {http://lal.cs.byu.edu/lal/HOL95/Bprocs/peterson.ps}
}
@INPROCEEDINGS{ExtStaTran,
AUTHOR = {D. Peticolas and C. Zhang and B. R. Becker and M. R. Heckman and K. N. Levitt
and R. A. Olsson},
TITLE = {Extending a State Transition System with Real-Time Semantics},
BOOKTITLE = {Supplementary Proceedings of the 9th International Conference on
Theorem Proving in Higher Order Logics: {TPHOL}s'96},
EDITOR = {J. von Wright and J. Grundy and J. Harrison},
SERIES = {TUCS General Publication},
NUMBER = {1},
PUBLISHER = {Turku Centre for Computer Science},
MONTH = {August},
YEAR = {1996},
PAGES = {95--104},
URL = {http://www.abo.fi/~jharriso/supp-root.html}
}
@INPROCEEDINGS{DefRecFun,
AUTHOR = {W. Ploegaerts and L. Claesen and H. De Man},
TITLE = {Defining Recursive Functions in {HOL}},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {358--366}
}
@INPROCEEDINGS{MaVaLoHO,
AUTHOR = {I. Polak},
TITLE = {Many-valued Logic in {HOL}},
BOOKTITLE = {Proceedings Accolade '95},
EDITOR = {S. Fischer and M. Trautwein},
PUBLISHER = {Dutch Graduate School in Logic, Amsterdam},
YEAR = {1995},
PAGES = {113--127},
URL = {http://www.cs.rug.nl/OZSL/accolade/indra.ps.gz}
}
@INPROCEEDINGS{FormVar,
AUTHOR = {I.S.W.B. Prasetya},
TITLE = {Formalization of Variables Access Constraints to Support Compositionality
of Liveness Properties},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {324--337}
}
@PHDTHESIS{MeSupDeS,
AUTHOR = {I. S. W. B. Prasetya},
TITLE = {Mechanically Supported Design of Self-stabilising Algorithms},
SCHOOL = {University of Utrecht},
MONTH = {August},
YEAR = {1995},
URL = {ftp://ftp.cs.ruu.nl/pub/RUU/CS/phdtheses/Prasetya/}
}
@INPROCEEDINGS{StyleMP,
AUTHOR = {I. S. W. B. Prasetya},
TITLE = {On the Style of Mechanical Proving},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {475--488}
}
@INPROCEEDINGS{ToMechSup,
AUTHOR = {I. S. W. B. Prasetya},
TITLE = {Towards a Mechanically Supported and Compositional Calculus
to Design Distributed Algorithms},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {362--377}
}
@INPROCEEDINGS{ExecHOLS,
AUTHOR = {S. Rajan},
TITLE = {Executing {HOL} Specifications: Towards an Evaluation Semantics
for Classical Higher Order Logic},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {527--536}
}
@INPROCEEDINGS{AbstDat,
AUTHOR = {S. Rajan and J. Joyce and C.-J. Seger},
TITLE = {From Abstract Data Types to Shift Registers: A Case Study [...]},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {489--500}
}
@INPROCEEDINGS{FoProoCP,
AUTHOR = {S. R. Ramirez Chavez},
TITLE = {Formal Proof of the Cascading Properties of a Parallel Sorting Circuit},
BOOKTITLE = {Formal {VLSI} Correctness Verification: {VLSI} Design Methods-{II}:
Proceedings of the {IFIP WG 10.2/WG1} 0.5 International Workshop
on Applied Formal Methods for {VLSI} Design, {B}elgium, {N}ovember 1989},
EDITOR = {L. J. M. Claesen},
PUBLISHER = {North-Holland},
YEAR = {1990},
PAGES = {419--427}
}
@INPROCEEDINGS{DeepEmb,
AUTHOR = {R. Reetz},
TITLE = {Deep Embedding {VHDL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah,
{S}eptember 1995: Proceedings},
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {277--299},
URL = {http://goethe.ira.uka.de/hvg/techreports/SFB358-C2-2-95.ps.gz}
}
@INCOLLECTION{FloGrSem,
AUTHOR = {R. Reetz and T. Kropf},
TITLE = {A Flow Graph Semantics of {VHDL}: A Basis for
Hardware Verification with {VHDL}},
BOOKTITLE = {Formal Semantics for {VHDL}},
EDITOR = {C. D. Kloos and P. T. Breuer},
PUBLISHER = {Kluwer},
YEAR = {1995},
PAGES = {205--238}
}
@ARTICLE{FlowGrSem,
AUTHOR = {R. Reetz and T. Kropf},
TITLE = {A Flow Graph Semantics of {VHDL}: Towards a
{VHDL} Verification Workbench in {HOL}},
JOURNAL = {Formal Methods in System Design},
VOLUME = {7},
NUMBER = {1--2},
MONTH = {August},
YEAR = {1995},
PAGES = {73--100}
}
@INPROCEEDINGS{SimpDeep,
AUTHOR = {R. Reetz and T. Kropf},
TITLE = {Simplifying Deep Embedding: A Formalised Code Generator},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {378--390}
}
@INPROCEEDINGS{HOLPack,
AUTHOR = {R. E. O. Roxas},
TITLE = {A {HOL} Package for Reasoning about Relations Defined by
Mutual Induction},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {129--140}
}
@PHDTHESIS{ProCoPT,
AUTHOR = {R. E. O. Roxas},
TITLE = {Proving the Correctness of Program Transformations in Higher
Order Logic},
SCHOOL = {Australian National University},
MONTH = {April},
YEAR = {1994}
}
@INPROCEEDINGS{ProProTran,
AUTHOR = {R. Roxas and M. Newey},
TITLE = {Proof of Program Transformations},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {223--230}
}
@PHDTHESIS{EinSe,
AUTHOR = {K. Schneider},
TITLE = {Ein Sequenzenkalk{\"{u}}l f{\"{u}}r {HOL}},
SCHOOL = {Universit{\"{a}}t Karlsruhe},
YEAR = {1991}
}
@INPROCEEDINGS{VeHardCor,
AUTHOR = {K. Schneider and T. Kropf},
TITLE = {Verifying Hardware Correctness by Combining Theorem Proving
and Model Checking},
BOOKTITLE = {{HOL}-95: International Workshop on Higher Order Logic Theorem
Proving and its Applications: {B}-Track: Short Presentations,
{A}spen {G}rove, {U}tah, {S}eptember, 1995},
EDITOR = {J. Alves-Foss},
YEAR = {1995},
PAGES = {89--104},
URL = {http://lal.cs.byu.edu/lal/{HOL}95/Bprocs/schneider.ps}
}
@ARTICLE{AccTabP,
AUTHOR = {K. Schneider and R. Kumar and T. Kropf},
TITLE = {Accelerating Tableaux Proofs using Compact Representations},
JOURNAL = {Formal Methods in System Design},
VOLUME = {5},
NUMBER = {1--2},
MONTH = {July},
YEAR = {1994},
PAGES = {145--176}
}
@INPROCEEDINGS{AltProof,
AUTHOR = {K. Schneider and R. Kumar and T. Kropf},
TITLE = {Alternative Proof procedures for Finite-State Machines
in Higher-Order Logic},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {213--226},
URL = {http://goethe.ira.uka.de/hvg/techreports/SFB358-C2-8-93.ps.gz}
}
@INPROCEEDINGS{AuMoPaHP,
AUTHOR = {K. Schneider and R. Kumar and T. Kropf},
TITLE = {Automating Most Parts of Hardware Proofs in {HOL}},
BOOKTITLE = {Computer Aided Verification: 3rd International
Workshop, {CAV}'91; {A}alborg, 1991: Proceedings},
EDITOR = {K. G. Larsen and A. Skou},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {575},
PUBLISHER = {Springer-Verlag},
YEAR = {1991},
PAGES = {365--37}
}
@INPROCEEDINGS{AutVer,
AUTHOR = {K. Schneider and R. Kumar and T. Kropf},
TITLE = {Automating Verification by Functional Abstraction at the System Level},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {391--406},
URL = {http://goethe.ira.uka.de/hvg/techreports/SFB358-C2-13-94.ps.gz}
}
@INPROCEEDINGS{EffRepC,
AUTHOR = {K. Schneider and R. Kumar and T. Kropf},
TITLE = {Efficient Representation and Computation of Tableaux Proofs},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {39--57}
}
@INPROCEEDINGS{ElimHO,
AUTHOR = {K. Schneider and R. Kumar and T. Kropf},
TITLE = {Eliminating Higher-Order Quantifiers to Obtain
Decision Procedures for Hardware Verification},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {385--398},
URL = {http://goethe.ira.uka.de/hvg/techreports/SFB358-C2-9-93.ps.gz}
}
@INPROCEEDINGS{FAUSTPro,
AUTHOR = {K. Schneider and R. Kumar and T. Kropf},
TITLE = {The {FAUST}-Prover},
BOOKTITLE = {Automated Deduction - {CADE}--11: 11th International
Conference, Proceedings},
EDITOR = {D. Kapur},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {607},
PUBLISHER = {Springer-Verlag},
YEAR = {1992},
PAGES = {766--770}
}
@INPROCEEDINGS{ModGenHS,
AUTHOR = {K. Schneider and R. Kumar and T. Kropf},
TITLE = {Modelling Generic Hardware Structures by Abstract Datatypes},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {165--175}
}
@INPROCEEDINGS{StHaPF,
AUTHOR = {K. Schneider and R. Kumar and T. Kropf},
TITLE = {Structuring Hardware Proofs: First Steps Towards Automation in a
Higher-Order Environment},
BOOKTITLE = {Proceedings of the International Conference on {VLSI},{VLSI'91}},
EDITOR = {P. B. Denyer and A. Halaas},
PUBLISHER = {North-Holland},
YEAR = {1991}
}
@INPROCEEDINGS{WhyHarVerMod,
AUTHOR = {K. Schneider and R. Kumar and T. Kropf},
TITLE = {Why Hardware Verification needs more than Model Checking},
BOOKTITLE = {Supplementary Proceedings of the 7th International Workshop on Higher
Order Logic Theorem Proving and its Applications},
EDITOR = {T. F. Melham and J. Camilleri},
PUBLISHER = {University of Malta, Valletta},
YEAR = {1994},
URL = {ftp://ftp.dcs.glasgow.ac.uk/pub/hug94/schneider.ps.gz}
}
@INPROCEEDINGS{HybMoR,
AUTHOR = {E. T. Schubert},
TITLE = {A Hybrid Model for Reasoning about Composed Hardware Systems},
BOOKTITLE = {Computer Aided Verification: 6th International Conference:
Proceedings},
EDITOR = {D. L. Dill},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {818},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {260--272},
URL = {ftp://ftp.cs.pdx.edu/pub/faculty/schubert/cav.ps.Z}
}
@INPROCEEDINGS{VerCoHaS,
AUTHOR = {E. T. Schubert},
TITLE = {Verification of Composed Hardware Systems Using {CCS}},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {88--95}
}
@INPROCEEDINGS{VeInSub,
AUTHOR = {E. T. Schubert},
TITLE = {Verification of Integrated Subsystems},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {38--51}
}
@INPROCEEDINGS{TreeBaGr,
AUTHOR = {T. Schubert and J. Biggs},
TITLE = {A Tree-Based, Graphical Interface for Large Proof Development},
BOOKTITLE = {Supplementary Proceedings of the 7th International Workshop on Higher
Order Logic Theorem Proving and its Applications},
EDITOR = {T. F. Melham and J. Camilleri},
PUBLISHER = {University of Malta, Valletta},
YEAR = {1994},
URL = {ftp://ftp.dcs.glasgow.ac.uk/pub/hug94/schubert.ps.gz}
}
@INPROCEEDINGS{MechLog,
AUTHOR = {E. T. Schubert and S. Mocas},
TITLE = {A Mechanized Logic for Secure Key Escrow Protocol Verification},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah, {S}eptember 1995:
Proceedings},
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {308--323},
URL = {ftp://ftp.cs.pdx.edu/pub/faculty/schubert/hug95-SM.ps.gz}
}
@PROCEEDINGS{HOLTPandA,
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
TITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah,
{S}eptember 1995: Proceedings},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995}
}
@INPROCEEDINGS{TwoLeForV,
AUTHOR = {C.-J. H. Seger and J. J. Joyce},
TITLE = {A Two-Level Formal Verification Methodology
using {HOL} and {COSMOS}},
BOOKTITLE = {Computer Aided Verification: 3rd International
Workshop, {CAV}'91; {A}alborg, 1991: Proceedings},
EDITOR = {K. G. Larsen and A. Skou},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {575},
PUBLISHER = {Springer-Verlag},
YEAR = {1991},
PAGES = {299--309}
}
@INCOLLECTION{DesaProc,
AUTHOR = {D. Shepherd},
TITLE = {Designing a Processor},
BOOKTITLE = {Towards Verified Systems},
EDITOR = {J. Bowen},
SERIES = {Real-Time Safety Critical Systems Series},
VOLUME = {2},
PUBLISHER = {Elsevier},
YEAR = {1994},
PAGES = {167-192}
}
@INPROCEEDINGS{UsingHPro,
AUTHOR = {D. Shepherd},
TITLE = {Using {HOL} to produce custom verification tools},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {162--169}
}
@INPROCEEDINGS{ACUnif,
AUTHOR = {K. Slind},
TITLE = {{AC} Unification in {HOL}90},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {437--449}
}
@INPROCEEDINGS{AddNewR,
AUTHOR = {K. Slind},
TITLE = {Adding New Rules to an {LCF}-style Logic Implementation},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {549--559}
}
@INPROCEEDINGS{DefNestRec,
AUTHOR = {K. Slind},
TITLE = {Another Look at Nested Recursion},
BOOKTITLE = {Theorem Proving in Higher Order Logics, 13th
International Conference, {TPHOLs'00},
Portland Oregon, August 2000},
EDITOR = {Mark Aagaard and John Harrison},
PUBLISHER = {Springer-Verlag},
VOLUME = {1869},
PAGES = {498--518},
YEAR = {2000}
}
@TECHREPORT{ComplDerRI,
AUTHOR = {K. Slind},
TITLE = {Completion as a Derived Rule of Inference},
NUMBER = {90--409--33},
INSTITUTION = {Computer Science Department, University of Calgary},
YEAR = {1990}
}
@INPROCEEDINGS{DerUseInduction,
AUTHOR = {K. Slind},
TITLE = {Derivation and Use of Induction Schemes in Higher Order Logic},
BOOKTITLE = {Theorem Proving in Higher Order Logics, 10th
International Conference, {TPHOLs'97}, Murray Hill,
New Jersey, August 1997: Proceedings},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
EDITOR = {E. Gunter and A. Felty},
PAGES = {275--291},
VOLUME = {1275}
}
@INPROCEEDINGS{FuncDefHOL,
AUTHOR = {K. Slind},
TITLE = {Function Definition in Higher Order Logic},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International Conference,
{T}urku, {F}inland, {A}ugust 1996: Proceedings},
EDITOR = {J. von Wright and J. Grundy and J. Harrison},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1125},
PUBLISHER = {Springer-Verlag},
YEAR = {1996},
PAGES = {381--397}
}
@TECHREPORT{ImplHOL,
AUTHOR = {K. Slind},
TITLE = {An Implementation of Higher Order Logic},
NUMBER = {91--419--03},
INSTITUTION = {Computer Science Department, University of Calgary},
MONTH = {January},
YEAR = {1991}
}
@INPROCEEDINGS{Paraproof,
AUTHOR = {K. Slind},
TITLE = {A Parameterized Proof Manager},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {407--424}
}
@PHDTHESIS{SlindPhd,
AUTHOR = {K. Slind},
TITLE = {Reasoning about Terminating Functional Programs},
YEAR = {1999},
SCHOOL = {Institut f{\"u}r Informatik, Technische
Universit{\"a}t M{\"u}nchen},
URL = {http://tumb1.biblio.tu-muenchen.de/publ/diss/in/1999/slind.html}
}
@INPROCEEDINGS{TaggedProofArch,
AUTHOR = {K. Slind},
TITLE = {A Tagged {LCF}-style Proof Architecture},
BOOKTITLE = {Labelled Deduction {LD'98}, First International
Workshop, Freiburg,Germany, September 1998: Participants
Proceedings},
YEAR = {1998},
EDITOR = {David Basin and Luca Vigano},
URL = {http://www.cs.utah.edu/~slind/papers/tag.html}
}
@INPROCEEDINGS{WellSchDef,
AUTHOR = {K. Slind},
TITLE = {Wellfounded Schematic Definitions},
BOOKTITLE = {Automated Deduction: 17th International
Conference, {CADE-17}, Pittsburgh,
Pennsylvania, June 2000: Proceedings},
PUBLISHER = {Springer-Verlag},
VOLUME = {1831},
EDITOR = {D. McAllester},
PAGES = {45--63},
YEAR = {2000}
}
@INPROCEEDINGS{FroLoLa,
AUTHOR = {K. Slind and G. Birtwistle and M. Hermann and T. Simpson},
TITLE = {From Logic to Layout: transforming {HOL} specifications into gate
array netlists},
BOOKTITLE = {Proceedings of the Canadian Conference on Electrical and
Computer Engineering: {M}ontreal, {Q}uebec, {C}anada},
YEAR = {1989},
PAGES = {352--355}
}
@INPROCEEDINGS{IterativeDialoguesAutoProof,
AUTHOR = {K. Slind and R. Boulton},
TITLE = {Iterative Dialogues and Automated Proof},
BOOKTITLE = {Frontiers of Combining Systems 2, Second International
Workshop, {FroCoS'98}: Proceedings},
EDITOR = {D. M. Gabbay and M. de Rijke},
PAGES = {317--335},
YEAR = {2000},
SERIES = {Studies in Logic and Computation},
VOLUME = {7},
PUBLISHER = {Research Studies Press}
}
@INPROCEEDINGS{SysDescClamHOL,
AUTHOR = {K. Slind and M. Gordon and R. Boulton and A. Bundy},
TITLE = {System Description: An Interface Between
{CL{\raisebox{1ex}{A}}M} and {HOL}},
PAGES = {134--138},
ISBN = {3-540-64675-2},
EDITOR = {C. Kirchner and H. Kirchner},
BOOKTITLE = {15th International Conference on Automated Deduction
{CADE}-98, Lindau, July 1998: Proceedings},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {1421},
PUBLISHER = {Springer-Verlag}
}
@PHDTHESIS{FoSpAn,
AUTHOR = {E. Snekkenes},
TITLE = {Formal Specification and Analysis of Cryptographic Protocols},
SCHOOL = {University of Oslo},
MONTH = {January},
YEAR = {1995},
URL = {ftp://ftp.ffi.no/pub/easthesis.ps.Z}
}
@INPROCEEDINGS{FoSpVeH,
AUTHOR = {V. Stavridou and H. Barringer and D. A. Edwards},
TITLE = {Formal Specification and Verification of Hardware:
A Comparative Case Study},
BOOKTITLE = {25th {ACM/IEEE} Design Automation Conference: Proceedings},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1988},
PAGES = {197--204}
}
@PHDTHESIS{MaAsReSt,
AUTHOR = {D. Syme},
TITLE = {Machine Assisted Reasoning About Standard ML Using {HOL}},
SCHOOL = {Australian National University},
MONTH = {November},
YEAR = {1992},
URL = {ftp://ftp.cl.cam.ac.uk/hvg/papers/MLinHOL.thesis.ps.gz}
}
@INPROCEEDINGS{NewIntHOL,
AUTHOR = {D. Syme},
TITLE = {A New Interface for {HOL} - Ideas, Issues, and Implementation},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah, {S}eptember 1995:
Proceedings},
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {324--339},
URL = {http://www.cl.cam.ac.uk/users/drs1004/papers/Tk{HOL}.hug95/paper.html}
}
@INPROCEEDINGS{ReasFD,
AUTHOR = {D. Syme},
TITLE = {Reasoning with the Formal Definition of Standard ML in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {43--60},
URL = {ftp://ftp.cl.cam.ac.uk/hvg/papers/MLin{HOL}.hug93.ps.gz}
}
@INPROCEEDINGS{CompMDGHOL,
AUTHOR = {S. Tahar and P. Curzon},
TITLE = {A Comparison of {MDG} and {HOL} for Hardware Verification},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International Conference,
{T}urku, {F}inland, {A}ugust 1996: Proceedings},
EDITOR = {J. von Wright and J. Grundy and J. Harrison},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1125},
PUBLISHER = {Springer-Verlag},
YEAR = {1996},
PAGES = {415--430}
}
@ARTICLE{ForSpVerT,
AUTHOR = {S. Tahar and R. Kumar},
TITLE = {Formal Specification and Verification Techniques for
{RISC} Pipeline Conflicts},
JOURNAL = {The Computer Journal},
VOLUME = {38},
NUMBER = {2},
MONTH = {July},
YEAR = {1995},
PAGES = {111--120},
URL = {http://www.oup.co.uk/oup/smj/journals/ed/titles/computer_journal/docs/journal_contents/Volume_38_Number_2/38.2.ps/kumar.ps}
}
@INPROCEEDINGS{FoVerPi,
AUTHOR = {S. Tahar and R. Kumar},
TITLE = {Formal Verification of Pipeline Conflicts in {RISC} Processors},
BOOKTITLE = {Proceedings of {E}uropean Design Automation Conference ({EURO-DAC}'94):
{G}renoble, {F}rance, {S}eptember 1994},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1994},
PAGES = {285--289},
URL = {http://www.iro.umontreal.ca/people/tahar/publications/EURO_DAC94.ps.gz}
}
@INPROCEEDINGS{AForHiMo,
AUTHOR = {S. Tahar and R. Kumar},
TITLE = {A Formalization of a Hierarchical Model for {RISC} Processors},
BOOKTITLE = {Proceedings of {E}uropean Informatics Congress
Computing Systems Architecture ({E}uro-{ARCH}'93), {M}unich,
{G}ermany, {O}ctober 1993},
EDITOR = {P. Spies},
PUBLISHER = {Springer-Verlag},
YEAR = {1993},
PAGES = {591-602},
URL = {http://www.iro.umontreal.ca/people/tahar/publications/Euro_ARCH93.ps.gz}
}
@INPROCEEDINGS{ImpIssVP,
AUTHOR = {S. Tahar and R. Kumar},
TITLE = {Implementational Issues for Verifying {RISC}-Pipeline Conflicts in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {424--439},
URL = {http://www.iro.umontreal.ca/people/tahar/publications/HUG94.ps.gz}
}
@INPROCEEDINGS{ImpMeth,
AUTHOR = {S. Tahar and R. Kumar},
TITLE = {Implementing a Methodology for Forally Verifying {RISC} Processors in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {281--294},
URL = {http://www.iro.umontreal.ca/people/tahar/publications/HUG93.ps.gz}
}
@TECHREPORT{PraMeFV,
AUTHOR = {S. Tahar and R. Kumar},
TITLE = {A Practical Methodology for the Formal Verification of {RISC} Processors},
NUMBER = {FZI 9/95},
INSTITUTION = {Forschungszentrum Informatik, Haid-und-Neu Strasse 10--14,
76131 Karlsruhe, Germany},
MONTH = {August},
YEAR = {1995},
URL = {http://www.iro.umontreal.ca/people/tahar/publications/FZI-TR-95.ps.gz}
}
@INPROCEEDINGS{ToMeVeRISC,
AUTHOR = {S. Tahar and R. Kumar},
TITLE = {Towards a Methodology for the Formal Hierarchical
Verification of RISC Processors},
BOOKTITLE = {Proceedings of the IEEE International Conference on Computer
Design ({ICCD}'93), {C}ambridge, {M}assachusetts, {USA}, {O}ctober 1993},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1993},
PAGES = {58--62},
URL = {http://www.iro.umontreal.ca/people/tahar/publications/ICCD93.ps.gz}
}
@INPROCEEDINGS{Proofdev,
AUTHOR = {L. Th{\'{e}}ry},
TITLE = {A Proof development System for the {HOL} Theorem Prover},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {115--128}
}
@INPROCEEDINGS{RealThePr,
AUTHOR = {L. Th{\'{e}}ry and Yves Bertot and Gilles Kahn},
TITLE = {Real Theorem Provers Deserve Real User-Interfaces},
BOOKTITLE = {Proceedings of The Fifth ACM Symposium on Software
Development Environments ({SDE}5), {W}ashington {D.C.}},
MONTH = {December},
YEAR = {1992},
URL = {file://babar.inria.fr:/pub/croap/General/sde5.ps}
}
@PHDTHESIS{MechNond,
AUTHOR = {P. G. Tredoux},
TITLE = {Mechanizing nondeterministic programming logics in higher-order logic},
SCHOOL = {Department of Mathematics,University of Cape Town},
MONTH = {March},
YEAR = {1993},
URL = {ftp://ftp.mosaic.co.za/gavan/thesis/}
}
@ARTICLE{MeExSeSe,
AUTHOR = {G. Tredoux},
TITLE = {Mechanizing Execution Sequence Semantics in {HOL}},
JOURNAL = {South African Computer Journal},
VOLUME = {7},
MONTH = {July},
YEAR = {1992}
}
@MANUAL{HOSysD,
AUTHOR = {SRI International and DSTO},
TITLE = {The {HOL} System: Description},
ORGANIZATION = {University of Cambridge Computer Laboratory},
MONTH = {July},
YEAR = {1991},
URL = {http://lal.cs.byu.edu/lal/HOLdoc/description.html},
NOTE = {revised edition}
}
@MANUAL{HOSysR,
AUTHOR = {SRI International and DSTO},
TITLE = {The {HOL} System: Description},
ORGANIZATION = {University of Cambridge Computer Laboratory},
MONTH = {July},
YEAR = {1991},
URL = {http://lal.cs.byu.edu/cgi-bin/HOL-reference_search},
NOTE = {revised edition}
}
@MANUAL{HOSysT,
AUTHOR = {SRI International and DSTO},
TITLE = {The {HOL} System: Description},
ORGANIZATION = {University of Cambridge Computer Laboratory},
MONTH = {July},
YEAR = {1991},
URL = {http://lal.cs.byu.edu/lal/{HOL}doc/tutorial.html},
NOTE = {revised edition}
}
@INPROCEEDINGS{HOLML,
AUTHOR = {M. VanInwegen and E. Gunter},
TITLE = {{HOL-ML}},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {61--74}
}
@TECHREPORT{FemVSem,
AUTHOR = {J. P. Van Tassel},
TITLE = {Femto-{VHDL}: The Semantics of a Subset of VHDL and
its Embedding in the {HOL} Proof Assistant},
NUMBER = {317},
INSTITUTION = {University of Cambridge Computer Laboratory },
MONTH = {November},
YEAR = {1993},
URL = {http://www.cl.cam.ac.uk:80/ftp/hvg/papers/JVTthesis}
}
@INPROCEEDINGS{FormVHDL,
AUTHOR = {J. P. Van Tassel},
TITLE = {A Formalisation of the {VHDL} Simulation Cycle},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {359--374}
}
@INCOLLECTION{OpSemSu,
AUTHOR = {J. P. Van Tassel},
TITLE = {An Operational Semantics for a Subset of {VHDL}},
BOOKTITLE = {Formal Semantics for {VHDL}},
EDITOR = {C. D. Kloos and P. T. Breuer},
PUBLISHER = {Kluwer},
YEAR = {1995},
PAGES = {71--106}
}
@PHDTHESIS{SemVHDLV,
AUTHOR = {J. P. Van Tassel},
TITLE = {The Semantics of {VHDL} with {VAL} and {HOL}: Towards Practical
Verification Tools},
SCHOOL = {Department of Computer Science and Engineering, Wright University},
YEAR = {1989}
}
@INPROCEEDINGS{ToForVerVHDL,
AUTHOR = {J. Van Tassel},
TITLE = {Toward Formal Verification of {VHDL} Specifications},
BOOKTITLE = {Formal {VLSI} Correctness Verification: {VLSI} Design Methods-{II}:
Proceedings of the {IFIP WG 10.2/WG1} 0.5 International Workshop
on Applied Formal Methods for {VLSI} Design, {B}elgium, {N}ovember 1989},
EDITOR = {L. J. M. Claesen},
PUBLISHER = {North-Holland},
YEAR = {1990},
PAGES = {399--408}
}
@INPROCEEDINGS{Introwff,
AUTHOR = {M. van der Voort},
TITLE = {Introducing well-founded function definitions in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {117--131}
}
@INPROCEEDINGS{ToEffConPE,
AUTHOR = {M. Welinder},
TITLE = {Towards Efficient Conversions by use of Partial Evaluation},
BOOKTITLE = {Supplementary Proceedings of the 7th International Workshop on Higher
Order Logic Theorem Proving and its Applications},
EDITOR = {T. F. Melham and J. Camilleri},
PUBLISHER = {University of Malta, Valletta},
YEAR = {1994},
URL = {ftp://ftp.dcs.glasgow.ac.uk/pub/hug94/welinder.ps.gz}
}
@INPROCEEDINGS{VEfficConv,
AUTHOR = {M. Welinder},
TITLE = {Very Efficient Conversions},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah, {S}eptember 1995:
Proceedings},
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {340--352},
URL = {ftp://ftp.diku.dk/diku/semantics/papers/D-248.dvi.gz}
}
@INPROCEEDINGS{AbstTheoHOL,
AUTHOR = {P. J. Windley},
TITLE = {Abstract Theories in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {197--210}
}
@PHDTHESIS{FoVeGen,
AUTHOR = {P. J. Windley},
TITLE = {The Formal Verification of Generic Interpreters},
SCHOOL = {University of California Davis},
YEAR = {1990},
URL = {ftp://lal.cs.byu.edu/pub/{HOL}/lal-papers/git.diss.ps.gz}
}
@INPROCEEDINGS{PractVerMic,
AUTHOR = {P. J. Windley},
TITLE = {The Practical Verification of Microprocessor Designs},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {32--37}
}
@INPROCEEDINGS{SpecIn,
AUTHOR = {P. J. Windley},
TITLE = {Specifying Instruction-Set Architectures in {HOL}: A Primer},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {440--455},
URL = {ftp://lal.cs.byu.edu/pub/HOL/lal-papers/archspec.ps.gz}
}
@INPROCEEDINGS{TheGeInt,
AUTHOR = {P. J. Windley},
TITLE = {A Theory of Generic Interpreters},
BOOKTITLE = {Correct Hardware Design and Verification Methods:
{IFIP WG}10.2 Advanced Research Working Conference: Proceedings},
EDITOR = {G. J. Milne and L. Pierre},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {683},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {122--134}
}
@INPROCEEDINGS{UMML,
AUTHOR = {P. J. Windley},
TITLE = {Using Make to Manage Large Proofs},
BOOKTITLE = {Supplementary Proceedings of the 7th International Workshop on Higher
Order Logic Theorem Proving and its Applications},
EDITOR = {T. F. Melham and J. Camilleri},
PUBLISHER = {University of Malta, Valletta},
YEAR = {1994},
URL = {ftp://ftp.dcs.glasgow.ac.uk/pub/hug94/windley.ps.gz}
}
@INPROCEEDINGS{CorrMoPiM,
AUTHOR = {P. J. Windley and M. L. Coe},
TITLE = {A Correctness Model for Pipelined Microprocessors},
BOOKTITLE = {Theorem Provers in Circuit Design: Theory, Practice and
Experience: Proceedings},
EDITOR = {R. Kumar and T. Kropf},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {901},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {33--51},
URL = {ftp://lal.cs.byu.edu/pub/{HOL}/lal-papers/pipeline.ps.gz}
}
@TECHREPORT{ProofThir,
AUTHOR = {G. Winskel},
TITLE = {Proceedings of the Third {HOL} Users Meeting:
{A}arhus, {O}ctober 1990},
NUMBER = {Report DAIMI PB -- 340},
INSTITUTION = {Computer Science Department, Aarhus University},
MONTH = {December},
YEAR = {1990}
}
@PHDTHESIS{ForTheRail,
AUTHOR = {W. Wong},
TITLE = {A Formal Theory of Railway Track Networks in
Higher-order Logic and its Applications in Interlocking Design},
SCHOOL = {Department of Engineering, University of Warwick},
YEAR = {1991}
}
@TECHREPORT{FVVIPA,
AUTHOR = {W. Wong},
TITLE = {Formal Verification of {VIPER}'s {ALU}},
NUMBER = {300},
INSTITUTION = {University of Cambridge Computer Laboratory },
MONTH = {May},
YEAR = {1993},
URL = {ftp://ftp.cl.cam.ac.uk/hvg/papers/WW_report_300.ps.gz}
}
@INPROCEEDINGS{HOLModIS,
AUTHOR = {W. Wong},
TITLE = {A {HOL} Model of Interlocking Systems},
BOOKTITLE = {Supplementary Proceedings of the 9th International Conference on
Theorem Proving in Higher Order Logics: {TPHOL}s'96},
EDITOR = {J. von Wright and J. Grundy and J. Harrison},
SERIES = {TUCS General Publication},
NUMBER = {1},
PUBLISHER = {Turku Centre for Computer Science},
MONTH = {August},
YEAR = {1996},
PAGES = {105--120},
URL = {http://www.abo.fi/~jharriso/supp-root.html}
}
@INPROCEEDINGS{ModBV,
AUTHOR = {W. Wong},
TITLE = {Modelling Bit Vectors in {HOL}: the word Library},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {371--384}
}
@TECHREPORT{RecordHOL,
AUTHOR = {W. Wong},
TITLE = {Recording {HOL} Proofs},
NUMBER = {306},
INSTITUTION = {University of Cambridge Computer Laboratory},
MONTH = {July},
YEAR = {1993},
URL = {ftp://ftp.cl.cam.ac.uk/hvg/papers/WW_report_306.ps.gz}
}
@INPROCEEDINGS{RecCheck,
AUTHOR = {W. Wong},
TITLE = {Recording and Checking {HOL} Proofs},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah, {S}eptember 1995:
Proceedings},
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {353-368}
}
@INPROCEEDINGS{SimGraTh,
AUTHOR = {W. Wong},
TITLE = {A Simple Graph Theory and Its Application in Railway Signalling},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {395--409}
}
@TECHREPORT{DoLatT,
AUTHOR = {J. von Wright},
TITLE = {Doing Lattice Theory in Higher Order Logic},
INSTITUTION = {{\AA}bo Akademi},
TYPE = {Series A, Reports on Computer Science {\&} Mathematics},
NUMBER = {136},
YEAR = {1992},
URL = {http://www.abo.fi/~mats/cs/publications/reports/abstracts/vonWright92b.html}
}
@INPROCEEDINGS{MeTemLog,
AUTHOR = {J. von Wright},
TITLE = {Mechanising the Temporal Logic of Actions in {HOL}},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {155--159}
}
@ARTICLE{MechAdvRC,
AUTHOR = {J. von Wright},
TITLE = {Mechanising some Advanced Refinement Concepts},
JOURNAL = {Formal Methods in System Design},
VOLUME = {3},
NUMBER = {1--2},
MONTH = {August},
YEAR = {1993},
PAGES = {49--81}
}
@TECHREPORT{ProRefby,
AUTHOR = {J. von Wright},
TITLE = {Program Refinement by Theorem Prover},
INSTITUTION = {{\AA}bo Akademi},
TYPE = {Series A, Reports on Computer Science {\&} Mathematics},
NUMBER = {146},
YEAR = {1994},
URL = {http://www.abo.fi/~mats/cs/publications/reports/abstracts/vonWright94a.html}
}
@ARTICLE{RepHOLPro,
AUTHOR = {J. von Wright},
TITLE = {Representing higher-order logic proofs in {HOL}},
JOURNAL = {The Computer Journal},
VOLUME = {38},
NUMBER = {2},
MONTH = {July},
YEAR = {1995},
PAGES = {171--179},
URL = {http://www.oup.co.uk/oup/smj/journals/ed/titles/computer_journal/docs/journal_contents/Volume_38_Number_2/38.2.ps/vonwright.ps}
}
@INPROCEEDINGS{RepHOL,
AUTHOR = {J. von Wright},
TITLE = {Representing higher-order logic proofs in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop,
{V}alletta, {M}alta, {S}eptember 1994: Proceedings},
EDITOR = {T. F. Melham and J. Camilleri},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {859},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {456--470}
}
@INPROCEEDINGS{UThePfor,
AUTHOR = {J. von Wright and T. L{\aa}ngbacka},
TITLE = {Using a Theorem Prover for Reasoning about Concurrent Algorithms},
BOOKTITLE = {Computer Aided Verification: Fourth International Workshop,
{CAV}'92; {M}ontreal, 1992; Proceedings},
EDITOR = {G. v. Bochmann and D. K. Probst},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {663},
PUBLISHER = {Springer-Verlag},
YEAR = {1993},
PAGES = {56--68}
}
@INPROCEEDINGS{MechARC,
AUTHOR = {J. von Wright and J. Hekanaho and P. Luostarinen and T. L{\aa}ngbacka},
TITLE = {Mechanising some Advanced Refinement Concepts},
BOOKTITLE = {Higher Order Logic Theorem Proving and its Applications:
Proceedings of the {IFIP TC10/WG10.2} International Workshop,
{L}euven, {S}eptember 1992},
EDITOR = {L. J. M. Claesen and M. J. C. Gordon},
SERIES = {IFIP Transactions A-20},
PUBLISHER = {North-Holland},
YEAR = {1993},
PAGES = {307--326}
}
@INPROCEEDINGS{ProTranRef,
AUTHOR = {J. von Wright and K. Sere},
TITLE = {Program Transformations and Refinements in {HOL}},
BOOKTITLE = {Proceedings of the 1991 International Workshop
on the {HOL} Theorem Proving System and its Applications,
{D}avis, {A}ugust 1991},
EDITOR = {M. Archer and J. J. Joyce and K. N. Levit and P. J. Windley},
PUBLISHER = {IEEE Computer Society Press},
YEAR = {1992},
PAGES = {231--239}
}
@INPROCEEDINGS{FormPlan,
AUTHOR = {M. Yamamoto and S. Nishizaki and M. Hagiya and Y. Toda},
TITLE = {Formalizing Planar Graphs},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah, {S}eptember 1995:
Proceedings},
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {369--384}
}
@INPROCEEDINGS{MechCompTheoHOL,
AUTHOR = {V. Zammit},
TITLE = {A Mechanisation of Computability Theory in {HOL}},
BOOKTITLE = {Theorem Proving in Higher Order Logics: 9th International Conference,
{T}urku, {F}inland, {A}ugust 1996: Proceedings},
EDITOR = {J. von Wright and J. Grundy and J. Harrison},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {1125},
PUBLISHER = {Springer-Verlag},
YEAR = {1996},
PAGES = {431--446}
}
@INPROCEEDINGS{HierMeth,
AUTHOR = {C. Zhang and B. R. Becker and M. R. Heckman and K. Levitt and R. A. Olsson},
TITLE = {A Hierarchical Method for Reasoning about Distributed Programming
Languages},
BOOKTITLE = {Higher Order Logic Theorem Proving and Its Applications:
8th International Workshop, {A}spen {G}rove, {U}tah, {S}eptember 1995:
Proceedings},
EDITOR = {E. T. Schubert and P. J. Windley and J. Alves-Foss},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {971},
PUBLISHER = {Springer-Verlag},
YEAR = {1995},
PAGES = {385--400}
}
@INPROCEEDINGS{MechPL,
AUTHOR = {C. Zhang and R. Shaw and R. A. Olsson and K. Levitt and M. Archer and
M. R. Heckman and G. D. Benson},
TITLE = {Mechanizing a Programming Logic for the Concurrent Programming Language
micro{SR} in {HOL}},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {29--42}
}
@INPROCEEDINGS{ToFoVeSDS,
AUTHOR = {C. Zhang and R. Shaw and M. R. Heckman and G. D. Benson and
M. Archer and K. Levitt and R. A. Olsson},
TITLE = {Towards a Formal Verification of a Secure Distributed System and
its Applications},
BOOKTITLE = {Supplementary Proceedings of the 7th International Workshop on Higher
Order Logic Theorem Proving and its Applications},
EDITOR = {T. F. Melham and J. Camilleri},
PUBLISHER = {University of Malta, Valletta},
YEAR = {1994},
URL = {ftp://ftp.dcs.glasgow.ac.uk/pub/hug94/zhang.ps.gz}
}
@INPROCEEDINGS{VerTam3,
AUTHOR = {Z. Zhu and J. Joyce and C. Seger},
TITLE = {Verification of the {T}amarack-3 Microprocessor in A Hybrid Verification
Environment},
BOOKTITLE = {Higher Order Logic Theorem Proving and
its Applications: 6th International Workshop, {HUG'93},
{V}ancouver, {B.C.}, {A}ugust 11--13 1993: Proceedings},
EDITOR = {J. J. Joyce and C.-J. H. Seger},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {780},
PUBLISHER = {Springer-Verlag},
YEAR = {1994},
PAGES = {253--266}
}
This file has been generated by
bibtex2html 1.52