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 Unified Diffs Ignore Whitespace Patch

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.)