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