equal
deleted
inserted
replaced
1 \documentclass{llncs} |
1 \documentclass{llncs} |
|
2 \usepackage{times} |
2 \usepackage{isabelle} |
3 \usepackage{isabelle} |
3 \usepackage{isabellesym} |
4 \usepackage{isabellesym} |
4 \usepackage{amsmath} |
5 \usepackage{amsmath} |
5 \usepackage{amssymb} |
6 \usepackage{amssymb} |
6 %%\usepackage{amsthm} |
7 %%\usepackage{amsthm} |
58 \newenvironment{proof-of}[1]{{\em Proof of #1:}}{} |
59 \newenvironment{proof-of}[1]{{\em Proof of #1:}}{} |
59 |
60 |
60 |
61 |
61 \begin{document} |
62 \begin{document} |
62 |
63 |
63 \title{General Bindings and Alpha-Equivalence in Nominal Isabelle} |
64 \title{General Bindings and Alpha-Equivalence\\ in Nominal Isabelle} |
64 \author{Christian Urban and Cezary Kaliszyk} |
65 \author{Christian Urban and Cezary Kaliszyk} |
65 \institute{TU Munich, Germany} |
66 \institute{TU Munich, Germany} |
66 %%%{\{urbanc, kaliszyk\}@in.tum.de} |
67 %%%{\{urbanc, kaliszyk\}@in.tum.de} |
67 \maketitle |
68 \maketitle |
68 |
69 |
69 \begin{abstract} |
70 \begin{abstract} |
70 Nominal Isabelle is a definitional extension of the popular Isabelle/HOL |
71 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
71 theorem |
|
72 prover. It provides a proving infrastructure for convenient reasoning about |
72 prover. It provides a proving infrastructure for convenient reasoning about |
73 programming language calculi involving named bound variables (as |
73 programming language calculi involving named bound variables (as |
74 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 |
75 Nominal Isabelle for dealing with general bindings, that means |
75 Nominal Isabelle for dealing with general bindings, that means |
76 term-constructors where multiple variables are bound at once. Such general |
76 term-constructors where multiple variables are bound at once. Such general |