equal
deleted
inserted
replaced
1 \documentstyle[epsf]{acmconf} |
1 \documentclass{acmconf} |
2 \usepackage{isabelle,isabellesym} |
2 \usepackage{isabelle,isabellesym} |
|
3 |
|
4 \ConferenceShortName{ICFP} |
|
5 \ConferenceName{International Conference on Functional Programming} |
3 |
6 |
4 % further packages required for unusual symbols (see also |
7 % further packages required for unusual symbols (see also |
5 % isabellesym.sty), use only when needed |
8 % isabellesym.sty), use only when needed |
6 |
9 |
7 %\usepackage{amssymb} |
10 %\usepackage{amssymb} |
43 |
46 |
44 %-------------------- environment definitions ----------------- |
47 %-------------------- environment definitions ----------------- |
45 \newenvironment{example}[0]{\begin{Example} \it}{\end{Example}} |
48 \newenvironment{example}[0]{\begin{Example} \it}{\end{Example}} |
46 \newenvironment{proof-of}[1]{{\em Proof of #1:}}{} |
49 \newenvironment{proof-of}[1]{{\em Proof of #1:}}{} |
47 |
50 |
|
51 |
48 \begin{document} |
52 \begin{document} |
49 |
53 |
50 \title{\LARGE\bf General Binding Structures in Nominal Isabelle, or How to |
54 \title{\LARGE\bf General Binding Structures in Nominal Isabelle, or How to |
51 Formalise Core-Haskell} |
55 Formalise Core-Haskell} |
52 \maketitle |
56 \maketitle |
53 |
57 |
54 \maketitle |
58 \maketitle |
55 \begin{abstract} |
59 \begin{abstract} |
56 TODO |
60 Nominal Isabelle is a definitional extension of the Isabelle/HOL |
|
61 theorem prover. It provides a reasoning infrastructure for formalisations |
|
62 of programming language calculi. In this paper we present an extension |
|
63 of Nominal Isabelle with general binding constructs. Such constructs |
|
64 are important in formalisation ... |
57 \end{abstract} |
65 \end{abstract} |
58 |
66 |
59 % generated text of all theories |
67 % generated text of all theories |
60 \input{session} |
68 \input{session} |
61 |
69 |