equal
deleted
inserted
replaced
1 \documentclass{acmconf} |
1 \documentclass{acmconf} |
2 \usepackage{isabelle} |
2 \usepackage{isabelle} |
3 \usepackage{isabellesym} |
3 \usepackage{isabellesym} |
4 \usepackage{amsmath} |
4 \usepackage{amsmath} |
5 \usepackage{amssymb} |
5 \usepackage{amssymb} |
|
6 \usepackage{tikz} |
|
7 \usepackage{pgf} |
|
8 \usepackage{pdfsetup} |
6 |
9 |
7 %\ConferenceShortName{ICFP} |
|
8 %\ConferenceName{International Conference on Functional Programming} |
|
9 |
|
10 \usepackage{pdfsetup} |
|
11 \urlstyle{rm} |
10 \urlstyle{rm} |
12 \isabellestyle{it} |
11 \isabellestyle{it} |
13 |
12 |
14 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
13 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
15 \renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}} |
14 \renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}} |
17 \renewcommand{\isasymequiv}{$\dn$} |
16 \renewcommand{\isasymequiv}{$\dn$} |
18 \renewcommand{\isasymiota}{} |
17 \renewcommand{\isasymiota}{} |
19 \renewcommand{\isasymemptyset}{$\varnothing$} |
18 \renewcommand{\isasymemptyset}{$\varnothing$} |
20 |
19 |
21 |
20 |
22 % for uniform font size |
|
23 %\renewcommand{\isastyle}{\isastyleminor} |
|
24 |
21 |
25 %----------------- theorem definitions ---------- |
22 %----------------- theorem definitions ---------- |
|
23 \newtheorem{Property}{Theorem}[section] |
26 \newtheorem{Theorem}{Theorem}[section] |
24 \newtheorem{Theorem}{Theorem}[section] |
27 \newtheorem{Definition}[Theorem]{Definition} |
25 \newtheorem{Definition}[Theorem]{Definition} |
28 \newtheorem{Example}{\it Example}[section] |
26 \newtheorem{Example}{\it Example}[section] |
29 |
27 |
30 %-------------------- environment definitions ----------------- |
28 %-------------------- environment definitions ----------------- |
39 \maketitle |
37 \maketitle |
40 |
38 |
41 \maketitle |
39 \maketitle |
42 \begin{abstract} |
40 \begin{abstract} |
43 Nominal Isabelle is a definitional extension of the Isabelle/HOL |
41 Nominal Isabelle is a definitional extension of the Isabelle/HOL |
44 theorem prover. It provides a reasoning infrastructure for formalisations |
42 theorem prover. It provides a proving infrastructure for |
45 of programming language calculi. In this paper we present an extension |
43 conveninet reasoning about programming language calculi. In this paper |
46 of Nominal Isabelle with general binding constructs. Such constructs |
44 we present an extension of Nominal Isabelle for dealing with general binding |
47 are important in formalisation ... |
45 structures. Such structures are ubiquitous in programming language research |
|
46 and only very poorly handled by the well-known single abstraction in the |
|
47 lambda-calculus. We give definitions for alpha-equivalence and establish |
|
48 the reasoning structure for alpha-equated terms. For example we provide |
|
49 a strong induction principle that has the variable convention already |
|
50 built in. |
48 \end{abstract} |
51 \end{abstract} |
49 |
52 |
50 %\begin{keywords} |
|
51 %Language formalisations, Isabelle/HOL, POPLmark |
|
52 %\end{keywords} |
|
53 |
53 |
54 |
|
55 % generated text of all theories |
|
56 \input{session} |
54 \input{session} |
57 |
55 |
58 \bibliographystyle{plain} |
56 \bibliographystyle{plain} |
59 \bibliography{root} |
57 \bibliography{root} |
60 |
58 |