30 non-empty types. Both extensions are often performed in quotient |
30 non-empty types. Both extensions are often performed in quotient |
31 constructions. To ease the work involved with such quotient constructions, we |
31 constructions. To ease the work involved with such quotient constructions, we |
32 re-implemented in Isabelle/HOL the quotient package by Homeier. In doing so we |
32 re-implemented in Isabelle/HOL the quotient package by Homeier. In doing so we |
33 extended his work in order to deal with compositions of quotients. Also, we |
33 extended his work in order to deal with compositions of quotients. Also, we |
34 designed our quotient package so that every step in a quotient construction |
34 designed our quotient package so that every step in a quotient construction |
35 can be performed separately and as a result we were able to specify completely |
35 can be performed separately and as a result we are able to specify completely |
36 the procedure of lifting theorems from the raw level to the quotient level. |
36 the procedure of lifting theorems from the raw level to the quotient level. |
37 The importance for programming language research is that many properties of |
37 The importance for programming language research is that many properties of |
38 programming language calculi are easier to verify over $\alpha$-equated, or |
38 programming language calculi are easier to verify over $\alpha$-equated, or |
39 $\alpha$-quotient, terms, than over ``raw'' terms. |
39 $\alpha$-quotient, terms, than over ``raw'' terms. |
40 \end{abstract} |
40 \end{abstract} |