|
1 |
|
2 \documentclass[a4wide]{article} |
|
3 \usepackage{isabelle,isabellesym} |
|
4 |
|
5 % further packages required for unusual symbols (see also isabellesym.sty) |
|
6 %\usepackage{latexsym} |
|
7 %\usepackage{amssymb} |
|
8 %\usepackage[english]{babel} |
|
9 %\usepackage[latin1]{inputenc} |
|
10 %\usepackage[only,bigsqcap]{stmaryrd} |
|
11 %\usepackage{wasysym} |
|
12 %\usepackage{eufrak} |
|
13 |
|
14 % this should be the last package used |
|
15 \usepackage{pdfsetup} |
|
16 |
|
17 % proper setup for best-style documents |
|
18 \urlstyle{rm} |
|
19 %\isabellestyle{it} |
|
20 \renewcommand{\isachardoublequote}{} |
|
21 |
|
22 % pretty printing for the Com language |
|
23 %\newcommand{\CMD}[1]{\isatext{\bf\sffamily#1}} |
|
24 \newcommand{\CMD}[1]{\isatext{\rm\sffamily#1}} |
|
25 \newcommand{\isasymSKIP}{\CMD{skip}} |
|
26 \newcommand{\isasymIF}{\CMD{if}} |
|
27 \newcommand{\isasymTHEN}{\CMD{then}} |
|
28 \newcommand{\isasymELSE}{\CMD{else}} |
|
29 \newcommand{\isasymWHILE}{\CMD{while}} |
|
30 \newcommand{\isasymDO}{\CMD{do}} |
|
31 |
|
32 \addtolength{\hoffset}{-1cm} |
|
33 \addtolength{\textwidth}{2cm} |
|
34 |
|
35 \begin{document} |
|
36 |
|
37 \title{IMP--A {\tt WHILE}-language and its Semantics} |
|
38 \author{Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow, Gerwin Klein} |
|
39 \maketitle |
|
40 |
|
41 \parindent 0pt\parskip 0.5ex |
|
42 |
|
43 \begin{abstract}\noindent |
|
44 The denotational, operational, and axiomatic semantics, a verification |
|
45 condition generator, and all the necessary soundness, completeness and |
|
46 equivalence proofs. Essentially a formalization of the first 100 pages |
|
47 of \cite{Winskel}. |
|
48 |
|
49 An eminently readable description of this theory is found in \cite{Nipkow}. |
|
50 |
|
51 A denotational semantics for IMP based on HOLCF is found in {\tt HOLCF/IMP}. |
|
52 \end{abstract} |
|
53 |
|
54 \tableofcontents |
|
55 |
|
56 \parindent 0pt\parskip 0.5ex |
|
57 |
|
58 % include generated text of all theories |
|
59 \input{session} |
|
60 |
|
61 \bibliographystyle{plain} |
|
62 \bibliography{root} |
|
63 |
|
64 \end{document} |