| [1] |
M. Aagaard, M. E. Leeser, and P. J. Windley.
Toward a super duper hardware tactic.
In J. J. Joyce and C.-J. H. Seger, editors, Higher Order Logic
Theorem Proving and its Applications: 6th International Workshop, HUG'93,
Vancouver, B.C., August 11-13 1993: Proceedings, volume 780 of
Lecture Notes in Computer Science, pages 399-412. Springer-Verlag, 1994. [ bib | .ps.gz ] |
| [2] |
S. Agerholm.
Domain theory in HOL.
In J. J. Joyce and C.-J. H. Seger, editors, Higher Order Logic
Theorem Proving and its Applications: 6th International Workshop, HUG'93,
Vancouver, B.C., August 11-13 1993: Proceedings, volume 780 of
Lecture Notes in Computer Science, pages 295-310. Springer-Verlag, 1994. [ bib ] |
| [3] |
S. Agerholm.
Formalising a model of the lambda-calculus in HOL-st.
Technical Report 354, University of Cambridge Computer Laboratory,
1994. [ bib ] |
| [4] |
S. Agerholm.
A HOL basis for reasoning about functional programs.
Technical Report BRICS Technical Report RS-94-44, Department of
Computer Science, University of Aarhus, December 1994. [ bib | .html ] |
| [5] |
S.Agerholm.
LCF examples in HOL.
The Computer Journal, 38(2):121-130, July 1995. [ bib | .ps ] |
| [6] |
S.Agerholm.
LCF examples in HOL.
In T. F. Melham and J. Camilleri, editors, Higher Order Logic
Theorem Proving and Its Applications: 7th International Workshop, Valletta,
Malta, September 1994: Proceedings, volume 859 of Lecture Notes in
Computer Science, pages 1-16. Springer-Verlag, 1994. [ bib ] |
| [7] |
S. Agerholm.
Mechanizing program verification in HOL.
In M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 208-222.
IEEE Computer Society Press, 1992. [ bib ] |
| [8] |
S.Agerholm.
Mechanizing program verification in HOL.
Technical Report DAIMI Report Number IR-111, Department of Computer
Science, University of Aarhus, April 1992. [ bib ] |
| [9] |
S.Agerholm.
Non-primitive recursive function definition.
In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors,
Higher Order Logic Theorem Proving and Its Applications: 8th International
Workshop, Aspen Grove, Utah, September 1995: Proceedings, volume 971
of Lecture Notes in Computer Science, pages 17-31. Springer-Verlag,
1995. [ bib | .html ] |
| [10] |
S.Agerholm, I. Beylin, and P. Dybjer.
A comparison of HOL and ALF formalizations of a categorical
coherence theorem.
In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem
Proving in Higher Order Logics: 9th International Conference, Turku,
Finland, August 1996: Proceedings, volume 1125 of Lecture Notes in
Computer Science, pages 17-32. Springer-Verlag, 1996. [ bib ] |
| [11] |
S. Agerholm and M. Gordon.
Experiments with ZF set theory in HOL and Isabelle.
In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors,
Higher Order Logic Theorem Proving and Its Applications: 8th International
Workshop, Aspen Grove, Utah, September 1995: Proceedings, volume 971
of Lecture Notes in Computer Science, pages 32-45. Springer-Verlag,
1995. [ bib | .html ] |
| [12] |
S. Agerholm and H. Skjødt.
Automating a model checker for recursive modal assertions in HOL.
Technical Report DAIMI Report Number IR-92, Department of Computer
Science, University of Aarhus, January 1990. [ bib ] |
| [13] |
O. Aït Mohamed.
Mechanizing a pi-calculus equivalence in HOL.
In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors,
Higher Order Logic Theorem Proving and Its Applications: 8th International
Workshop, Aspen Grove, Utah, September 1995: Proceedings, volume 971
of Lecture Notes in Computer Science, pages 1-16. Springer-Verlag,
1995. [ bib ] |
| [14] |
O. Aït Mohamed.
The theory of the pi-calcul in HOL.
PhD thesis, Henri Poincare University, July 1996. [ bib ] |
| [15] |
J. Alves-Foss, editor.
HOL-95: International Workshop on Higher Order Logic Theorem
Proving and its Applications: B-Track: Short Presentations, Aspen
Grove, Utah, September, 1995, 1995. [ bib | .html ] |
| [16] |
J. Alves-Foss.
Modelling non-deterministic systems in HOL.
In L. J. M. Claesen and M. J. C. Gordon, editors, Higher Order
Logic Theorem Proving and its Applications: Proceedings of the IFIP
TC10/WG10.2 International Workshop, Leuven, September 1992, IFIP
Transactions A-20, pages 295-304. North-Holland, 1993. [ bib ] |
| [17] |
J. Alves-Foss and K. Levitt.
Mechanical verification of secure distributed systems in higher order
logic.
In M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 263-278.
IEEE Computer Society Press, 1992. [ bib ] |
| [18] |
J. Alves-Foss and K. Levitt.
Verification of secure distributed systems in higher order logic: A
modular approach using generic components.
In Proceedings of the 1991 IEEE Computer Society Symposium on
Research in Security and Privacy; Oakland, California, May 1991, pages
122-135, 1991. [ bib | http ] |
| [19] |
F. Andersen, U. Binau, K. Nyblad, K. D. Petersen, and J. S. Pettersson.
The HOL-UNITY verification system.
In P. D. Mosses, M. Nielsen, and M. I. Schwartzbach, editors,
TAPSOFT'95: Theory and Practice of Software Development: 6th International
Conference: Proceedings, volume 915 of Lecture Notes in Computer
Science, pages 795-796. Springer-Verlag, 1995. [ bib ] |
| [20] |
F. Andersen and K. D. Petersen.
Recursive boolean functions in HOL.
In M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 367-377.
IEEE Computer Society Press, 1992. [ bib ] |
| [21] |
F. Andersen, K. D. Petersen, and J. S. Pettersson.
A graphical tool for proving UNITY progress.
In T. F. Melham and J. Camilleri, editors, Higher Order Logic
Theorem Proving and Its Applications: 7th International Workshop, Valletta,
Malta, September 1994: Proceedings, volume 859 of Lecture Notes in
Computer Science, pages 17-32. Springer-Verlag, 1994. [ bib ] |
| [22] |
F. Andersen, K. D. Petersen, and J. S. Pettersson.
Program verification using HOL-UNITY.
In J. J. Joyce and C.-J. H. Seger, editors, Higher Order Logic
Theorem Proving and its Applications: 6th International Workshop, HUG'93,
Vancouver, B.C., August 11-13 1993: Proceedings, volume 780 of
Lecture Notes in Computer Science, pages 1-15. Springer-Verlag, 1994. [ bib ] |
| [23] |
C. M. Angelo.
Formal Hardware Verification in a Silicon Compilation
Environment by means of Theorem Proving.
PhD thesis, Katholieke Universiteit Leuven, February, 1994. [ bib | .html ] |
| [24] |
C. M. Angelo, L. Claesen, and H. De Man.
Degrees of formality in shallow embedding hardware description
languages in HOL.
In J. J. Joyce and C.-J. H. Seger, editors, Higher Order Logic
Theorem Proving and its Applications: 6th International Workshop, HUG'93,
Vancouver, B.C., August 11-13 1993: Proceedings, volume 780 of
Lecture Notes in Computer Science, pages 89-100. Springer-Verlag, 1994. [ bib | .html ] |
| [25] |
C. M. Angelo, L. Claesen, and H. De Man.
The formal semantics definition of a multi-rate DSP specification
language in HOL.
In L. J. M. Claesen and M. J. C. Gordon, editors, Higher Order
Logic Theorem Proving and its Applications: Proceedings of the IFIP
TC10/WG10.2 International Workshop, Leuven, September 1992, IFIP
Transactions A-20, pages 375-394. North-Holland, 1993. [ bib ] |
| [26] |
C. M. Angelo, L. Claesen, and H. De Man.
A methodology for proving correctness of parameterized hardware
modules in HOL.
In D. Borrione and R. Waxman, editors, Tenth International
Symposium on Computer Hardware Description Languages and their Applications,
CHDL'91: Marseille, France, pages 63-82. North-Holland, 1991. [ bib ] |
| [27] |
C. M. Angelo, L. Claesen, and H. De Man.
Modeling multi-rate DSP specification semantics for formal
transformational design in HOL.
Formal Methods in System Design, 5(1/2):61-94, July 1994. [ bib | .html ] |
| [28] |
C. M. Angelo, L. Claesen, and H. De Man.
Reasoning about a class of linear systems of equations in HOL.
In T. F. Melham and J. Camilleri, editors, Higher Order Logic
Theorem Proving and Its Applications: 7th International Workshop, Valletta,
Malta, September 1994: Proceedings, volume 859 of Lecture Notes in
Computer Science, pages 33-48. Springer-Verlag, 1994. [ bib | .html ] |
| [29] |
C. M. Angelo, D. Verkest, L. Claesen, and H. De Man.
On the comparison of HOL and Boyer-Moore for formal hardware
verification.
Formal Methods in System Design, 2(1):45-72, February 1993. [ bib | .html ] |
| [30] |
C. M. Angelo, D. Verkest, L. Claesen, and H. De Man.
Formal hardware verification in HOL and in boyer-moore: A
comparative analysis.
In M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 340-347.
IEEE Computer Society Press, 1992. [ bib ] |
| [31] |
C. M. Angelo, D. Verkest, L. Claesen, and H. De Man.
A synopsis on the comparison of HOL and Boyer-Moore for formal
hardware verification.
In P. Prinetto and P. Camurati, editors, Advanced Research
Workshop on Correct Hardware Design Methodologies, pages 421-426.
North-Holland, 1991. [ bib ] |
| [32] |
M. Archer, G. Fink, and L. Yang.
Linking other theorem provers to HOL using PM: Proof manager.
In L. J. M. Claesen and M. J. C. Gordon, editors, Higher Order
Logic Theorem Proving and its Applications: Proceedings of the IFIP
TC10/WG10.2 International Workshop, Leuven, September 1992, IFIP
Transactions A-20, pages 539-548. North-Holland, 1993. [ bib ] |
| [33] |
M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley, editors.
Proceedings of the 1991 International Workshop on the HOL
Theorem Proving System and its Applications, Davis, August 1991. IEEE
Computer Society Press, 1992. [ bib ] |
| [34] |
R. D. Arthan.
A report on ICL HOL.
In M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on HOL Theorem Proving
System and its Applications, Davis, August 1991, pages 280-283. IEEE
Computer Society Press, 1992. [ bib ] |
| [35] |
R. D. Arthan.
A formal specification of HOL.
Technical Report DS/FMU/IED/SPC001, ICL Defence Systems, April 1990. [ bib ] |
| [36] |
R. J. R. Back and J. von Wright.
Predicate transformers and higher order logic.
In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors,
Semantics: Foundations and Applications: REX Workshop, Beekbergen, June
1992, volume 666 of Lecture Notes in Computer Science, pages 1-20.
Springer-Verlag, 1993. [ bib ] |
| [37] |
R. J. R. Back and J. von Wright.
Refinement concepts formalised in higher order logic.
Formal Aspects of Computing, 2(3):247-272, July-September
1990. [ bib ] |
| [38] |
S. Bainbridge, A. Camilleri, and R. Fleming.
Industrial application of theorem proving to system level design.
In M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 130-142.
IEEE Computer Society Press, 1992. [ bib ] |
| [39] |
S. Bainbridge, A. Camilleri, and R. Fleming.
Theorem proving as an industrial tool for system level design.
In V. Stavridou, T. F. Melham, and R. T. Boute, editors, Theorem
Provers in Circuit Design: Proceedings of the IFIP TC10/WG 10.2
International Conference, Nijmegen, June 1992, IFIP Transactions A-10,
pages 253-274. North-Holland, 1992. [ bib | .html ] |
| [40] |
E. de Barros Lucena.
Reasoning about petri nets in HOL.
In M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 384-394.
IEEE Computer Society Press, 1992. [ bib ] |
| [41] |
R. H. Beers and P. J. Windley.
Abstracting signals: The waveform library.
In J. von Wright, J. Grundy, and J. Harrison, editors,
Supplementary Proceedings of the 9th International Conference on Theorem
Proving in Higher Order Logics: TPHOLs'96, number 1 in TUCS General
Publication, pages 1-13. Turku Centre for Computer Science, August 1996. [ bib | .html ] |
| [42] |
G. Birtwistle and B. Graham.
Verifying SECD in HOL.
In J. Staunstrup, editor, Formal Methods for VLSI Design:
IFIP WG10.2, Lecture Notes, pages 129-177. North-Holland, 1990. [ bib ] |
| [43] |
G. Birtwistle, B. Graham, and S.-K. Chin.
An introduction to hardware verification in higher order logic.
Published electronically, August 1994. [ bib | .html ] |
| [44] |
G. Birtwistle, B. Graham, T. Simpson, K. Slind, M. Williams, and S. Williams.
Verifying an SECD chip in HOL.
In Proceedings of the IFIP WG 10.2/WG 10.5 International
Workshop on Applied Formal Methods for Correct VLSI Design, pages 369-378.
North Holland, 1990. [ bib ] |
| [45] |
G. Birtwistle, B. Graham, T. Simpson, K. Slind, M. Williams, and S. Williams.
Verifying an SECD chip in HOL.
In L. J. M. Claesen, editor, 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, Belgium, November 1989, pages 369-378. North-Holland, 1990. [ bib ] |
| [46] |
G. Birtwistle, M. Hermann, T. Simpson, and K. Slind.
From formal proof to netlist.
In Proceedings of the Canadian Conference on VLSI, pages
217-224, Vancouver, British Columbia, Canada, 1989. [ bib ] |
| [47] |
P. E. Black and P. J. Windley.
Automatically synthesized term denotation predicates: A proof aid.
In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors,
Higher Order Logic Theorem Proving and Its Applications: 8th International
Workshop, Aspen Grove, Utah, September 1995: Proceedings, volume 971
of Lecture Notes in Computer Science, pages 46-57. Springer-Verlag,
1995. [ bib | .ps ] |
| [48] |
P. E. Black and P. J. Windley.
Formal verification of secure programs in the presence of side
effects.
In Jr. R. H. Sprague, editor, Proceedings of the Thirty-first
Hawai'i International Conference on System Sciences (HICSS-31), volume
III, pages 327-334. IEEE Computer Science Press, 1998. [ bib ] |
| [49] |
P. E. Black and P. J. Windley.
Inference rules for programming languages with side effects in
expressions.
In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem
Proving in Higher Order Logics: 9th International Conference, Turku,
Finland, August 1996: Proceedings, volume 1125 of Lecture Notes in
Computer Science, pages 51-60. Springer-Verlag, 1996. [ bib ] |
| [50] |
P. E. Black and P. J. Windley.
Verifying resilient software.
In Jr. R. H. Sprague, editor, Proceedings of the Thirty-first
Hawai'i International Conference on System Sciences (HICSS-31), volume
III, pages 262-266. IEEE Computer Science Press, 1998. [ bib ] |
| [51] |
K. Blackburn.
A report on ICL HOL.
In D. Kapur, editor, Automated Deduction - CADE-11: 11th
International Conference, Proceedings, volume 607 of Lecture Notes in
Artificial Intelligence, pages 743-747. Springer-Verlag, 1992. [ bib ] |
| [52] |
J.-P. Bodeviex and M. Filali.
On the refinement of symmetric memory protocols.
In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors,
Higher Order Logic Theorem Proving and Its Applications: 8th International
Workshop, Aspen Grove, Utah, September 1995: Proceedings, volume 971
of Lecture Notes in Computer Science, pages 58-74. Springer-Verlag,
1995. [ bib ] |
| [53] |
J-P. Bodeviex, M. Filali, and P. Roche.
Towards a HOL theory of memory.
In T. F. Melham and J. Camilleri, editors, Higher Order Logic
Theorem Proving and Its Applications: 7th International Workshop, Valletta,
Malta, September 1994: Proceedings, volume 859 of Lecture Notes in
Computer Science, pages 49-64. Springer-Verlag, 1994. [ bib ] |
| [54] |
R. Boulton.
Boyer-Moore automation for the HOL system.
In L. J. M. Claesen and M. J. C. Gordon, editors, Higher Order
Logic Theorem Proving and its Applications: Proceedings of the IFIP
TC10/WG10.2 International Workshop, Leuven, September 1992, IFIP
Transactions A-20, pages 133-142. North-Holland, 1993. [ bib ] |
| [55] |
R. Boulton.
Combining decision procedures in the HOL system.
In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors,
Higher Order Logic Theorem Proving and Its Applications: 8th International
Workshop, Aspen Grove, Utah, September 1995: Proceedings, volume 971
of Lecture Notes in Computer Science, pages 75-89. Springer-Verlag,
1995. [ bib | .dvi.gz ] |
| [56] |
R. J. Boulton.
Efficiency in a fully-expansive theorem prover.
Technical Report 337, University of Cambridge Computer Laboratory,
May 1994. [ bib | .html ] |
| [57] |
R. Boulton.
A lazy approach to full-expansive theorem proving.
In L. J. M. Claesen and M. J. C. Gordon, editors, Higher Order
Logic Theorem Proving and its Applications: Proceedings of the IFIP
TC10/WG10.2 International Workshop, Leuven, September 1992, IFIP
Transactions A-20, pages 19-38. North-Holland, 1993. [ bib ] |
| [58] |
R. J. Boulton.
Lazy techniques for fully expansive theorem proving.
Formal Methods in System Design, 3(1-2):25-47, August 1993. [ bib ] |
| [59] |
R. J. Boulton.
On efficiency in theorem provers which fully expand proofs into
primitive inferences.
Technical Report 248, University of Cambridge Computer Laboratory,
February 1992. [ bib | .dvi.gz ] |
| [60] |
R. Boulton.
A restricted form of higher-order rewriting applied to an HDL
semantics.
In J. Hsiang, editor, Rewriting Techniques and Applications: 6th
International Conference: Proceedings, volume 914 of Lecture Notes in
Computer Science, pages 309-323. Springer-Verlag, 1995. [ bib ] |
| [61] |
R. Boulton, A. Gordon, M. Gordon, J. Harrison, J. Herbert, and J. Van Tassel.
Experience with embedding hardware description languages in HOL.
In V. Stavridou, T. F. Melham, and R. T. Boute, editors, Theorem
Provers in Circuit Design: Proceedings of the IFIP TC10/WG 10.2
International Conference, Nijmegen, June 1992, IFIP Transactions A-10,
pages 129-156. North-Holland, 1992. [ bib | .ps.gz ] |
| [62] |
R. Boulton, M. Gordon, J. Herbert, and J. Van Tassel.
The HOL verification of ELLA designs.
Appeared in the Unpublished Proceedings of the International Workshop
on Formal Methods in VLSI Design, Miami, Florida January 1991, 1991. [ bib | .ps.gz ] |
| [63] |
R. Boulton and K. Slind.
Automatic derivation and application of induction schemes for
mutually recursive functions.
In J. Lloyd, V. Dahl, U. Furbach, M. Kerber, K.-K. Lau,
C. Palamidessi, L. Moniz Pereira, Y. Sagiv, and P. J. Stuckey, editors,
Computational Logic: First International Conference, CL2000, London,
UK, July 2000: Proceedings, volume 1861, pages 629-643. Springer-Verlag,
2000. [ bib ] |
| [64] |
R. Boulton, K. Slind, A. Bundy, and M. Gordon.
An interface between Clam and HOL.
In J. Grundy and M. Newey, editors, Theorem Proving in Higher
Order Logics, 11th International Conference, TPHOLs'98, Canberra:
Proceedings, volume 1479 of Lecture Notes in Computer Science, pages
87-104. Springer-Verlag, 1998. [ bib ] |
| [65] |
J. Bowen, editor.
Towards Verified Systems, volume 2 of Real-Time Safety
Critical Systems Series.
Elsevier, 1994. [ bib ] |
| [66] |
J. P. Bowen and M. J. C. Gordon.
A shallow embedding of Z in HOL.
Information and Software Technology, 37(5-6):269-276,
May/June 1995. [ bib | .ps ] |
| [67] |
J. P. Bowen and M. J. C. Gordon.
Z and HOL.
In J. P. Bowen and J. A. Hall, editors, Z User Workshop,
Cambridge 1994, Workshops in Computing Series, pages 141-167.
Springer-Verlag, 1994. [ bib | .ps.Z ] |
| [68] |
S. H. Brackin.
Deciding cryptographic protocol adequacy with HOL.
In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors,
Higher Order Logic Theorem Proving and Its Applications: 8th International
Workshop, Aspen Grove, Utah, September 1995: Proceedings, volume 971
of Lecture Notes in Computer Science, pages 90-105. Springer-Verlag,
1995. [ bib ] |
| [69] |
S. H. Brackin.
Deciding cryptographic protocol adequacy with HOL: The
implementation.
In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem
Proving in Higher Order Logics: 9th International Conference, Turku,
Finland, August 1996: Proceedings, volume 1125 of Lecture Notes in
Computer Science, pages 61-76. Springer-Verlag, 1996. [ bib ] |
| [70] |
S. H. Brackin.
Providing tractable security analyses in HOL.
In T. F. Melham and J. Camilleri, editors, Higher Order Logic
Theorem Proving and Its Applications: 7th International Workshop, Valletta,
Malta, September 1994: Proceedings, volume 859 of Lecture Notes in
Computer Science, pages 65-80. Springer-Verlag, 1994. [ bib ] |
| [71] |
S. H. Brackin and S.-K. Chin.
Server-process restrictiveness in HOL.
In J. J. Joyce and C.-J. H. Seger, editors, Higher Order Logic
Theorem Proving and its Applications: 6th International Workshop, HUG'93,
Vancouver, B.C., August 11-13 1993: Proceedings, volume 780 of
Lecture Notes in Computer Science, pages 450-463. Springer-Verlag, 1994. [ bib ] |
| [72] |
Michael Butler, Jim Grundy, Thomas Långbacka, Rimvydas Ruksenas, and Joakim
von Wright.
The refinement calculator: Proof support for program refinement.
In Lindsay Groves and Steve Reeves, editors, Formal Methods
Pacific'97: Proceedings of FMP'97, Discrete Mathematics & Theoretical
Computer Science, pages 40-61, Wellington, New Zealand, July 1997.
Springer-Verlag. [ bib ] |
| [73] |
M. Butler and T. Långbacka.
Program derivation using the refinement calculator.
In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem
Proving in Higher Order Logics: 9th International Conference, Turku,
Finland, August 1996: Proceedings, volume 1125 of Lecture Notes in
Computer Science, pages 93-108. Springer-Verlag, 1996. [ bib ] |
| [74] |
A. J. Camilleri.
Executing behavioural definitions in higher order logic.
Technical Report 140, University of Cambridge Computer Laboratory,
February 1988. [ bib ] |
| [75] |
A. J. Camilleri.
A higher order logic mechanization of the CSP failure-divergence
semantics.
In G. Birtwistle, editor, IV Higher Order Workshop, Banff
1990: Proceedings, pages 123-150. Springer-Verlag, 1991. [ bib ] |
| [76] |
A. J. Camilleri.
Mechanizing CSP trace theory in higher order logic.
IEEE Transactions on Software Engineering, 16(9):993-1004,
September 1990. [ bib ] |
| [77] |
A. J. Camilleri.
Reasoning in CSP via the HOL theorem prover.
In Next Decade in Information Technology: Proceedings of the 5th
Jerusalem Conference on Information Technology, Israel, 22-25 October
1990, pages 173-183. IEEE Computer Society Press, 1990. [ bib ] |
| [78] |
A. J. Camilleri.
Simulating hardware specifications within a theorem-proving
framework.
International Journal of Computer Aided VLSI Design,
2:315-337, 1990. [ bib ] |
| [79] |
A. J. Camilleri.
Simulation as an aid to verification using the HOL theorem prover.
In D. Edwards, editor, Design Methodologies for VLSI and
Computer Architecture: Proceedings of the IFIP TC-10 International
Working Conference, Pisa, Italy, 19-21 September 1988, pages
147-168. North-Holland, 1989. [ bib ] |
| [80] |
A. Camilleri, M. Gordon, and T. Melham.
Hardware verification using higher-order logic.
In D. Borrione, editor, From HDL Descriptions to Guaranteed
Correct Circuit Designs: Proceedings of the IFIP WG 10.2 Working
Conference, September 1986, pages 43-67. North-Holland, 1987. [ bib ] |
| [81] |
A. Camilleri, P. Inverardi, and M. Nesi.
Combining interaction and automation in process algebra verification.
In S. Abramsky and T. Maibaum, editors, TAPSOFT'91:
Proceedings of the International Joint Conference on Theory and Practice of
Software Development, Brighton, 8-12 April 1991, volume 494 of
Lecture Notes in Computer Science, pages 283-296. Springer-Verlag, 1991. [ bib ] |
| [82] |
J. Camilleri and T. Melham.
Reasoning with inductively defined relations in the HOL theorem
prover.
Technical Report 265, University of Cambridge Computer Laboratory,
August 1992. [ bib | .ps ] |
| [83] |
J. Camilleri and V. Zammit.
Symbolic animation as a proof tool.
In T. F. Melham and J. Camilleri, editors, Higher Order Logic
Theorem Proving and Its Applications: 7th International Workshop, Valletta,
Malta, September 1994: Proceedings, volume 859 of Lecture Notes in
Computer Science, pages 113-127. Springer-Verlag, 1994. [ bib ] |
| [84] |
R. M. Cardell-Oliver.
The formal verification of hard real-time systems.
Technical Report 255, University of Cambridge Computer Laboratory,
May 1992. [ bib ] |
| [85] |
R. Cardell-Oliver.
HTTDs and HOL.
In C. Lewerentz and T. Lindner, editors, Formal development of
Reactive Systems: Case Study Production Cell, volume 891 of Lecture
Notes in Computer Science, pages 261-276. Springer-Verlag, 1994. [ bib | .ps.Z ] |
| [86] |
R. Cardell-Oliver.
On the use of the HOL system for protocol verification.
In M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 59-62.
IEEE Computer Society Press, 1992. [ bib ] |
| [87] |
R. M. Cardell-Oliver and R. Hale.
Linking notations and theories in a proof tool.
Technical Report CSM-245, Department of Computer Science, University
of Essex, August 1995. [ bib | .ps.Z ] |
| [88] |
R. Cardell-Oliver, R. Hale, and J. Herbert.
An embedding of timed transition systems in HOL.
In L. J. M. Claesen and M. J. C. Gordon, editors, Higher Order
Logic Theorem Proving and its Applications: Proceedings of the IFIP
TC10/WG10.2 International Workshop, Leuven, September 1992, IFIP
Transactions A-20, pages 263-278. North-Holland, 1993. [ bib ] |
| [89] |
R. Cardel-Oliver and C. Southon.
Theorem proving abstraction of model checking.
Technical Report CSM-253, Department of Computer Science, University
of Essex, October 1995. [ bib | .ps.Z ] |
| [90] |
V. A. Carreño.
Definition and partial verification of data routing circuit in hol.
July 1991. [ bib | .ps ] |
| [91] |
V. A. Carreño.
Transition Assertions: A Higher-Order Logic Based Method for the
Specification and Verfication of Real-Time Systems.
PhD thesis, University of Cambridge Computer Laboratory, 1997. [ bib | .ps.gz ] |
| [92] |
V. A. Carreño.
The transition assertions specification method.
Technical Report 279, Computer Laboratory, University of Cambridge,
January 1993. [ bib | .ps ] |
| [93] |
V. A. Carreño.
Verification in higher order logic of mutual exclusion algorithm.
In J. J. Joyce and C.-J. H. Seger, editors, Higher Order Logic
Theorem Proving and its Applications: 6th International Workshop, HUG'93,
Vancouver, B.C., August 11-13 1993: Proceedings, volume 780 of
Lecture Notes in Computer Science, pages 501-513. Springer-Verlag, 1994. [ bib ] |
| [94] |
V. A. Carre o and P. S. Miner.
Specification of the IEEE-854 floating-point standard in HOL and
PVS.
In J. Alves-Foss, editor, HOL-95: International Workshop on
Higher Order Logic Theorem Proving and its Applications: B-Track: Short
Presentations, Aspen Grove, Utah, September, 1995, pages 1-16,
1995. [ bib | .ps ] |
| [95] |
S.-K. Chin.
Combining engineering vigor with mathematical rigor.
In M. Leeser and G. Brown, editors, Hardware Specification,
Verification and Synthesis: Mathematical Aspects: Mathematical Sciences
Institute Workshop, Cornell, July 1989, volume 408 of Lecture Notes
in Computer Science, pages 152-176. Springer-Verlag, 1990. [ bib ] |
| [96] |
S.-K. Chin.
Verified functions for generating signed-binary arithmetic hardware.
IEEE Transactions on Computer-Aided Design of Integrated
Circuits and Systems, 11(12):1529-1558, December 1992. [ bib ] |
| [97] |
S.-K. Chin.
Verified synthesis functions for negabinary arithmetic hardware.
In L. J. M. Claesen, editor, 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, Belgium, November 1989, pages 187-196. North-Holland, 1990. [ bib ] |
| [98] |
S.-K. Chin.
Verifying arithmetic hardware in higher-order logic.
In M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 22-31.
IEEE Computer Society Press, 1992. [ bib ] |
| [99] |
S.-K. Chin and G. Birtwistle.
Implementing and verifying finite-state machines using types in
higher-order logic.
In M. Archer, J. J. Joyce, K. N. Levit, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 121-129.
IEEE Computer Society Press, 1992. [ bib ] |
| [100] |
C.-T. Chou.
A formal theory of undirected graphs in higher-order logic.
In T. F. Melham and J. Camilleri, editors, Higher Order Logic
Theorem Proving and Its Applications: 7th International Workshop, Valletta,
Malta, September 1994: Proceedings, volume 859 of Lecture Notes in
Computer Science, pages 144-157. Springer-Verlag, 1994. [ bib | .ps ] |
| [101] |
C.-T. Chou.
Mechanical verification of distributed algorithms in higher-order
logic.
The Computer Journal, 38(2):152-161, July 1995. [ bib | .ps ] |
| [102] |
C.-T. Chou.
Mechanical verification of distributed algorithms in higher-order
logic.
In T. F. Melham and J. Camilleri, editors, Higher Order Logic
Theorem Proving and Its Applications: 7th International Workshop, Valletta,
Malta, September 1994: Proceedings, volume 859 of Lecture Notes in
Computer Science, pages 158-176. Springer-Verlag, 1994. [ bib ] |
| [103] |
C.-T. Chou.
Note on interactive theorem proving with theorem continuation
functions.
In L. J. M. Claesen and M. J. C. Gordon, editors, Higher Order
Logic Theorem Proving and its Applications: Proceedings of the IFIP
TC10/WG10.2 International Workshop, Leuven, September 1992, IFIP
Transactions A-20, pages 59-69. North-Holland, 1993. [ bib | .ps ] |
| [104] |
C.-T. Chou.
Predicates, temporal logic, and simulations.
In J. J. Joyce and C.-J. H. Seger, editors, Higher Order Logic
Theorem Proving and its Applications: 6th International Workshop, HUG'93,
Vancouver, B.C., August 11-13 1993: Proceedings, volume 780 of
Lecture Notes in Computer Science, pages 310-323. Springer-Verlag, 1994. [ bib ] |
| [105] |
C.-T. Chou.
Sequent formulation of a logic of predicates in HOL.
In L. J. M. Claesen and M. J. C. Gordon, editors, Higher Order
Logic Theorem Proving and its Applications: Proceedings of the IFIP
TC10/WG10.2 International Workshop, Leuven, September 1992, IFIP
Transactions A-20, pages 71-80. North-Holland, 1993. [ bib | .ps ] |
| [106] |
C.-T. Chou and D. Peled.
Formal verification of a partial-order reduction technique for model
checking.
In T. Margaria and B. Steffen, editors, Tools and Algorithms for
the Construction and Analysis of Systems: Second International Workshop,
TACAS'96: Passau, March 27-29 1996: Proceedings, volume 1055 of
Lecture Notes in Computer Science, pages 241-257. Springer-Verlag, 1996. [ bib ] |
| [107] |
L. J. M. Claesen and M. J. C. Gordon, editors.
Higher Order Logic Theorem Proving and its Applications:
Proceedings of the IFIP TC10/WG10.2 International Workshop, Leuven,
September 1992, IFIP Transactions A-20. North-Holland, 1993. [ bib ] |
| [108] |
M. L. Coe.
Results from Verifying a Pipelined Microprocessor.
PhD thesis, University of Idaho, October 1994. [ bib | .ps.gz ] |
| [109] |
A. Cohn.
Correctness properties of the viper block model: The second level.
In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends
in Hardware Verification and Automated Theorem Proving, pages 1-91.
Springer-Verlag, 1989. [ bib ] |
| [110] |
A. Cohn.
A proof of correctness of the VIPER microprocessor: The first
level.
In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends
in Hardware Verification and Automated Theorem Proving, pages 27-71.
Springer-Verlag, 1989. [ bib ] |
| [111] |
A. Cohn.
The notion of proof in hardware verification.
Journal of Automated Reasoning, 5(2):127-139, June 1989. [ bib ] |
| [112] |
A. Cohn and M. Gordon.
A mechanized proof of correctness of a simple counter.
In K. McEvoy and J. V. Tucker, editors, Theoretical Foundations
of VLSI Design, number 10 in Cambridge Tracts in Theoretical Computer
Science, pages 65-96. Cambridge University Press, 1990. [ bib ] |
| [113] |
G. Collins.
A proof tool for reasoning about functional programs.
In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem
Proving in Higher Order Logics: 9th International Conference, Turku,
Finland, August 1996: Proceedings, volume 1125 of Lecture Notes in
Computer Science, pages 109-124. Springer-Verlag, 1996. [ bib ] |
| [114] |
G. Collins.
Supporting formal reasoning about standard ML.
Master's thesis, University of Edinburgh, November 1994. [ bib | .ps.Z ] |
| [115] |
G. Collins and D. Syme.
A theory of finite maps.
In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors,
Higher Order Logic Theorem Proving and Its Applications: 8th International
Workshop, Aspen Grove, Utah, September 1995: Proceedings, volume 971
of Lecture Notes in Computer Science, pages 122-137. Springer-Verlag,
1995. [ bib | .ps ] |
| [116] |
G. Collins and S. Gilmore.
Supporting formal reasoning about standard ML.
Technical Report LFCS report ECS-LFCS-94-310, Department of Computer
Science, University of Edinburgh, November 1994. [ bib | .html ] |
| [117] |
I. Craig.
Review of introduction to HOL, edited by M. Gordon and T.
Melham (Cambridge university press), 1993.
The Computer Journal, 36(6):601, 1993. [ bib ] |
| [118] |
W. J. Cullyer and W. J. Scales.
Irregularities in the behaviour of the 68020 processor.
High Integrity Systems, 1(3):301-311, 1995. [ bib ] |
| [119] |
W. J. Cullyer and W. Wong.
Application of formal methods to railway signalling - a case study.
IEE Computing and Control Engineering Journal, 4(1):15-22,
February 1993. [ bib ] |
| [120] |
P. Curzon.
Compiler correctness and input/output.
In C. E. Landwehr, B. Randell, and L. Simoncini, editors,
Dependable Computing for Critical Applications 3, volume 8 of
Dependable Computing and Fault-Tolerant Systems series, pages 189-209.
Springer Verlag, 1993. [ bib | .html ] |
| [121] |
P. Curzon.
Deriving correctness properties of compiled code.
Formal Methods in System Design, 3(1-2):83-115, August 1993. [ bib ] |
| [122] |
P. Curzon.
Deriving correctness properties of compiled code.
In L. J. M. Claesen and M. J. C. Gordon, editors, Higher Order
Logic Theorem Proving and its Applications: Proceedings of the IFIP
TC10/WG10.2 International Workshop, Leuven, September 1992, IFIP
Transactions A-20, pages 327-346. North-Holland, 1993. [ bib | .html ] |
| [123] |
P. Curzon.
The formal verification of an ATM network.
In Proceedings of the 13th Annual ACM Symposium on Principles
of Distributed Computing, page 392. ACM Press, 1994. [ bib | .html ] |
| [124] |
P. Curzon.
Experiences formally verifying a network component.
In Proceedings of the 9th Annual IEEE Conference on Computer
Assurance, pages 183-193. IEEE Press, 1994. [ bib | .html ] |
| [125] |
P. Curzon.
The formal verification of the fairisle ATM switching element.
Technical Report 329, Computer Laboratory, University of Cambridge,
March 1994. [ bib | .html ] |
| [126] |
P. Curzon.
The formal verification of the fairisle ATM switching element: an
overview.
Technical Report 328, Computer Laboratory, University of Cambridge,
March 1994. [ bib | .html ] |
| [127] |
P. Curzon.
The importance of proof maintenance and reengineering.
In J. Alves-Foss, editor, HOL-95: International Workshop on
Higher Order Logic Theorem Proving and its Applications: B-Track: Short
Presentations, Aspen Grove, Utah, September, 1995, pages 17-31,
1995. [ bib | .html ] |
| [128] |
P. Curzon.
Of what use is a verified compiler specification?
Technical Report 274, Computer Laboratory, University of Cambridge,
November 1992. [ bib | .html ] |
| [129] |
P. Curzon.
Problems encountered with the machine-assisted proof of hardware.
In P. E. Camurati and H. Eveking, editors, Correct Hardware
Design and Verification Methods, volume 987 of Lecture Notes in
Computer Science, pages 56-70. Springer-Verlag, 1995. [ bib | .html ] |
| [130] |
P. Curzon.
A programming logic for a verified structured assembly language.
In A. Voronkov, editor, Logic Programming and Automated
Reasoning:International Conference, LPAR'92: St. Petersburg, 1992,
volume 624 of Lecture Notes in Artificial Intelligence, pages 403-408.
Springer-Verlag, 1992. [ bib | .html ] |
| [131] |
P. Curzon.
Tracking design changes with formal machine-checked proof.
The Computer Journal, 38(2):91-100, July 1995. [ bib | .ps ] |
| [132] |
P. Curzon.
Tracking design changes with formal verification.
In T. F. Melham and J. Camilleri, editors, Higher Order Logic
Theorem Proving and Its Applications: 7th International Workshop, Valletta,
Malta, September 1994: Proceedings, volume 859 of Lecture Notes in
Computer Science, pages 177-192. Springer-Verlag, 1994. [ bib | .html ] |
| [133] |
P. Curzon.
Verified compiler for a structured assembly language.
In M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 253-262.
IEEE Computer Society Press, 1992. [ bib | .html ] |
| [134] |
P. Curzon.
A verified vista implementation.
Technical Report 311, Computer Laboratory, University of Cambridge,
September 1993. [ bib | .html ] |
| [135] |
P. Curzon.
Virtual theories.
In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors,
Higher Order Logic Theorem Proving and Its Applications: 8th International
Workshop, Aspen Grove, Utah, September 1995: Proceedings, volume 971
of Lecture Notes in Computer Science, pages 138-153. Springer-Verlag,
1995. [ bib | .html ] |
| [136] |
P. Curzon and I. M. Leslie.
A case study on design for provability.
In Proceedings of the First International Conference on
Engineering of Complex Computer Systems, pages 59-62. IEEE Press, November
1995. [ bib | .html ] |
| [137] |
P. Curzon, I. Leslie, and M. Gordon.
Conclusions from a study to verify a real network component.
In A. Ireland, editor, Automated Reasoning: Bridging the Gap
Between Theory and Practice; Proceedings, April 1995. [ bib | .html ] |
| [138] |
P. Curzon and W. Wong.
A theory of lists for HOL based on higher-order functions.
In T. F. Melham and J. Camilleri, editors, Supplementary
Proceedings of the 7th International Workshop on Higher Order Logic Theorem
Proving and its Applications. University of Malta, Valletta, 1994. [ bib | .ps.gz ] |
| [139] |
N. Day and J. J. Joyce.
The semantics of statecharts in HOL.
In J. J. Joyce and C.-J. H. Seger, editors, Higher Order Logic
Theorem Proving and its Applications: 6th International Workshop, HUG'93,
Vancouver, B.C., August 11-13 1993: Proceedings, volume 780 of
Lecture Notes in Computer Science, pages 338-351. Springer-Verlag, 1994. [ bib ] |
| [140] |
I. S. Dhingra.
Formal validation of an integrated circuit design style.
In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends
in Hardware Verification and Automated Theorem Proving, pages 293-321.
Springer-Verlag, 1989. [ bib ] |
| [141] |
I. S. Dhingra.
Formalising an integrated circuit design style in higher order logic.
Technical Report 151, Computer Laboratory, University of Cambridge,
November 1988. [ bib ] |
| [142] |
D. Eisenbiegler, C. Blumenröhr, and R. Kumar.
Implementation issues about the embedding of existing high level
synthesis algorithms in HOL.
In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem
Proving in Higher Order Logics: 9th International Conference, Turku,
Finland, August 1996: Proceedings, volume 1125 of Lecture Notes in
Computer Science, pages 157-172. Springer-Verlag, 1996. [ bib ] |
| [143] |
D. Eisenbiegler and R. Kumar.
An automata theory dedicated towards formal circuit synthesis.
In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors,
Higher Order Logic Theorem Proving and Its Applications: 8th International
Workshop, Aspen Grove, Utah, September 1995: Proceedings, volume 971
of Lecture Notes in Computer Science, pages 154-169. Springer-Verlag,
1995. [ bib ] |
| [144] |
D. Eisenbiegler and R. Kumar.
Evaluation techniques as a part of the verification process.
In T. F. Melham and J. Camilleri, editors, Supplementary
Proceedings of the 7th International Workshop on Higher Order Logic Theorem
Proving and its Applications. University of Malta, Valletta, 1994. [ bib | .ps.gz ] |
| [145] |
D. Eisenbiegler, K. Schneider, and R. Kumar.
A functional approach to formalizing regular hardware structures.
In J. J. Joyce and C.-J. H. Seger, editors, Higher Order Logic
Theorem Proving and its Applications: 6th International Workshop, HUG'93,
Vancouver, B.C., August 11-13 1993: Proceedings, volume 780 of
Lecture Notes in Computer Science, pages 101-114. Springer-Verlag, 1994. [ bib | .ps.gz ] |
| [146] |
G. Fink, M. Archer, and L. Yang.
Pm: A proof manager for HOL and other provers.
In M. Archer, J. J. Joyce, K. N. Levit, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 286-304.
IEEE Computer Society Press, 1992. [ bib ] |
| [147] |
T. Forster.
Weak systems of set theory related to HOL.
In T. F. Melham and J. Camilleri, editors, Higher Order Logic
Theorem Proving and Its Applications: 7th International Workshop, Valletta,
Malta, September 1994: Proceedings, volume 859 of Lecture Notes in
Computer Science, pages 193-204. Springer-Verlag, 1994. [ bib | .ps.gz ] |
| [148] |
D. A. Fura and A. K. Somani.
An interpreter interface language: From its formal embedding in
higher-order logic to its role in better simulation practices.
In T. F. Melham and J. Camilleri, editors, Supplementary
Proceedings of the 7th International Workshop on Higher Order Logic Theorem
Proving and its Applications. University of Malta, Valletta, 1994. [ bib | .ps.gz ] |
| [149] |
D. A. Fura and A. K. Somani.
Intervel-semantic component models and the efficient verification of
transaction-level circuit behavior.
In T. F. Melham and J. Camilleri, editors, Higher Order Logic
Theorem Proving and Its Applications: 7th International Workshop, Valletta,
Malta, September 1994: Proceedings, volume 859 of Lecture Notes in
Computer Science, pages 205-220. Springer-Verlag, 1994. [ bib ] |
| [150] |
D. A. Fura, P. J. Windley, and A. K. Somani.
Abstraction techniques for modeling real-world interface chips.
In J. J. Joyce and C.-J. H. Seger, editors, Higher Order Logic
Theorem Proving and its Applications: 6th International Workshop, HUG'93,
Vancouver, B.C., August 11-13 1993: Proceedings, volume 780 of
Lecture Notes in Computer Science, pages 267-280. Springer-Verlag, 1994. [ bib ] |
| [151] |
J. W. Gambles and P. J. Windley.
An HOL theory for logic states with indeterminate strengths.
In M. Archer, J. J. Joyce, K. N. Levit, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 96-103.
IEEE Computer Society Press, 1992. [ bib ] |
| [152] |
R. Gerber, E. L. Gunter, and I. Lee.
Implementing a real-time process algebra in HOL.
In M. Archer, J. J. Joyce, K. N. Levit, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 144-154.
IEEE Computer Society Press, 1992. [ bib ] |
| [153] |
A. Gordon.
The formal definition of a synchronous hardware-description language
in higher order logic.
In 1992 IEEE International Conference on Computer Design: VLSI
in Computers & Processors, pages 531-534. IEEE Computer Society Press,
1992. [ bib | .dvi.gz ] |
| [154] |
A. Gordon.
A mechanisation of name-carrying syntax up to alpha-conversion.
In J. J. Joyce and C.-J. H. Seger, editors, Higher Order Logic
Theorem Proving and its Applications: 6th International Workshop, HUG'93,
Vancouver, B.C., August 11-13 1993: Proceedings, volume 780 of
Lecture Notes in Computer Science, pages 413-425. Springer-Verlag, 1994. [ bib | .dvi.gz ] |
| [155] |
A. Gordon.
A mechanised definition of SILAGE in HOL.
Technical Report 287, Computer Laboratory, University of Cambridge,
February 1993. [ bib | .dvi.gz ] |
| [156] |
A. D. Gordon and T. Melham.
Five axioms of alpha-conversion.
In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem
Proving in Higher Order Logics: 9th International Conference, Turku,
Finland, August 1996: Proceedings, volume 1125 of Lecture Notes in
Computer Science, pages 173-190. Springer-Verlag, 1996. [ bib ] |
| [157] |
M. Gordon.
HOL: A machine oriented formulation of higher order logic.
Technical Report 68, Computer Laboratory, University of Cambridge,
July 1985. [ bib ] |
| [158] |
M. J. C. Gordon.
HOL: A proof generating system for higher-order logic.
In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends
in Hardware Verification and Automated Theorem Proving, pages 73-128.
Springer-Verlag, 1989. [ bib ] |
| [159] |
M. Gordon.
Introduction to the HOL system.
In M. Archer, J. J. Joyce, K. N. Levit, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 2-3.
IEEE Computer Society Press, 1992. [ bib ] |
| [160] |
M. Gordon.
A mechanized hoare logic of state transitions.
In A. W. Roscoe, editor, A Classical Mind: Essays in Honour of
C. A. R. Hoare, pages 143-159. Prentice-Hall, 1994. [ bib | .ps.gz ] |
| [161] |
M. J. C. Gordon.
Mechanizing programming logics in higher order logic.
In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends
in Hardware Verification and Automated Theorem Proving, pages 387-439.
Springer-Verlag, 1989. [ bib | .dvi.gz ] |
| [162] |
M. J. C. Gordon.
Merging HOL with set theory: preliminary experiments.
Technical Report 353, Computer Laboratory, University of Cambridge,
1994. [ bib | .ps.gz ] |
| [163] |
M. Gordon.
The semantic challenge of verilog HDL.
In Proceedings, Tenth Annual IEEE Symposium on Logic in
Computer Science, pages 136-145. IEEE Computer Society Press, 1995. [ bib | .ps.gz ] |
| [164] |
M. Gordon.
Set theory, higher order logic or both?
In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem
Proving in Higher Order Logics: 9th International Conference, Turku,
Finland, August 1996: Proceedings, volume 1125 of Lecture Notes in
Computer Science, pages 191-201. Springer-Verlag, 1996. [ bib ] |
| [165] |
M. J. C. Gordon.
State transition assertions: A case study.
In J. Bowen, editor, Towards Verified Systems, volume 2 of
Real-Time Safety Critical Systems Series, pages 93-113. Elsevier, 1994. [ bib ] |
| [166] |
M. J. C. Gordon.
A verifier and timing analyser for simple imperative programs
(abstract).
In C. Courcoubetis, editor, Computer Aided Verification: 5th
International Conference, CAV'93: Elounda, Greece: Proceedings, volume
697 of Lecture Notes in Computer Science, page 320. Springer-Verlag,
1993. [ bib ] |
| [167] |
M. Gordon.
Why higher-order logic is a good formalism for specifying and
verifying hardware.
In G. J. Milne and P. A. Subrahmanyam, editors, Formal Aspects
of VLSI Design Proceedings of the 1985 Edinburgh Conference on VLSI,
Lecture Notes in Computer Science, pages 153-177. North-Holland, 1986. [ bib ] |
| [168] |
M. Gordon, P. Loewenstein, and M. Shahaf.
Formal verification of a cell library: a case study in technology
transfer.
In L. J. M. Claesen, editor, 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, Belgium, November 1989, pages 409-417. North-Holland, 1990. [ bib ] |
| [169] |
M. J. C. Gordon and T. F. Melham, editors.
Introduction to HOL: A theorem proving environment for higher
order logic.
Cambridge University Press, 1993. [ bib | .html ] |
| [170] |
M. J. C. Gordon and A. M. Pitts.
The HOL logic and system.
In J. Bowen, editor, Towards Verified Systems, volume 2 of
Real-Time Safety Critical Systems Series, pages 49-70. Elsevier, 1994. [ bib ] |
| [171] |
B. T. Graham.
An interpretation of NODEN in HOL.
In T. F. Melham and J. Camilleri, editors, Higher Order Logic
Theorem Proving and Its Applications: 7th International Workshop, Valletta,
Malta, September 1994: Proceedings, volume 859 of Lecture Notes in
Computer Science, pages 221-234. Springer-Verlag, 1994. [ bib ] |
| [172] |
B. T. Graham.
SECD: The design and verification of a functional microprocessor.
Master's thesis, Department of Computer Science, University of
Calgary, June 1990. [ bib ] |
| [173] |
B. T. Graham.
The SECD Microprocessor: A Verification Case Study.
Kluwer, 1992. [ bib ] |
| [174] |
B. Graham and G. Birtwistle.
Formalising the design of an SECD chip.
In M. Leeser and G. Brown, editors, Hardware Specification,
Verification and Synthesis: Mathematical Aspects: Mathematical Sciences
Institute Workshop, Cornell, July 1989, volume 408 of Lecture Notes
in Computer Science, pages 40-66. Springer-Verlag, 1990. [ bib ] |
| [175] |
R. Groenboom, C. Hendriks, I. Polak, J. Terlouw, and J. T. Udding.
Algebraic proof assistants in HOL.
In B. Möller, editor, Mathematics of Program Construction:
Third International Conference, MPC'95: Kloster Irsee, July 1995:
Proceedings, volume 947 of Lecture Notes in Computer Science, pages
304-321. Springer-Verlag, 1995. [ bib | .dvi.Z ] |
| [176] |
J. Grundy.
A method of program refinement.
Technical Report 318, Computer Laboratory, University of Cambridge,
November 1993. [ bib | .html ] |
| [177] |
J. Grundy.
Window inference in the HOL system.
In M. Archer, J. J. Joyce, K. N. Levit, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 177-189.
IEEE Computer Society Press, 1992. [ bib | .html ] |
| [178] |
J. Grundy.
A window inference tool for refinement.
In C. B. Jones, B. T. Denvir, and Roger C. F. Shaw, editors,
Proceedings of the 5th Refinement Workshop, volume 947 of Lecture Notes
in Computer Science, pages 240-254. Springer-Verlag, 1992. [ bib | .html ] |
| [179] |
Jim Grundy and Thomas Långbacka.
Recording HOL proofs in a structured browsable format.
In Michael Johnson, editor, Algebraic Methodology and Software
Technology: 6th International Conference, AMAST'97, volume 1349 of
Lecture Notes in Computer Science, pages 567-571, Sydney, Australia,
December 1997. Springer-Verlag. [ bib ] |
| [180] |
J. Grundy and T. Långbacka.
Towards a browsable record of HOL proofs.
Technical Report 7, Turku Centre for Computer Science, May 1996. [ bib | .html ] |
| [181] |
J. J. Joyce and C.-J. H. Seger, editors.
A Broader Class of Trees for Recursive Type Definitions for
HOL, volume 780 of Lecture Notes in Computer Science.
Springer-Verlag, 1994. [ bib ] |
| [182] |
E. L. Gunter.
Doing algebra in simple type theory.
Technical Report MS-CIS-89-38, Department of Computer and Information
Science, Moore School of Engineering,University of Pennsylvania, June 1989.
Distributed with the HOL system in
Training/studies/int_mod/doing_alg_paper. [ bib ] |
| [183] |
E. L. Gunter.
Why we can't have SML style datatype declarations in HOL.
In L. J. M. Claesen and M. J. C. Gordon, editors, Higher Order
Logic Theorem Proving and its Applications: Proceedings of the IFIP
TC10/WG10.2 International Workshop, Leuven, September 1992, IFIP
Transactions A-20, pages 561-568. North-Holland, 1993. [ bib ] |
| [184] |
E. L. Gunter and L. Libkin.
Interfacing HOL90 with a functional database query language.
In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors,
Higher Order Logic Theorem Proving and Its Applications: 8th International
Workshop, Aspen Grove, Utah, September 1995: Proceedings, volume 971
of Lecture Notes in Computer Science, pages 170-185. Springer-Verlag,
1995. [ bib | .html ] |
| [185] |
M. Hagiya, H. Tanaka, M. Yamamoto, and S. Nishizaki.
Problem solving with tactics.
In J. von Wright, J. Grundy, and J. Harrison, editors,
Supplementary Proceedings of the 9th International Conference on Theorem
Proving in Higher Order Logics: TPHOLs'96, number 1 in TUCS General
Publication, pages 31-43. Turku Centre for Computer Science, August 1996. [ bib | .html ] |
| [186] |
R. W. S. Hale.
Program compilation.
In J. Bowen, editor, Towards Verified Systems, volume 2 of
Real-Time Safety Critical Systems Series, pages 131-146. Elsevier, 1994. [ bib ] |
| [187] |
R. Hale.
Reasoning about software.
In M. Archer, J. J. Joyce, K. N. Levit, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 52-58.
IEEE Computer Society Press, 1992. [ bib ] |
| [188] |
R. Hale, R. Cardell-Oliver, and J. Herbert.
An embedding of timed transition systems in HOL.
Formal Methods in System Design, 3(1-2):151-174, August 1993. [ bib ] |
| [189] |
R. W. S. Hale, R. M. Cardell-Oliver, and J. M. J. Herbert.
Timed transition systems.
In J. Bowen, editor, Towards Verified Systems, volume 2 of
Real-Time Safety Critical Systems Series, pages 71-90. Elsevier, 1994. [ bib ] |
| [190] |
R. W. S. Hale and H. Jifeng.
A real-time programming language.
In J. Bowen, editor, Towards Verified Systems, volume 2 of
Real-Time Safety Critical Systems Series, pages 115-130. Elsevier, 1994. [ bib ] |
| [191] |
K. M. Hall and P. J. Windley.
Simulating microprocessors from formal specifications.
In L. J. M. Claesen and M. J. C. Gordon, editors, Higher Order
Logic Theorem Proving and its Applications: Proceedings of the IFIP
TC10/WG10.2 International Workshop, Leuven, September 1992, IFIP
Transactions A-20, pages 507-525. North-Holland, 1993. [ bib ] |
| [192] |
W. A. Halang, B. Krämer, and L. Trybus.
Exploiting a graphical programming paradigm to facilitate rigorous
verification of embedded software.
The Computer Journal, 38(4):301-309, 1995. [ bib ] |
| [193] |
J. Harrison.
Binary decision diagrams as a HOL derived rule.
The Computer Journal, 38(2):162-170, July 1995. [ bib | .ps ] |
| [194] |
J. Harrison.
Binary decision diagrams as a HOL derived rule.
In T. F. Melham and J. Camilleri, editors, Higher Order Logic
Theorem Proving and Its Applications: 7th International Workshop, Valletta,
Malta, September 1994: Proceedings, volume 859 of Lecture Notes in
Computer Science, pages 254-268. Springer-Verlag, 1994. [ bib ] |
| [195] |
J. Harrison.
Constructing the real numbers in HOL.
Formal Methods in System Design, 5(1-2):35-59, July 1994. [ bib | .ps.gz ] |
| [196] |
J. Harrison.
Constructing the real numbers in HOL.
In L. J. M. Claesen and M. J. C. Gordon, editors, Higher Order
Logic Theorem Proving and its Applications: Proceedings of the IFIP
TC10/WG10.2 International Workshop, Leuven, September 1992, IFIP
Transactions A-20, pages 145-164. North-Holland, 1993. [ bib ] |
| [197] |
J. Harrison.
Finding proofs and checking proofs.
In H. Stoyan, K. Homann, S. Jacob, and M. Kerber, editors,
ECAI96: 12th European Conference on Artificial Intelligence, Workshop on
Representation of Mathematical Knowledge: Proceedings. Budapest, 1996. [ bib | .html ] |
| [198] |
J. Harrison.
Floating point verification in HOL.
In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors,
Higher Order Logic Theorem Proving and Its Applications: 8th International
Workshop, Aspen Grove, Utah, September 1995: Proceedings, volume 971
of Lecture Notes in Computer Science, pages 186-199. Springer-Verlag,
1995. [ bib | .dvi.gz ] |
| [199] |
J. J. Joyce and C.-J. H. Seger, editors.
A HOL Decision Procedure for Elementary Real Algebra, volume
780 of Lecture Notes in Computer Science. Springer-Verlag, 1994. [ bib | .dvi.gz ] |
| [200] |
J. Harrison.
Inductive definitions: automation and applications.
In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors,
Higher Order Logic Theorem Proving and Its Applications: 8th International
Workshop, Aspen Grove, Utah, September 1995: Proceedings, volume 971
of Lecture Notes in Computer Science, pages 200-213. Springer-Verlag,
1995. [ bib | .dvi.gz ] |
| [201] |
J. Harrison.
Metatheory and reflection in theorem proving: A survey and critique.
Technical Report CRC-53, SRI International, Cambridge Computer
Science Research Centre, February 1995. [ bib | .dvi.gz ] |
| [202] |
J. Harrison.
A mizar mode for HOL.
In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem
Proving in Higher Order Logics: 9th International Conference, Turku,
Finland, August 1996: Proceedings, volume 1125 of Lecture Notes in
Computer Science, pages 203-220. Springer-Verlag, 1996. [ bib ] |
| [203] |
J. Harrison.
Pure mathematics in a mechanized logic.
In C. Gefwert, P. Orponen, and J. Seppänen, editors,
Proceedings of the Finnish Artificial Intelligence Society Symposium:
Logic, Mathematics and the Computer, volume 14 of Suomen
Tekoälyseuran julkaisuja, pages 153-169. Finnish Artificial
Intelligence Society, 1996. [ bib | .html ] |
| [204] |
J. Harrison.
Stålmarck's algorithm as a HOL derived rule.
In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem
Proving in Higher Order Logics: 9th International Conference, Turku,
Finland, August 1996: Proceedings, volume 1125 of Lecture Notes in
Computer Science, pages 221-234. Springer-Verlag, 1996. [ bib ] |
| [205] |
J. Harrison.
Theorem proving with the real numbers.
Technical Report 408, University of Cambridge Computer Laboratory,
1996. [ bib | .html ] |
| [206] |
J. Harrison and K. Slind.
A reference version of HOL.
In T. F. Melham and J. Camilleri, editors, Proceedings of the
7th International Workshop on Higher Order Logic Theorem Proving and its
Applications. University of Malta, Valletta, 1994. [ bib | .ps.gz ] |
| [207] |
J. Harrison and L. Théry.
Extending the HOL theorem prover with a computer algebra system to
reason about the reals.
In J. J. Joyce and C.-J. H. Seger, editors, Higher Order Logic
Theorem Proving and its Applications: 6th International Workshop, HUG'93,
Vancouver, B.C., August 11-13 1993: Proceedings, volume 780 of
Lecture Notes in Computer Science, pages 174-184. Springer-Verlag, 1994. [ bib | .ps.gz ] |
| [208] |
J. Harrison and L. Théry.
Reasoning about the reals: the marriage of HOL and maple.
In A. Voronkov, editor, Logic Programming and Automated
Reasoning: 4th International Conference, St. Petersburg: Proceedings,
volume 698 of Lecture Notes in Artificial Intelligence, pages 351-353.
Springer-Verlag, 1993. [ bib | .ps.gz ] |
| [209] |
W. L. Harrison.
Mechanizing security in HOL.
In M. Archer, J. J. Joyce, K. N. Levit, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 63-66.
IEEE Computer Society Press, 1992. [ bib ] |
| [210] |
W. L. Harrison, M. A. Archer, and K. N. Levitt.
A HOL mechanization of the axiomatic semantics of a simple
distributed programming language.
In L. J. M. Claesen and M. J. C. Gordon, editors, Higher Order
Logic Theorem Proving and its Applications: Proceedings of the IFIP
TC10/WG10.2 International Workshop, Leuven, September 1992, IFIP
Transactions A-20, pages 347-359. North-Holland, 1993. [ bib ] |
| [211] |
M. R. Heckman, C. Zhang, B. R. Becker, D. Peticolas, K. N. Levitt, and R. A.
Olsson.
Towards applying the composition principle to verify a microkernel
operating system.
In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem
Proving in Higher Order Logics: 9th International Conference, Turku,
Finland, August 1996: Proceedings, volume 1125 of Lecture Notes in
Computer Science, pages 235-250. Springer-Verlag, 1996. [ bib ] |
| [212] |
L. Henschen.
Review of introduction to HOL, edited by M. Gordon and T.
Melham (cambridge university press, 1993.
Computing Reviews, 35(8):400-401, August 1994. [ bib ] |
| [213] |
J. M. J. Herbert.
Application of Formal Methods to Digital System Design.
PhD thesis, University of Cambridge Computer Laboratory, 1986. [ bib ] |
| [214] |
J. Herbert.
Dealing with temporal complexity in hardware verification.
In M. Archer, J. J. Joyce, K. N. Levit, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 13-21.
IEEE Computer Society Press, 1992. [ bib ] |
| [215] |
J. Herbert.
Formal reasoning about the timing and function of basic memory
devices.
In L. J. M. Claesen, editor, 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, Belgium, November 1989, pages 379-298. North-Holland, 1990. [ bib ] |
| [216] |
J. M. J. Herbert.
A framework for microprocessor design.
In J. Bowen, editor, Towards Verified Systems, volume 2 of
Real-Time Safety Critical Systems Series, pages 149-165. Elsevier, 1994. [ bib ] |
| [217] |
J. Herbert.
Incremental design and formal verification of microcoded
microprocessors.
In V. Stavridou, T. F. Melham, and R. T. Boute, editors, Theorem
Provers in Circuit Design: Proceedings of the IFIP TC10/WG 10.2
International Conference, Nijmegen, June 1992, IFIP Transactions A-10,
pages 157-174. North-Holland, 1992. [ bib | .html ] |
| [218] |
P. V. Homeier.
Trustworthy Tools for Trustworthy Programs: A Mechanically
Verified Verification Condition Generator for the Total Correctness of
Procedures.
PhD thesis, University of California Los Angeles, June 1995. [ bib | .html ] |
| [219] |
P. V. Homeier and D. F. Martin.
Trustworthy tools for trustworthy programs: Automatic verification of
mutually recursive procedures.
In T. F. Melham and J. Camilleri, editors, Supplementary
Proceedings of the 7th International Workshop on Higher Order Logic Theorem
Proving and its Applications. University of Malta, Valletta, 1994. [ bib | .ps.gz ] |
| [220] |
P. V. Homeier and D. F. Martin.
Trustworthy tools for trustworthy programs: A verified verification
condition generator.
In T. F. Melham and J. Camilleri, editors, Higher Order Logic
Theorem Proving and Its Applications: 7th International Workshop, Valletta,
Malta, September 1994: Proceedings, volume 859 of Lecture Notes in
Computer Science, pages 269-284. Springer-Verlag, 1994. [ bib | .ps.Z ] |
| [221] |
P. V. Homeier and D. F. Martin.
A verified verification condition generator.
The Computer Journal, 38(2):131-141, July 1995. [ bib | .ps ] |
| [222] |
D. J. Howe.
Importing mathematics from HOL into Nuprl.
In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem
Proving in Higher Order Logics: 9th International Conference, Turku,
Finland, August 1996: Proceedings, volume 1125 of Lecture Notes in
Computer Science, pages 267-281. Springer-Verlag, 1996. [ bib ] |
| [223] |
M. A. Hutchins.
Machine Assisted Reasoning about Standard ML Using HOL.
PhD thesis, Australian National University, November 1990. [ bib ] |
| [224] |
G. Hutton.
Review of introduction to HOL, edited by M. Gordon and T.
Melham (Cambridge university press, 1993).
Journal of Functional Programming, 4(4):557-559, October 1994. [ bib ] |
| [225] |
S. Ikram and S.-K. Chin.
A process algebra for instruction-set architecture design.
In J. Alves-Foss, editor, HOL-95: International Workshop on
Higher Order Logic Theorem Proving and its Applications: B-Track: Short
Presentations, Aspen Grove, Utah, September, 1995, pages 33-44,
1995. [ bib | .ps ] |
| [226] |
B. Jacobs and T. Melham.
Translating dependent type theory into higher order logic.
In M. Bezem and J. F. Groote, editors, Typed Lambda Calculi and
Applications: Proceedings of the International Conference, Utrecht, March
1993, volume 664 of Lecture Notes in Computer Science, pages 209-229.
Springer-Verlag, 1993. [ bib | .ps ] |
| [227] |
M. D. Jones.
Representing Abstract Theories using Predicate Types.
PhD thesis, Brigham Young University, June 1997. [ bib | .ps.gz ] |
| [228] |
M. D. Jones, T. N. Larson, and P. J. Windley.
Toward <tt>GHDL_EVAL</tt>: A framework for deeply embedding simple
HDLs in HOL.
In J. von Wright, J. Grundy, and J. Harrison, editors,
Supplementary Proceedings of the 9th International Conference on Theorem
Proving in Higher Order Logics: TPHOLs'96, number 1 in TUCS General
Publication, pages 45-56. Turku Centre for Computer Science, August 1996. [ bib | .html ] |
| [229] |
J. J. Joyce.
Formal verification and implementation of a microprocessor.
In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends
in Hardware Verification and Automated Theorem Proving, pages 129-157.
Springer-Verlag, 1989. [ bib ] |
| [230] |
J. J. Joyce.
Generic specification of digital hardware.
In G. Jones and M. Sheeran, editors, Designing Correct Circuits:
September 1990, Oxford, Workshops in Computing Series, pages 68-91.
Springer-Verlag, 1991. [ bib ] |
| [231] |
J. J. Joyce.
Multi-level verification of microprocessor-based systems.
Technical Report 195, University of Cambridge Computer Laboratory,
May 1990. [ bib ] |
| [232] |
J. J. Joyce.
Totally verified systems: Linking verified software to verified
hardware.
In M. Leeser and G. Brown, editors, Hardware Specification,
Verification and Synthesis: Mathematical Aspects: Mathematical Sciences
Institute Workshop, Cornell, July 1989, volume 408 of Lecture Notes
in Computer Science, pages 177-201. Springer-Verlag, 1990. [ bib ] |
| [233] |
J. J. Joyce and C.-J. H. Seger, editors.
Higher Order Logic Theorem Proving and its Applications: 6th
International Workshop, HUG'93, Vancouver, B.C., August 11-13 1993:
Proceedings, volume 780 of Lecture Notes in Computer Science.
Springer-Verlag, 1994. [ bib ] |
| [234] |
J. Joyce and C. Seger.
The HOL-voss system: Model-checking inside a general-purpose
theorem-prover.
In J. J. Joyce and C.-J. H. Seger, editors, Higher Order Logic
Theorem Proving and its Applications: 6th International Workshop, HUG'93,
Vancouver, B.C., August 11-13 1993: Proceedings, volume 780 of
Lecture Notes in Computer Science, pages 185-198. Springer-Verlag, 1994. [ bib ] |
| [235] |
S. Kalvala.
Annotations in formal specifications and proofs.
Formal Methods in System Design, 5(1-2):119-144, July 1994. [ bib ] |
| [236] |
S. Kalvala.
Developing an interface for HOL.
In M. Archer, J. J. Joyce, K. N. Levit, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 305-317.
IEEE Computer Society Press, 1992. [ bib ] |
| [237] |
S. Kalvala.
HOL around the world.
In M. Archer, J. J. Joyce, K. N. Levit, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 4-12.
IEEE Computer Society Press, 1992. [ bib ] |
| [238] |
S. Kalvala, M. Archer, and K. Levitt.
Implementation and use of annotations in HOL.
In L. J. M. Claesen and M. J. C. Gordon, editors, Higher Order
Logic Theorem Proving and its Applications: Proceedings of the IFIP
TC10/WG10.2 International Workshop, Leuven, September 1992, IFIP
Transactions A-20, pages 407-426. North-Holland, 1993. [ bib ] |
| [239] |
J. D. Kim and S.-K. Chin.
Formal verification of serial pipeline multipliers.
In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors,
Higher Order Logic Theorem Proving and Its Applications: 8th International
Workshop, Aspen Grove, Utah, September 1995: Proceedings, volume 971
of Lecture Notes in Computer Science, pages 229-244. Springer-Verlag,
1995. [ bib ] |
| [240] |
T. Kropf, R. Kumar, and K. Schneider.
Embedding hardware verification within a commercial design framework.
In G. J. Milne and L. Pierre, editors, Correct Hardware Design
and Verification Methods: IFIP WG10.2 Advanced Research Working Conference:
Proceedings, volume 683 of Lecture Notes in Computer Science, pages
242-257. Springer-Verlag, 1994. [ bib | .ps.gz ] |
| [241] |
T. Kropf, K. Schneider, and R. Kumar.
A formal framework for high level synthesis.
In R. Kumar and T. Kropf, editors, Theorem Provers in Circuit
Design: Theory, Practice and Experience: Proceedings, volume 901 of
Lecture Notes in Computer Science, pages 223-238. Springer-Verlag, 1995. [ bib | .ps.gz ] |
| [242] |
R. Kumar, T. Kropf, and K. Schneider.
First steps towards automating hardware proofs in HOL.
In M. Archer, J. J. Joyce, K. N. Levit, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 190-193.
IEEE Computer Society Press, 1992. [ bib ] |
| [243] |
R. Kumar, T. Kropf, and K. Schneider.
Integrating a first-order automatic prover in the HOL environment.
In M. Archer, J. J. Joyce, K. N. Levit, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 170-176.
IEEE Computer Society Press, 1992. [ bib ] |
| [244] |
R. Kumar, K. Schneider, and T. Kropf.
Structuring and automating hardware proofs in a higher-order
theorem-proving environment.
Formal Methods in System Design, 2(2):165-223, April 1993. [ bib ] |
| [245] |
L. Laibinis.
Using lattice theory in higher order logic.
In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem
Proving in Higher Order Logics: 9th International Conference, Turku,
Finland, August 1996: Proceedings, volume 1125 of Lecture Notes in
Computer Science, pages 315-330. Springer-Verlag, 1996. [ bib ] |
| [246] |
T. Långbacka.
A HOL formalisation of the temporal logic of actions.
In T. F. Melham and J. Camilleri, editors, Higher Order Logic
Theorem Proving and Its Applications: 7th International Workshop, Valletta,
Malta, September 1994: Proceedings, volume 859 of Lecture Notes in
Computer Science, pages 332-345. Springer-Verlag, 1994. [ bib ] |
| [247] |
T. Långbacka, R. Ruksenas, and J. von Wright.
TkWinHOL: A tool for window inference in HOL.
In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors,
Higher Order Logic Theorem Proving and Its Applications: 8th International
Workshop, Aspen Grove, Utah, September 1995: Proceedings, volume 971
of Lecture Notes in Computer Science, pages 245-260. Springer-Verlag,
1995. [ bib ] |
| [248] |
M. Larsson.
An engineering approach to formal digital system design.
The Computer Journal, 38(2):101-110, July 1995. [ bib | .ps ] |
| [249] |
M. Larsson.
An engineering approach to formal digital system design.
In T. F. Melham and J. Camilleri, editors, Higher Order Logic
Theorem Proving and Its Applications: 7th International Workshop, Valletta,
Malta, September 1994: Proceedings, volume 859 of Lecture Notes in
Computer Science, pages 300-315. Springer-Verlag, 1994. [ bib ] |
| [250] |
M. Larsson.
Improving the result of high-level synthesis using interactive
transformational design.
In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem
Proving in Higher Order Logics: 9th International Conference, Turku,
Finland, August 1996: Proceedings, volume 1125 of Lecture Notes in
Computer Science, pages 299-314. Springer-Verlag, 1996. [ bib ] |
| [251] |
M. Larsson.
A Transformational Approach to Formal Digital System Design.
PhD thesis, Department of Computer and Information Science,
Linköping University, May 1993.
Licentiate of Engineering Dissertation, Thesis number 378. [ bib ] |
| [252] |
M. Larsson and A. D. Gordon.
A HOL embedding of a small parallel HDL.
In J. Alves-Foss, editor, HOL-95: International Workshop on
Higher Order Logic Theorem Proving and its Applications: B-Track: Short
Presentations, Aspen Grove, Utah, September, 1995, pages 45-60,
1995. [ bib | .ps ] |
| [253] |
P. Loewenstein.
A formal theory of simulations between infinite automata.
Formal Methods in System Design, August:35-59, 1993. [ bib | www ] |
| [254] |
P. Loewenstein.
A formal theory of simulations between infinite automata.
In L. J. M. Claesen and M. J. C. Gordon, editors, Higher Order
Logic Theorem Proving and its Applications: Proceedings of the IFIP
TC10/WG10.2 International Workshop, Leuven, September 1992, IFIP
Transactions A-20, pages 227-246. North-Holland, 1993. [ bib ] |
| [255] |
P. Loewenstein.
Formal verification of counterflow pipeline architecture.
In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors,
Higher Order Logic Theorem Proving and Its Applications: 8th International
Workshop, Aspen Grove, Utah, September 1995: Proceedings, volume 971
of Lecture Notes in Computer Science, pages 261-276. Springer-Verlag,
1995. [ bib | .html ] |
| [256] |
P. Loewenstein.
Learning to use HOL.
In M. Archer, J. J. Joyce, K. N. Levit, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 67-74.
IEEE Computer Society Press, 1992. [ bib ] |
| [257] |
P. Loewenstein.
Reasoning about state machines in higher-order logic.
In M. Leeser and G. Brown, editors, Hardware Specification,
Verification and Synthesis: Mathematical Aspects: Mathematical Sciences
Institute Workshop, Cornell, July 1989, volume 408 of Lecture Notes
in Computer Science, pages 67-89. Springer-Verlag, 1990. [ bib ] |
| [258] |
P. Loewenstein.
Temporal transformation of state machines using higher order logic.
In L. J. M. Claesen, editor, 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, Belgium, November 1989, pages 171-186. North-Holland, 1990. [ bib ] |
| [259] |
P. Loewenstein and D. L. Dill.
Verification of a multiprocessor cache protocol using simulation
relations and higher-order logic.
Formal Methods in System Design, 1(4):355-383, December 1992. [ bib ] |
| [260] |
P. Loewenstein and D. L. Dill.
Verification of a multiprocessor cache protocol using simulation
relations and higher-order logic.
In E. M. Clarke and R. P. Kurshan, editors, Computer-Aided
Verifiction: 2nd International Conference, CAV'90: New Brunswick, 1990:
Proceedings, volume 531 of Lecture Notes in Computer Science, pages
302-311. Springer-Verlag, 1991. [ bib ] |
| [261] |
J.-Y. Lu and S.-K. Chin.
Generating designs using an algorithmic register transfer language
with formal semantics.
In T. F. Melham and J. Camilleri, editors, Higher Order Logic
Theorem Proving and Its Applications: 7th International Workshop, Valletta,
Malta, September 1994: Proceedings, volume 859 of Lecture Notes in
Computer Science, pages 316-331. Springer-Verlag, 1994. [ bib ] |
| [262] |
J.-Y. Lu and S.-K. Chin.
Linking higher order logic to a VLSI CAD system.
In J. J. Joyce and C.-J. H. Seger, editors, Higher Order Logic
Theorem Proving and its Applications: 6th International Workshop, HUG'93,
Vancouver, B.C., August 11-13 1993: Proceedings, volume 780 of
Lecture Notes in Computer Science, pages 199-212. Springer-Verlag, 1994. [ bib ] |
| [263] |
M. McAllister.
Machine abstraction in microprocessor specification.
In L. J. M. Claesen and M. J. C. Gordon, editors, Higher Order
Logic Theorem Proving and its Applications: Proceedings of the IFIP
TC10/WG10.2 International Workshop, Leuven, September 1992, IFIP
Transactions A-20, pages 211-224. North-Holland, 1993. [ bib ] |
| [264] |
D. MacKenzie.
The fangs of the VIPER.
Nature, 352:467-468, August 1991. [ bib ] |
| [265] |
S. Maharaj and E. Gunter.
Studying the ML module system in HOL.
The Computer Journal, 38(2):142-151, July 1995. [ bib | .ps ] |
| [266] |
S. Maharaj and E. Gunter.
Studying the ML module system in HOL.
In T. F. Melham and J. Camilleri, editors, Higher Order Logic
Theorem Proving and Its Applications: 7th International Workshop, Valletta,
Malta, September 1994: Proceedings, volume 859 of Lecture Notes in
Computer Science, pages 346-361. Springer-Verlag, 1994. [ bib ] |
| [267] |
D. F. Martin and R. J. Toal.
Case studies in compiler correctness using HOL.
In M. Archer, J. J. Joyce, K. N. Levit, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 242-252.
IEEE Computer Society Press, 1992. [ bib ] |
| [268] |
T. Melham.
Abstraction mechanisms for hardware verification.
In G. Birtwistle and P. A. Subrahmanyam, editors, VLSI
Specification, Verification and Synthesis, pages 267-291. Kluwer, 1988. [ bib ] |
| [269] |
T. F. Melham.
Automating recursive type definitions in higher order logic.
In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends
in Hardware Verification and Automated Theorem Proving, pages 341-386.
Springer-Verlag, 1989. [ bib | .ps.gz ] |
| [270] |
T. F. Melham.
Formalizing abstraction mechanisms for hardware verification in
higher order logic.
Technical Report 201, University of Cambridge Computer Laboratory,
August 1990. [ bib ] |
| [271] |
T. Melham.
Higher Order Logic and Hardware Verification, volume 31 of
Cambridge Tracts in Theoretical Computer Science.
Cambridge University Press, 1993. [ bib | .html ] |
| [272] |
T. F. Melham.
The HOL logic extended with quantification over type variables.
Formal Methods in System Design, 3(1-2):7-24, August 1992. [ bib | .ps.gz ] |
| [273] |
T. F. Melham.
A mechanized theory of the pi-calculus in HOL.
Nordic Journal of Computing, 1(1):50-76, Spring 1994. [ bib | .ps.gz ] |
| [274] |
T. F. Melham.
A package for inductive relation definitions in HOL.
In M. Archer, J. J. Joyce, K. N. Levit, and P. J. Windley, editors,
Proceedings of the 1991 International Workshop on the HOL Theorem
Proving System and its Applications, Davis, August 1991, pages 350-357.
IEEE Computer Society Press, 1992. [ bib | .ps.gz ] |
| [275] |
T. F. Melham.
Using recursive types to reason about hardware in higher order logic.
In J. Staunstrup, editor, The Fusion of Hardware Design and
Verification: Proceedings of the IFIP WG 10.2 Working Conference,
Glasgow, July 1988, pages 27-50. North-Holland, 1988. [ bib | .ps.gz ] |
| [276] |
T. F. Melham and J. Camilleri, editors.
Higher Order Logic Theorem Proving and Its Applications: 7th
International Workshop, Valletta, Malta, September 1994: Proceedings,
volume 859 of Lecture Notes in Computer Science. Springer-Verlag, 1994. [ bib | .ps ] |
| [277] |
T. F. Melham and J. Camilleri, editors.
Supplementary Proceedings of the 7th International Workshop on
Higher Order Logic Theorem Proving and its Applications. University of
Malta, Valletta, 1994. [ bib | .html ] |
| [278] |
S. W. Moore and B. T. Graham.
Tagged up/down sorter-a hardware priority queue.
The Computer Journal, 38(9):695-703, 1996. [ bib ] |
| [279] |
M. J. Morley.
Safety in railway signalling data: A behavioural analysis.
In J. J. Joyce and C.-J. H. Seger, editors, Higher Order Logic
Theorem Proving and its Applications: 6th International Workshop, HUG'93,
Vancouver, B.C., August 11-13 1993: Proceedings, volume 780 of
Lecture Notes in Computer Science, pages 464-474. Springer-Verlag, 1994. [ bib ] |
| [280] |
Munna and J. Alves-Foss.
Mechanizing a theory of authentication in higher order logic.
In J. Alves-Foss, editor, HOL-95: International Workshop on
Higher Order Logic Theorem Proving and its Applications: B-Track: Short
Presentations, Aspen Grove, Utah, September, 1995, pages 61-72,
1995. [ bib | .ps ] |
| [281] |
M. Mutz.
Using the HOL prove assistant for proving the correctness of term
rewriting rules reducing terms of sequential behaviour.
In K. G. Larsen and A. Skou, editors, Computer Aided
Verification: 3rd International Workshop, CAV'91; Aalborg, 1991:
Proceedings, volume 575 of Lecture Notes in Computer Science, pages
277-287. Springer-Verlag, 1991. [ bib ] |
| [282] |
M. Nesi.
Formalizing a modal logic for ccs in the HOL theorem prover.
In L. J. M. Claesen and M. J. C. Gordon, editors, Higher Order
Logic Theorem Proving and its Applications: Proceedings of the IFIP
TC10/WG10.2 International Workshop, Leuven, September 1992, IFIP
Transactions A-20, pages 279-294. North-Holland, 1993. [ bib ] |
| [283] |
M. Nesi.
Mechanising a modal logic for value-passing agents in HOL.
In B. Steffen and T. Margaria, editors, Proceedings of
INFINITY, International Workshop on Verification of Infinite State Systems,
August 30-31, 1996, Pisa, Italy, pages 139-148, 1996.
Technical Report MIP-9614, Universitat Passau. [ bib ] |
| [284] |
M. Nesi.
Mechanizing a proof by induction of process algebra specifications in
higher order logic.
In K. G. Larsen and A. Skou, editors, Computer Aided
Verification: 3rd International Workshop, CAV'91; Aalborg, 1991:
Proceedings, volume 575 of Lecture Notes in Computer Science, pages
288-298. Springer-Verlag, 1991. [ bib ] |
| [285] |
M. Nesi.
Value-passing ccs in HOL.
In J. J. Joyce and C.-J. H. Seger, editors, Higher Order Logic
Theorem Proving and its Applications: 6th International Workshop, HUG'93,
Vancouver, B.C., August 11-13 1993: Proceedings, volume 780 of
Lecture Notes in Computer Science, pages 352-365. Springer-Verlag, 1994. [ bib ] |