A Step-Indexing Approach to Partial Functions
ACL, pp. 42-53, 2013.
We describe an ACL2 package for defining partial recursive functions that also supports efficient execution. While packages for defining partial recursive functions already exist for other theorem provers, they often require inductive definitions or recursion operators which are not available in ACL2 and they provide little, if any, sup...More
PPT (Upload PPT)