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