Check-in [e4688d49fd]

Not logged in

Overview
Comment: Fixed a missing section reference. Tarball | ZIP archive | SQL archive family | ancestors | descendants | both | trunk files | file ages | folders e4688d49fd2bd3ddc1b74744fffa681d5fef0744 andy 2015-04-26 16:27:10
Context
 2015-04-26 21:15 Full presentation (still draft). check-in: dab782646e user: andy tags: trunk 16:27 Fixed a missing section reference. check-in: e4688d49fd user: andy tags: trunk 16:26 Fixed a typo in the poster. check-in: b0f1fc67b4 user: andy tags: trunk
Changes

Changes to report/arend-report.pdf.

cannot compute difference between binary files

Changes to report/arend-report.tex.

 1918 1919 1920 1921 1922 1923 1924 1925 1926 1927 1928 1929 1930 1931  being a flaw in our system, this surprising result reflects the fact that one computational interpretation of $\bot$ is that of a non-terminating computation. In fact, this result is simply the computational analogue of the well-known \emph{ex falso quodlibet} principle of classical logic. \clearpage \section{Future work} There are many areas in which Arend could be enhanced and extended. We examine ten possibilities here, including one, equational reasoning, in some depth. \begin{itemize} \item Arend's specification logic is simple enough that formalization of   >  1918 1919 1920 1921 1922 1923 1924 1925 1926 1927 1928 1929 1930 1931 1932  being a flaw in our system, this surprising result reflects the fact that one computational interpretation of $\bot$ is that of a non-terminating computation. In fact, this result is simply the computational analogue of the well-known \emph{ex falso quodlibet} principle of classical logic. \clearpage \section{Future work} \label{sec:future-work} There are many areas in which Arend could be enhanced and extended. We examine ten possibilities here, including one, equational reasoning, in some depth. \begin{itemize} \item Arend's specification logic is simple enough that formalization of