Check-in [1275718981]

Not logged in

Overview
Comment: Presentation work. Tarball | ZIP archive | SQL archive family | ancestors | descendants | both | trunk files | file ages | folders 1275718981cbad26ddef615b78ac8c42edc973c8 andy 2015-04-22 20:50:44
Context
 2015-04-23 16:08 Finished poster. check-in: 8547fc1005 user: andy tags: trunk 2015-04-22 20:50 Presentation work. check-in: 1275718981 user: andy tags: trunk 20:50 Added jsonterm module, eventually to replace term_to_json (which is terrible). check-in: 0784891462 user: andy tags: trunk
Changes

Changes to presentation/arend-presentation.pdf.

cannot compute difference between binary files

Changes to presentation/arend-presentation.tex.

 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166  \end{frame} \begin{frame}\frametitle{Curry-Howard isomorphism, cont.} Some examples: \begin{itemize} \item If $p : P$ and $q : Q$ then the pair $(p,q) : P \land Q$. \item If $p : P$ and $q : Q$ then either $\mathsf{left}(p) : P \lor Q$ or $\mathsf{right}(q) : P \lor Q$. \item The most interesting: $P -> Q$ means $P$ implies $Q$''. \pause But it is also the type of \alert{functions} from $P$ to $Q$. A proof of $P -> Q$ is a \emph{program} that converts a proof (value) of $P$ into a proof (value) of $Q$! \end{itemize} (End of aside.)   | > > > > > | > |  150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172  \end{frame} \begin{frame}\frametitle{Curry-Howard isomorphism, cont.} Some examples: \begin{itemize} \item If $p : P$ and $q : Q$ then the pair $(p,q) : P \land Q$. \item If $p : P$ and $q : Q$ then either $\mathsf{left}(p) : P \lor Q$ or $\mathsf{right}(q) : P \lor Q$ \item More interesting: $P -> Q$ means $P$ implies $Q$''. \pause \\ But it is also the type of \alert{functions} from $P$ to $Q$. A proof of $P -> Q$ is a \emph{program} that converts a proof (value) of $P$ into a proof (value) of $Q$! \end{itemize} (End of aside.)