equal
deleted
inserted
replaced
1 %\documentclass{svjour3} |
1 \documentclass{sig-alternate} |
2 \documentclass{llncs} |
2 \pdfpagewidth=8.5truein |
|
3 \pdfpageheight=11truein |
3 \usepackage{times} |
4 \usepackage{times} |
4 \usepackage{isabelle} |
5 \usepackage{isabelle} |
5 \usepackage{isabellesym} |
6 \usepackage{isabellesym} |
6 \usepackage{amsmath} |
7 \usepackage{amsmath} |
7 \usepackage{amssymb} |
8 \usepackage{amssymb} |
9 \usepackage{tikz} |
10 \usepackage{tikz} |
10 \usepackage{pgf} |
11 \usepackage{pgf} |
11 \usepackage{verbdef} |
12 \usepackage{verbdef} |
12 \usepackage{longtable} |
13 \usepackage{longtable} |
13 \usepackage{mathpartir} |
14 \usepackage{mathpartir} |
|
15 \newtheorem{definition}{Definition} |
|
16 \newtheorem{proposition}{Proposition} |
|
17 \newtheorem{lemma}{Lemma} |
14 |
18 |
15 \urlstyle{rm} |
19 \urlstyle{rm} |
16 \isabellestyle{it} |
20 \isabellestyle{it} |
17 \renewcommand{\isastyle}{\isastyleminor} |
21 \renewcommand{\isastyleminor}{\it}% |
|
22 \renewcommand{\isastyle}{\normalsize\rm}% |
18 |
23 |
19 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
24 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
20 \verbdef\singlearr|--->| |
25 \verbdef\singlearr|--->| |
21 \verbdef\doublearr|===>| |
26 \verbdef\doublearr|===>| |
22 \verbdef\tripple|###| |
27 \verbdef\tripple|###| |
32 |
37 |
33 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}} |
38 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}} |
34 |
39 |
35 \begin{document} |
40 \begin{document} |
36 |
41 |
|
42 \conferenceinfo{SAC'11}{March 21-25, 2011, TaiChung, Taiwan.} |
|
43 \CopyrightYear{2011} |
|
44 \crdata{978-1-4503-0113-8/11/03} |
|
45 |
37 \title{Quotients Revisited for Isabelle/HOL} |
46 \title{Quotients Revisited for Isabelle/HOL} |
38 \author{Cezary Kaliszyk$^*$ and Christian Urban$^*$} |
47 \numberofauthors{2} |
39 \institute{$^*$ Technical University of Munich, Germany} |
48 \author{ |
|
49 \alignauthor |
|
50 Cezary Kaliszyk\\ |
|
51 \affaddr{University of Tsukuba, Japan}\\ |
|
52 \email{kaliszyk@score.cs.tsukuba.ac.jp} |
|
53 \alignauthor |
|
54 Christian Urban\\ |
|
55 \affaddr{Technical University of Munich, Germany}\\ |
|
56 \email{urbanc@in.tum.de} |
|
57 } |
|
58 |
40 \maketitle |
59 \maketitle |
41 |
60 |
42 \begin{abstract} |
61 \begin{abstract} |
43 Higher-Order Logic (HOL) is based on a small logic kernel, whose only |
62 Higher-Order Logic (HOL) is based on a small logic kernel, whose only |
44 mechanism for extension is the introduction of safe definitions and of |
63 mechanism for extension is the introduction of safe definitions and of |
52 The importance for programming language research is that many properties of |
71 The importance for programming language research is that many properties of |
53 programming language calculi are easier to verify over $\alpha$-equated, or |
72 programming language calculi are easier to verify over $\alpha$-equated, or |
54 $\alpha$-quotient, terms, than over raw terms. |
73 $\alpha$-quotient, terms, than over raw terms. |
55 \end{abstract} |
74 \end{abstract} |
56 |
75 |
|
76 \category{D.??}{TODO}{TODO} |
|
77 |
|
78 \keywords{quotients, isabelle, higher order logic} |
|
79 |
57 % generated text of all theories |
80 % generated text of all theories |
58 \input{session} |
81 \input{session} |
59 |
82 |
60 % optional bibliography |
83 % optional bibliography |
61 \bibliographystyle{abbrv} |
84 \bibliographystyle{abbrv} |