equal
deleted
inserted
replaced
65 {TU Munich, Germany} |
65 {TU Munich, Germany} |
66 {\{urbanc, kaliszyk\}@in.tum.de} |
66 {\{urbanc, kaliszyk\}@in.tum.de} |
67 \maketitle |
67 \maketitle |
68 |
68 |
69 \begin{abstract} |
69 \begin{abstract} |
70 Nominal Isabelle is a definitional extension of the poular Isabelle/HOL theorem |
70 Nominal Isabelle is a definitional extension of the popular Isabelle/HOL |
|
71 theorem |
71 prover. It provides a proving infrastructure for convenient reasoning about |
72 prover. It provides a proving infrastructure for convenient reasoning about |
72 programming language calculi involving named bound variables (as |
73 programming language calculi involving named bound variables (as |
73 opposed to de-Bruijn indices). In this paper we present an extension of |
74 opposed to de-Bruijn indices). In this paper we present an extension of |
74 Nominal Isabelle for dealing with general bindings, that means |
75 Nominal Isabelle for dealing with general bindings, that means |
75 term-constructors where multiple variables are bound at once. Such general |
76 term-constructors where multiple variables are bound at once. Such general |