Check-in [1275718981]

Not logged in

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

Overview
Comment:Presentation work.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:1275718981cbad26ddef615b78ac8c42edc973c8
User & Date: 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
Hide Diffs Side-by-Side Diffs Ignore Whitespace Patch

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