equal
deleted
inserted
replaced
1 \documentclass{article} |
1 \documentclass{acmconf} |
2 %%\documentclass[epsf]{acmconf} |
|
3 \usepackage{isabelle,isabellesym} |
2 \usepackage{isabelle,isabellesym} |
|
3 |
|
4 \ConferenceShortName{ICFP} |
|
5 \ConferenceName{International Conference on Functional Programming} |
4 |
6 |
5 % further packages required for unusual symbols (see also |
7 % further packages required for unusual symbols (see also |
6 % isabellesym.sty), use only when needed |
8 % isabellesym.sty), use only when needed |
7 |
9 |
8 %\usepackage{amssymb} |
10 %\usepackage{amssymb} |
44 |
46 |
45 %-------------------- environment definitions ----------------- |
47 %-------------------- environment definitions ----------------- |
46 \newenvironment{example}[0]{\begin{Example} \it}{\end{Example}} |
48 \newenvironment{example}[0]{\begin{Example} \it}{\end{Example}} |
47 \newenvironment{proof-of}[1]{{\em Proof of #1:}}{} |
49 \newenvironment{proof-of}[1]{{\em Proof of #1:}}{} |
48 |
50 |
|
51 |
49 \begin{document} |
52 \begin{document} |
50 |
53 |
51 \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 |
52 Formalise Core-Haskell} |
55 Formalise Core-Haskell} |
53 \maketitle |
56 \maketitle |
54 |
57 |
55 \maketitle |
58 \maketitle |
56 \begin{abstract} |
59 \begin{abstract} |
57 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 ... |
58 \end{abstract} |
65 \end{abstract} |
59 |
66 |
60 % generated text of all theories |
67 % generated text of all theories |
61 \input{session} |
68 \input{session} |
62 |
69 |