X-Git-Url: https://git.enpas.org/?a=blobdiff_plain;f=presentation.tex;fp=presentation.tex;h=a2cf6aba85c816091641715567119ec7903063ac;hb=6731f090d5edb85f628501e5dcc513e542fce325;hp=a1b2419ca7bc50da5bb4739d1f0d54e704a1d8a5;hpb=ec1119dffc5801526058a816d498b58e3c8f9e7f;p=bitonic-mengthesis.git

diff --git a/presentation.tex b/presentation.tex
index a1b2419..a2cf6ab 100644
--- 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}.
+
+  We have figured out theory of \mykant, and have a near-complete
+  implementation.
 \end{frame}
 
 \begin{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:
   \[