1 \documentclass{acmconf} |
1 \documentclass{acmconf} |
2 \usepackage{isabelle,isabellesym} |
2 \usepackage{isabelle} |
|
3 \usepackage{isabellesym} |
|
4 \usepackage{amsmath} |
|
5 \usepackage{amssymb} |
3 |
6 |
4 \ConferenceShortName{ICFP} |
7 %\ConferenceShortName{ICFP} |
5 \ConferenceName{International Conference on Functional Programming} |
8 %\ConferenceName{International Conference on Functional Programming} |
6 |
9 |
7 % further packages required for unusual symbols (see also |
|
8 % isabellesym.sty), use only when needed |
|
9 |
|
10 %\usepackage{amssymb} |
|
11 %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>, |
|
12 %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>, |
|
13 %\<triangleq>, \<yen>, \<lozenge> |
|
14 |
|
15 %\usepackage[greek,english]{babel} |
|
16 %option greek for \<euro> |
|
17 %option english (default language) for \<guillemotleft>, \<guillemotright> |
|
18 |
|
19 %\usepackage[latin1]{inputenc} |
|
20 %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>, |
|
21 %\<threesuperior>, \<threequarters>, \<degree> |
|
22 |
|
23 %\usepackage[only,bigsqcap]{stmaryrd} |
|
24 %for \<Sqinter> |
|
25 |
|
26 %\usepackage{eufrak} |
|
27 %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb) |
|
28 |
|
29 %\usepackage{textcomp} |
|
30 %for \<cent>, \<currency> |
|
31 |
|
32 % this should be the last package used |
|
33 \usepackage{pdfsetup} |
10 \usepackage{pdfsetup} |
34 |
|
35 % urls in roman style, theory text in math-similar italics |
|
36 \urlstyle{rm} |
11 \urlstyle{rm} |
37 \isabellestyle{it} |
12 \isabellestyle{it} |
|
13 |
|
14 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
|
15 \renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}} |
|
16 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
|
17 \renewcommand{\isasymequiv}{$\dn$} |
|
18 \renewcommand{\isasymiota}{} |
|
19 \renewcommand{\isasymemptyset}{$\varnothing$} |
|
20 |
38 |
21 |
39 % for uniform font size |
22 % for uniform font size |
40 %\renewcommand{\isastyle}{\isastyleminor} |
23 %\renewcommand{\isastyle}{\isastyleminor} |
41 |
24 |
42 %----------------- theorem definitions ---------- |
25 %----------------- theorem definitions ---------- |
62 of programming language calculi. In this paper we present an extension |
45 of programming language calculi. In this paper we present an extension |
63 of Nominal Isabelle with general binding constructs. Such constructs |
46 of Nominal Isabelle with general binding constructs. Such constructs |
64 are important in formalisation ... |
47 are important in formalisation ... |
65 \end{abstract} |
48 \end{abstract} |
66 |
49 |
|
50 %\begin{keywords} |
|
51 %Language formalisations, Isabelle/HOL, POPLmark |
|
52 %\end{keywords} |
|
53 |
|
54 |
67 % generated text of all theories |
55 % generated text of all theories |
68 \input{session} |
56 \input{session} |
69 |
57 |
70 %\bibliographystyle{plain} |
58 \bibliographystyle{plain} |
71 % optional bibliography |
59 \bibliography{root} |
72 %\bibliographystyle{abbrv} |
|
73 %\bibliography{root} |
|
74 |
60 |
75 \end{document} |
61 \end{document} |
76 |
62 |
77 %%% Local Variables: |
63 %%% Local Variables: |
78 %%% mode: latex |
64 %%% mode: latex |