22 \author{Cezary Kaliszyk$^*$ and Christian Urban$^*$} |
23 \author{Cezary Kaliszyk$^*$ and Christian Urban$^*$} |
23 \institute{$^*$ Technical University of Munich, Germany} |
24 \institute{$^*$ Technical University of Munich, Germany} |
24 \maketitle |
25 \maketitle |
25 |
26 |
26 \begin{abstract} |
27 \begin{abstract} |
27 Higher-order logic (HOL), used in a number of theorem provers, is based on a small |
28 Higher-Order Logic (HOL) is based on a small logic kernel, whose only |
28 logic kernel, whose only mechanism for extension is the introduction of safe |
29 mechanism for extension is the introduction of safe definitions and of |
29 definitions and non-empty types. Both extensions are often performed by |
30 non-empty types. Both extensions are often performed in quotient |
30 quotient constructions; for example finite sets are constructed by quotienting |
31 constructions. To ease the work involved with such quotient constructions, we |
31 lists, or integers by quotienting pairs of natural numbers. To ease the work |
32 re-implemented in Isabelle/HOL the quotient package by Homeier. In doing so we |
32 involved with quotient constructions, we re-implemented in Isabelle/HOL the |
33 extended his work in order to deal with compositions of quotients. Also, we |
33 quotient package by Homeier. In doing so we extended his work in order to deal |
34 designed our quotient package so that every step in a quotient construction |
34 with compositions of quotients. Also, we designed our quotient package so that |
35 can be performed separately and as a result we were able to specify completely |
35 every step in a quotient construction can be performed separately and as a |
36 the procedure of lifting theorems from the raw level to the quotient level. |
36 result we were able to specify completely the procedure of lifting theorems from |
37 The importance for programming language research is that many properties of |
37 the raw level to the quotient level. The importance to programming language |
38 programming language calculi are easier to verify over $\alpha$-equated, or |
38 research is that many properties of programming languages are more convenient |
39 $\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 |
42 % generated text of all theories |
42 % generated text of all theories |
43 \input{session} |
43 \input{session} |
44 |
44 |