doc-src/Codegen/codegen.tex
author haftmann
Fri Jan 22 13:38:28 2010 +0100 (2010-01-22)
changeset 34944 970e1466028d
parent 33926 dd017d9db05f
child 37613 355ec1b521e6
permissions -rw-r--r--
code literals: distinguish numeral classes by different entries
haftmann@20948
     1
haftmann@30227
     2
\documentclass[12pt,a4paper,fleqn]{article}
haftmann@20948
     3
\usepackage{latexsym,graphicx}
haftmann@20948
     4
\usepackage[refpage]{nomencl}
haftmann@30226
     5
\usepackage{../iman,../extra,../isar,../proof}
haftmann@30226
     6
\usepackage{../isabelle,../isabellesym}
haftmann@20948
     7
\usepackage{style}
haftmann@30226
     8
\usepackage{../pdfsetup}
haftmann@20948
     9
haftmann@20948
    10
\hyphenation{Isabelle}
haftmann@20948
    11
\hyphenation{Isar}
haftmann@20948
    12
\isadroptag{theory}
haftmann@28564
    13
haftmann@20948
    14
\title{\includegraphics[scale=0.5]{isabelle_isar}
haftmann@21222
    15
  \\[4ex] Code generation from Isabelle/HOL theories}
bulwahn@33926
    16
\author{\emph{Florian Haftmann with contributions from Lukas Bulwahn}}
haftmann@20948
    17
haftmann@20948
    18
\begin{document}
haftmann@20948
    19
haftmann@20948
    20
\maketitle
haftmann@20948
    21
haftmann@20948
    22
\begin{abstract}
haftmann@30227
    23
  \noindent This tutorial gives an introduction to a generic code generator framework in Isabelle
haftmann@28213
    24
  for generating executable code in functional programming languages from logical
haftmann@28213
    25
  specifications in Isabelle/HOL.
haftmann@20948
    26
\end{abstract}
haftmann@20948
    27
haftmann@20948
    28
\thispagestyle{empty}\clearpage
haftmann@20948
    29
haftmann@20948
    30
\pagenumbering{roman}
haftmann@20948
    31
\clearfirst
haftmann@20948
    32
haftmann@28419
    33
\input{Thy/document/Introduction.tex}
haftmann@28419
    34
\input{Thy/document/Program.tex}
haftmann@31050
    35
\input{Thy/document/Adaptation.tex}
haftmann@28419
    36
\input{Thy/document/Further.tex}
haftmann@28419
    37
\input{Thy/document/ML.tex}
haftmann@20948
    38
haftmann@20948
    39
\begingroup
haftmann@20948
    40
\bibliographystyle{plain} \small\raggedright\frenchspacing
haftmann@30226
    41
\bibliography{../manual}
haftmann@20948
    42
\endgroup
haftmann@20948
    43
haftmann@20948
    44
\end{document}
haftmann@20948
    45
haftmann@20948
    46
haftmann@20948
    47
%%% Local Variables: 
haftmann@20948
    48
%%% mode: latex
haftmann@20948
    49
%%% TeX-master: t
haftmann@20948
    50
%%% End: