equal
deleted
inserted
replaced
31 lists, or integers by quotienting pairs of natural numbers. To ease the work |
31 lists, or integers by quotienting pairs of natural numbers. To ease the work |
32 involved with quotient constructions, we re-implemented in Isabelle/HOL the |
32 involved with quotient constructions, we re-implemented in Isabelle/HOL the |
33 quotient package by Homeier. In doing so we extended his work in order to deal |
33 quotient package by Homeier. In doing so we extended his work in order to deal |
34 with compositions of quotients. Also, we designed our quotient package so that |
34 with compositions of quotients. Also, we designed our quotient package so that |
35 every step in a quotient construction can be performed separately and as a |
35 every step in a quotient construction can be performed separately and as a |
36 result were able to specify completely the procedure of lifting theorems from |
36 result we were able to specify completely the procedure of lifting theorems from |
37 the raw level to the quotient level. The importance to programming language |
37 the raw level to the quotient level. The importance to programming language |
38 research is that many properties of programming languages are more convenient |
38 research is that many properties of programming languages are more convenient |
39 to verify over $\alpha$-quotient terms, than over raw terms. |
39 to verify over $\alpha$-quotient terms, than over raw terms. |
40 \end{abstract} |
40 \end{abstract} |
41 |
41 |