@inproceedings{8930bfd5453c459880ecfd865fc4c10b,
title = "Implementing and verifying finite-state machines using types in higher-order logic",
abstract = "The combination of declarative functional languages, formal logic, and mechanical theorem-pro vers offers the opportunity to extend current CAD tools dealing with finite-state machine synthesis and verification. Theorems are proved showing equivalence between machines under certain correctness conditions. Implementations are related to one another and to specifications where the state, input, and output alphabets are viewed as data types.",
author = "Chin, {Shiu Kai} and Graham Birtwistle",
note = "Publisher Copyright: {\textcopyright} 1991 Institute of Electrical and Electronics Engineers Inc. 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.596279",
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 = "121--129",
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",
}