coursework/cw04.tex
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Sun, 21 Sep 2014 17:40:04 +0100
changeset 253 75c469893514
child 260 65d1ea0e989f
permissions -rw-r--r--
added coursework

\documentclass{article}
\usepackage{../style}
\usepackage{../langs}

\begin{document}

\section*{Coursework Alternative}

\noindent
This coursework is worth 25\% and is due on 12 December at 16:00. You are 
asked to prove the correctness of a regular expression matcher with the 
Isabelle theorem prover. This theorem prover is available from 

\begin{center}
\url{http://isabelle.in.tum.de}
\end{center}

\noindent
There is a shorte user guide for Isabelle called 
``Programming and Proving in Isabelle/HOL'' at

\begin{center}
\url{http://isabelle.in.tum.de/documentation.html}
\end{center}

\noindent
and also a longer (free) book at

\begin{center}
\url{http://www.concrete-semantics.org}
\end{center}

\noindent
If you need more help or you are stuck somewhere, please feel free
to contact me (christian.urban@kcl.ac.uk). I am a main developer of
Isabelle and have used it for approximately the last 14 years.


\subsection*{Problem}

\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: