...

[bitonic-mengthesis.git] / presentation.tex

diff --git a/presentation.tex b/presentation.tex
index a1b2419ca7bc50da5bb4739d1f0d54e704a1d8a5..3637b14eb72cbe1f1e28d813e236515578667b5f 100644 (file)
--- a/presentation.tex
+++ b/presentation.tex
@@ -228,11 +228,14 @@
 \begin{frame}
   \frametitle{\mykant?}
 
-  \mykant\ is an \emph{interactive theorem prover}, implemented in
-  Haskell.
+  \mykant\ is an \emph{interactive theorem prover}/\emph{functional
+    programming language}, implemented in Haskell.
 
-  It is similar in scope to Agda or Coq, but with a more powerful notion
-  of \emph{equality}.
+  It is in the tradition of Agda and Epigram (and to a lesser extent
+  Coq), but with a more powerful notion of \emph{equality}.
+
+  We have figured out theory of \mykant, and have a near-complete
+  implementation.
 \end{frame}
 
 \begin{frame}
@@ -371,7 +374,7 @@
   Or
   \[ \myfun{head} \myappsp (3 \mycons \mynil) : \myunit \myarr \mynat \]
 
-  Yes: to typecheck, we reduce terms fully (to their \emph{normal} form)
+  Yes: to typecheck, we reduce terms fully (to their \emph{normal form})
   before comparing:
   \[
   \begin{array}{@{}r@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }l}
@@ -474,7 +477,7 @@ Without the $\myb{l}$ we cannot compute, so we are stuck with
   \[
   \begin{array}{@{}l@{\ }l}
     \mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{pc} \myappsp \mynil & \myred \myse{pn} \\
-    \mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{pc} \myappsp (\mytmm \mycons \mytmn) & \myred \myse{pc} \myappsp \mytmm \myappsp \mytmn \myappsp (\mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{ps} \myappsp \mytmt )
+    \mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{pc} \myappsp (\mytmm \mycons \mytmn) & \myred \myse{pc} \myappsp \mytmm \myappsp \mytmn \myappsp (\mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{ps} \myappsp \mytmn )
   \end{array}
   \]
 \end{frame}
@@ -532,7 +535,7 @@ Without the $\myb{l}$ we cannot compute, so we are stuck with
   \[
   \cancel{\mytyp : \mytyp}\ \ \ \text{\textbf{inconsistent}}
   \]
-  Much like na{\"i}ve set theory is (Girard's paradox).
+  Similar to Russel's paradox in na{\"i}ve set theory.
 
   Instead, we have a hierarchy:
   \[