Implementing And Verifying Finite-state Machines Using Types In Higher-order Logic

The combination of declarative functional languages, formal logic, and mechanical theorem-provers 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.