Check-in [e4688d49fd]

Not logged in

Many hyperlinks are disabled.

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