Final submission: links to repo tags

SwampertX · May 5, 2023 · 2236acd · 2236acd
1 parent 9453e3b
commit 2236acd
Show file tree

Hide file tree

Showing 7 changed files with 33 additions and 3 deletions.
diff --git a/final-report-new/01-introduction.tex b/final-report-new/01-introduction.tex
@@ -124,7 +124,10 @@ \section{Contributions}
 surfaced from the initial implementation. Finally, Chapter \ref{ch:machineries}
 will document the skill acquired in writing formal proofs in Coq during the
 implementation of the project. This report will end with possible future work in
-Chapter \ref{ch:future}.
+Chapter \ref{ch:future}. The first implementation and the draft for the second
+can be found on \url{https://github.com/SwampertX/metacoq/tree/fyp-first-impl}
+and \url{https://github.com/SwampertX/metacoq/releases/tag/fyp-second-impl}
+respectively.
 % while some technical details, such as concrete typing rules
 % % , and some type-theoretic results I studied as a joint
 % % thesis with the Mathematics Department

diff --git a/final-report-new/04-implementation.tex b/final-report-new/04-implementation.tex
@@ -4,6 +4,8 @@
 % mind includes inductive, but not necessarily mutual (or rather, might be
 % mutual with one branch)
 \chapter{Implementation of MetaCoq Modules}
+The code listings used in this chapter can be found on
+\url{https://github.com/SwampertX/metacoq/releases/tag/fyp-first-impl}.
 \label{ch:impl1}
 \newcommand{\tc}[3]{
   % \begin{listing}[H]

diff --git a/final-report-new/05-modular.tex b/final-report-new/05-modular.tex
@@ -77,7 +77,9 @@ \section{The Modular Environment}
 ambient, top-level module, thus just a special case of a module. Under this
 generalization, any well-formedness properties or well-typedness properties
 about environments should be subsumed under modules, thus giving us a good sense
-when defining the typing rules for modules.
+when defining the typing rules for modules. A draft implementation of the rest
+of the code listings can be found on
+\url{https://github.com/SwampertX/metacoq/releases/tag/fyp-second-impl}.
 
 \subsection{Definition of the Data Structure}
 Let us begin by defining modules, then specialize into global declarations.

diff --git a/final-report-new/main.pdf b/final-report-new/main.pdf
diff --git a/final-report-new/main.tex b/final-report-new/main.tex
@@ -51,4 +51,6 @@
 \include{06-machineries.tex}
 \include{07-future-work.tex}
 
+\printbibliography
+
 \end{document}
diff --git a/final-report-new/presentation/02-modules.tex b/final-report-new/presentation/02-modules.tex
@@ -2,6 +2,28 @@
 
 \subsection{The MetaCoq Project}
 
+\begin{frame}
+  \frametitle{The Coq Proof Assistant}
+
+  In its core, Coq is a strongly typed lambda calculus, basically calculus of
+  constructions + co-inductive types + universe polymorphism + cumulativity.
+  \pause
+
+  Core objects are terms. Operational semantics -- reduction.
+  \begin{align*}
+    (\lambda x.x)\ y \to_\beta y
+  \end{align*}
+  \pause
+
+  Denotational semantics -- conversion.
+  \begin{align*}
+    \lambda x.x\equiv_\alpha\lambda y.y
+  \end{align*}
+
+  Curry-Howard Correspondance -- Types are Theorems, Programs are Proofs.
+
+\end{frame}
+
 \begin{frame}
   \frametitle{The MetaCoq Project - History}
   A metaprogramming platform for Coq.
@@ -27,7 +49,6 @@ \subsection{The MetaCoq Project}
     \item Actual data structure of modules live in \textbf{TemplateCoq}.
     \item Verification of properties of modules live in \textbf{TemplateCoq}.
     \item Translation from \textbf{TemplateCoq} to \textbf{PCUIC}.
-    \item Difference? PCUIC is easier to prove (semantical) theorems.
   \end{itemize}
 \end{frame}
 

diff --git a/final-report-new/presentation/presentation.pdf b/final-report-new/presentation/presentation.pdf