NS
N.P. Soekarman
info
Please Note
<p>This page displays the records of the person named above and is not linked to a unique person identifier. This record may need to be merged to a profile.</p>
1 records found
1
Encoding Finite State Automata in Agda using coinduction
Evaluating the support for coinduction in Agda
The proof assistant Agda supports coinduction, which can be used to reason about infinite and cyclic structures. The possibilities and limitations of using coinduction in Agda are not well known. To better understand these, I will implement Finite State Automata and their equivalence in Agda. Finite State Automata (FSA) is an example of a cyclic structure. FSA are an introductory model in computation theory, and can be used text processing and hardware design. Equivalence of two FSA is used in software and hardware verification. I created various encodings for FSA and prove equivalence between two deterministic FSA for each of them. At the end, I compared them and see whether they are limited by the support for coinduction in Agda.
...
The proof assistant Agda supports coinduction, which can be used to reason about infinite and cyclic structures. The possibilities and limitations of using coinduction in Agda are not well known. To better understand these, I will implement Finite State Automata and their equivalence in Agda. Finite State Automata (FSA) is an example of a cyclic structure. FSA are an introductory model in computation theory, and can be used text processing and hardware design. Equivalence of two FSA is used in software and hardware verification. I created various encodings for FSA and prove equivalence between two deterministic FSA for each of them. At the end, I compared them and see whether they are limited by the support for coinduction in Agda.