@inproceedings{7582fa80f022474681504a7578a71bca,

title = "Implementing a real-time process algebra in HOL",

abstract = "In [6] a real-time process algebra was discussed, a model for the algebra was developed, and the axiomatization was shown to be sound and complete for reasoning about equality and containment of processes for this model. In this work we show how to implement this theory in HOL and to develop a procedure for proving the equality of finite processes.",

author = "Richard Gerber and Gunter, {Elsa L.} and Insup Lee",

note = "Funding Information: 'This research was supported in part by ONR N00014-89-J-1131 Publisher Copyright: {\textcopyright} 1991 Institute of Electrical and Electronics Engineers Inc. All rights reserved. Copyright: Copyright 2020 Elsevier B.V., All rights reserved.; 1991 International Tutorial and Workshop on the HOL Theorem Proving System and Its Applications ; Conference date: 28-08-1991 Through 30-08-1991",

year = "1991",

doi = "10.1109/HOL.1991.596281",

language = "English (US)",

series = "Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and Its Applications",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "144--154",

editor = "Myla Archer and Joyce, {Jeffrey J.} and Levitt, {Karl N.} and Windley, {Phillip J.}",

booktitle = "Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and Its Applications",

address = "United States",

}