Check-in [e4688d49fd]

Not logged in

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

Overview
Comment:Fixed a missing section reference.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:e4688d49fd2bd3ddc1b74744fffa681d5fef0744
User & Date: 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
Hide Diffs Unified Diffs Ignore Whitespace Patch

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