equal
deleted
inserted
replaced
18 \renewcommand{\isasymemptyset}{$\varnothing$} |
18 \renewcommand{\isasymemptyset}{$\varnothing$} |
19 |
19 |
20 |
20 |
21 |
21 |
22 %----------------- theorem definitions ---------- |
22 %----------------- theorem definitions ---------- |
23 \newtheorem{Property}{Theorem}[section] |
23 \newtheorem{property}{Property}[section] |
24 \newtheorem{Theorem}{Theorem}[section] |
24 \newtheorem{Theorem}{Theorem}[section] |
25 \newtheorem{Definition}[Theorem]{Definition} |
25 \newtheorem{Definition}[Theorem]{Definition} |
26 \newtheorem{Example}{\it Example}[section] |
26 \newtheorem{Example}{\it Example}[section] |
27 |
27 |
28 %-------------------- environment definitions ----------------- |
28 %-------------------- environment definitions ----------------- |
36 Formalise Core-Haskell} |
36 Formalise Core-Haskell} |
37 \maketitle |
37 \maketitle |
38 |
38 |
39 \maketitle |
39 \maketitle |
40 \begin{abstract} |
40 \begin{abstract} |
41 Nominal Isabelle is a definitional extension of the Isabelle/HOL |
41 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
42 theorem prover. It provides a proving infrastructure for |
42 prover. It provides a proving infrastructure for convenient reasoning about |
43 conveninet reasoning about programming language calculi. In this paper |
43 programming language calculi. In this paper we present an extension of Nominal |
44 we present an extension of Nominal Isabelle for dealing with general binding |
44 Isabelle for dealing with general binding structures. Such binding structures are |
45 structures. Such structures are ubiquitous in programming language research |
45 ubiquitous in programming language research and only very poorly handled by |
46 and only very poorly handled by the well-known single abstraction in the |
46 single binding from the lambda-calculus. We give in this |
47 lambda-calculus. We give definitions for alpha-equivalence and establish |
47 paper novel definitions for alpha-equivalence and establish automatically the |
48 the reasoning structure for alpha-equated terms. For example we provide |
48 reasoning structure for alpha-equated terms. For example we provide a strong |
49 a strong induction principle that has the variable convention already |
49 induction principle that has the variable convention already built in. |
50 built in. |
|
51 \end{abstract} |
50 \end{abstract} |
52 |
51 |
53 |
52 |
54 \input{session} |
53 \input{session} |
55 |
54 |