Check-in [e4688d49fd]

Not logged in

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Comment:Fixed a missing section reference.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
User & Date: andy 2015-04-26 16:27:10
Full presentation (still draft). check-in: dab782646e user: andy tags: trunk
Fixed a missing section reference. check-in: e4688d49fd user: andy tags: trunk
Fixed a typo in the poster. check-in: b0f1fc67b4 user: andy tags: trunk
Hide Diffs Side-by-Side Diffs Ignore Whitespace Patch

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