CA ready to submit (without appendix)

.vscode/ltex.dictionary.en-US.txt

@@ -0,0 +1,5 @@
+Coq
+PCUIC
+TemplateCoq
+intuitionistic
+Intuitionistic

chapters/coq-metacoq/coq.tex

@@ -6,28 +6,29 @@ \chapter{The Coq Proof Assistant}
 co-inductive types into the Calculus of Constructions.
 
 \section{An example of a Coq program} This is a simple example featuring the
-definition of a type ``nat'', a definition of a term of type ``nat'', namely
+definition of a type ``nat'', a definition of a constant of type ``nat'', namely
 ``zero'', and a function ``plus''  which takes two ``nat''s and returns its sum.
 
+Finally, thanks to Curry-Howard Correspondence, a proposition is a type; and
+here a named proposition is postulated. A simple proof is also given, which
+constructs a term inhabiting that type, hence proving the correctness of this
+proposition.
+
 \begin{listing}[!ht]
 \inputminted{coq}{code/example.v}
 \caption{A simple Coq program.}
 \end{listing}
 
-Finally, as explained before, a proposition is a type; and here a named
-proposition is postulated. A simple proof is also given, which constructs a term
-inhabiting that type, hence proving the correctness of this proposition.
-
 \section{Coq Modules}
 Modules in Coq not only allows the reuse of code, it also provides parametrized
 theories or data structures in the form of functors (or parametrized modules).
 
 In the following example, we show how one can package definitions into named modules
 for reuse; we also show how we can create parametrized generic data structures.
+In the final line, a new Magma was created based on the Magma ``Nat''
+by the functor ``DoubleMagma''.
 
 \begin{listing}[!ht]
 \inputminted{coq}{code/module_example.v}
 \caption{An example of Modules.}
 \end{listing}
-
-In the final line, a new Magma was created by the functor ``DoubleMagma''.

chapters/coq-metacoq/coqmod.tex

@@ -1,15 +1,15 @@
+\section{Towards Specifying the Meaning of Coq Modules}
 
-\section{A specification of Coq Modules}
 % \subsection{A specification of Coq Modules}
-Module systems are  a feature of the ML family of languages; it allows
+Module systems are a feature of the ML family of languages; it allows
 for massive abstraction and the reuse of code. In particular, Coq 
 also has a module system that is influenced by ML modules, first 
 implemented by Jacek Chrząszcz in 2003, then modified by Elie Soubrian
 in 2010.
 
 There are a few keywords when it comes to Coq Modules:
 \begin{itemize}
-\item A \textbf{structure} is a anynomous collection of definitions, and is the 
+\item A \textbf{structure} is an anynomous collection of definitions, and is the 
     underlying construct of modules. They contain \textbf{structure elements},
     which can be a
     \begin{itemize}
@@ -72,10 +72,10 @@ \subsection{Modules as second-class objects}
 are therefore opaque second-class objects which is only useful when a module is
 generated.
 
-In this chapter, we formalize the syntax and semantics of the current
-implementation of Coq and implement in the level of TemplateCoq. Section
-\ref{sec:plainmodules} describes the implementation of plain modules
-without functors.
+In this chapter, we formalize the semantics of the current implementation of Coq
+Modules and formalize them at the level of TemplateCoq. Section
+\ref{sec:semantics-of-modules} describes the semantics behind plain modules and
+aliased modules, without functors.
 
 
 % \section{Related Works}
@@ -94,7 +94,7 @@ \subsection{Related Works} Jacek Chrzaszcz's article in TPHOLs 2003
 Other slightly useful references include papers that explain modules in the ML
 family of languages, specifically OCaml and to a certain extent, Standard ML.
 On this note, Derek Dreyer wrote his PhD thesis \sidecite{dreyerphd} on
-understanding and extending ML modules, and subsequently a on implementing ML
+understanding and extending ML modules, and subsequently on implementing ML
 modules in its most desirable form, applicative and first-order as a subset of a
 small type system, $F_\omega$\sidecite{f-ing}. Other notable implementations
 include that of CakeML \sidecite{cakeml}, a verified ML language and Standard ML
@@ -121,23 +121,71 @@ \subsection{Related Works} Jacek Chrzaszcz's article in TPHOLs 2003
 % \item CakeML has modules, but not functors. YK Tan (2015).
 % \end{enumerate}
 
-\section{Semantic of Modules}
+\section{Semantics of Modules}
+\label{sec:semantics-of-modules}
+From now onwards, we consider only non-parametrized modules.
+
+There are two operations involving modules: how to define a module and how to
+use a module. We will specify the behaviour, implementation and proof
+obligations below.
+
+Modules are containers for definitions that allow reuse. Definitions in Coq are
+stored in a Global Environment. We first look at the structure of Global Environment:
+
+\subsection{Global Environment}
+The Global Environment in Coq can be understood as a table or a map. There are
+three columns in the map: first is a canonical kername, second a pathname, and
+finally, the definition object. Canonical kernames can be though of as unique
+labels, and for the ease of understanding, as natural numbers 1, 2, 3 etc.
+The pathname is a name which the user gives to the definition; it is of the form
+of a dot-separated string, such as $M.N.a$. Finally, the definition object can
+be:
+\begin{itemize}
+
+\item A \textbf{constant definition} to a Coq term, such as a lambda term,
+application term, etc..
+
+\item An \textbf{inductive definition} of a type.
+
+\item A \textbf{module definition}. We consider a module to be inductively
+defined as a list of constant, inductive, module or module signature
+definitions. Alternatively, it can also be an alias to a previously defined
+module (which may be an alias).
+
+\item A \textbf{module signature definition} has the same structure as a module
+definition, but instead of concrete definitions, it only specifies a name and a
+type for each entry. It can be also an alias to a previously defined module
+signature (which may be an alias).
+
+\end{itemize}
+The terms ``module type'' and ``module signature'' are used interchangeably.
+
 \subsection{Plain Modules}
 \label{sec:plainmodules}
 
-Plain modules are just saving declarations and definitions in a structure, in the
-global context. Its contents are not modified during conversion/reduction.
+\subsubsection{Behaviour and Implementation}
 
-In Coq, modules are second-class objects; in other words, a module is not a
-term.  Its definition is stored and referred to by a canonical kername. We say
-the implementation of such a module is correct if the metatheory of the original
-system are unchanged and remains correct; that is the proofs go through when
-terms can be defined within modules. Since the MetaCoq project has proven
+Modules can be thought of as a named global environment where the definitions
+within it are namespaced by the module name. Therefore, its contents are not
+modified during conversion/reduction.  In Coq, modules are second-class objects;
+in other words, a module is not a term.  Its definition is stored and referred
+to by a pathname and a kername.
+
+Therefore, implementation wise, one need to ensure the correctness of "referring
+to definition"; that is, when a definition within a module is referred to by its
+pathname $M.N.a$, it will be fetched correctly from the table.
+
+\subsubsection{Proof obligation}
+
+We say the implementation of such a module is correct if the meta-theory of the
+original system are unchanged and remains correct; that is the proofs go through
+when terms can be defined within modules. Since the MetaCoq project has proven
 various nice properties about conversion in Coq, our project on plain modules is
 two-fold:
+
 \begin{enumerate}
 \item Ensure the correctness of the static semantics of Coq Modules
-(well-typedness).
+(well-typedness) during its definition.
 \item Define the behaviour of access of definitions within Modules.
 \end{enumerate}
 
@@ -147,7 +195,7 @@ \subsection{Plain Modules}
 This follows as our definition of Modules on the TemplateCoq level, is
 eventually elaborated down into the PCUIC calculus the idea of modules and
 aliasing do not exist anymore, they are flattened into the corresponding global
-environment.
+environment. The details of (2) are described in Section \ref{sec:using-modules}.
 
 Concretely, if a module as below is defined while the Global Environment, which
 stores definitions is denoted as $\Sigma$:
@@ -156,24 +204,53 @@ \subsection{Plain Modules}
     Definition a: nat := 0.
 End M.
 \end{minted}
-Then the environment will have an new declaration added:
+Then the environment must have a new declaration added:
 \[\Sigma := \Sigma :: \text{ModuleDeclaration}(M,
 [\text{ConstantDeclaration}(M.a, nat, 0)])\]
 
-So when $M.a$ is called, it refers to the definition in the 
+So when $M.a$ is called, it must refer to the definition in the Global
+Environment correctly.
 
 \subsection{Aliased Modules}
 Aliased modules are just a renaming of existing modules, which can be seen as
 syntactic sugar for modules. Therefore, the correctness depends only on
-implementing this internal referencing correctly. Suppose we have
+implementing this internal referencing correctly.
+
+\subsubsection{Behaviour and Implementation}
+Suppose we have
 
 \begin{minted}{coq}
 Module N := M.
 \end{minted}
 
-Aliasing $N$ to $M$, then any access path $N.X$ should be resolved similarly to
+Aliasing $N$ to $M$ and $M$ is a previously defined module (or an alias),
+then any access path $N.X$ should be resolved similarly to
 $M.X$ (note that since $M$ is possibly an alias as well, we do not require $N.X$
-to resolve \emph{to} $M.X$). In the OCaml implementation, this is implemented 
-by an internal kernel name, conceptually similar to a lookup table; formally,
-the kernel name is a pair of a \emph{name} and a \emph{label}, with label being
-the internal reference used by both $N$ and $M$.
+to resolve \emph{to} $M.X$). In the OCaml implementation, all definitions in $M$
+can now be referred to by the pathnames $N.X$ in addition to $M.X$, while still
+having the same kername.
+
+\subsubsection{Proof Obligations}
+\begin{enumerate}
+\item Well-definedness: aliasing can only occur for well-defined modules. There
+    cannot be self-alias and forward aliasing (aliasing something not yet defined).
+\item The resolution of aliased modules is done at definition. If $N$ is aliased
+    to $M$, then $N$ will immediately inherit the same kername as $M$. We will
+    show this resolution is decidable and results in correct aliasing.
+\end{enumerate}
+
+\subsection{Using Modules}
+\label{sec:using-modules}
+As mentioned, the only way modules are used is during reduction or conversion
+of a Coq term. In Coq, reduction and conversion are made up of smaller reduction
+rules, such as $\beta, \delta,\zeta,\eta,\iota$ reductions. In particular, 
+Modules are related only to $\delta$ reductions, which "replaces a defined
+variable with its definition" 
+\sidenote{\href{https://coq.inria.fr/refman/language/core/conversion.html} {Coq:
+Conversion}}.
+
+The correctness of $\delta$-reduction and conversion is a meta-theoretic
+property, which is already shown to be correct and have properties such as 
+normalization, confluence etc. in PCUIC \sidecite{coqcoqcorrect}. I will
+contribute by expanding the definition of delta-conversion and expand the
+existing proofs in the MetaCoq project that such properties continue to hold.

chapters/coq-metacoq/metacoq.tex

@@ -3,41 +3,44 @@ \chapter{Introduction to the MetaCoq Project}
 
 \section{The MetaCoq Project}
 % \subsection{The MetaCoq Project}
-MetaCoq is a project to formalize the core calculus, PCUIC, in Coq, and become
-a platform to write tools that can manipulate Coq terms. The effort was complete
-for a large part of the core language of Coq, with a few missing pieces:
+MetaCoq is a project to formalize the core calculus, PCUIC, in Coq, and become a
+platform to write tools that can manipulate Coq terms
+\sidecite{sozeau2020metacoq}. The effort was complete for a large part of the
+core language of Coq \sidecite{coqcoqcorrect}, with a few missing pieces :
 
 \begin{itemize}
-    \item Eta 
+    \item Eta-conversion
     \item Template Polymorphism
     \item SProps
     \item Modules
 \end{itemize}
 
 I will be tackling the last.
 
-\section{Structure of the MetaCoq Project} The MetaCoq project is an
-ambitious project aiming to provide a verified implementation of Coq, and for
-its size, it is reasonably split into a few main components. From the layer
-closest to the Coq language to the machine code, we have: TemplateCoq (Section
+\section{Structure of the MetaCoq Project} The MetaCoq project is an ambitious
+project aiming to provide a verified implementation of Coq, and for its size, it
+is reasonably split into a few main components. From the layer closest to the
+Coq language to layer closest to machine code, we have: TemplateCoq (Section
 \ref{sec:mc-template}), PCUIC (Section \ref{sec:mc-pcuic}), followed by Safe
 Checker, Erasure and beyond(Section \ref{sec:mc-beyond}).
 
 Let us remind ourselves of the task of MetaCoq: we would like to see that the
-OCaml representation of Coq is indeed correct and preserves the desired properties 
-of the underlying theory. Since Coq has added many bells and whistles for its 
-users, the terms of Coq definitely is much more complex than its underlying,
-platonic type theoretical form. Therfore, MetaCoq has several stages for a term
-to go through, stripping down to the bare minimum through the following few 
-stages.
+OCaml representation of Coq is indeed correct and preserves the desired
+properties of the underlying theory. Since Coq has added many ``bells and
+whistles'' for its users, the terms of Coq definitely is much more complex than
+its underlying, Platonic type theoretical form. Therefore, MetaCoq has several
+stages for a Coq term to go through, stripping down to the bare minimum through
+the following few stages.
 
 \subsection{TemplateCoq}
 \label{sec:mc-template}
 
 TemplateCoq is a quoting library for Coq: a Coq program that takes a Coq term,
 and constructs an inductive data type that correspond to its kernel
 representation in the OCaml implementation. This is the first layer of the
-stripping of a Coq term, where the structures are preserved properly.
+stripping of a Coq term, where the structures associated with a term, such as
+the Global Environment under which it is defined, are preserved properly as in
+the kernel.
 
 % TODO: Insert example
 
@@ -50,29 +53,32 @@ \subsection{PCUIC}
 
 PCUIC is the Polymorphic Cumulative Calculus of Inductive Constructions. It is a
 "cleaned up version of the term language of Coq and its associated type system,
-shown equivalent to the one in Coq." (From MetqCoq website). In other words, it 
-is a type theory that is as powerful as Coq can express, having the good
-properties such as weakening, confluence, principality (that every term has a
-principal type) etc.
+shown equivalent to the one in Coq." \sidenote{from
+\url{https://metacoq.github.io}}.  In other words, it is a type theory that is
+as powerful as Coq can express, having the good properties such as weakening,
+confluence, principality (that every term has a principal type) etc.
+\sidecite{coqcoqcorrect}.
 
-A term generated in TemplateCoq can be converted into PCUIC term via a verified
-process. The theory of PCUIC is then proven to have all the nice properties in
-Coq.
+A term generated in TemplateCoq can be converted into a PCUIC term via a
+verified process. Since the theory of PCUIC is then proven to have all the
+``nice'' properties in Coq, by the equivalence, the verified translation of
+TemplateCoq terms into PCUIC terms propagates these properties to the language
+of Coq.
 
 
 \subsection{Safe Checker, Erasure and Beyond}
 \label{sec:mc-beyond}
 
 The core semantic operation of type theories are the reductions. The safechecker
 is a verified "reduction machine, conversion checker and type checker" for PCUIC
-terms. So far, we have the tools to start with a Coq term, first quoting into
-TemplateCoq, then converted into a PCUIC term, and eventually has its type
-checked in the Safe Checker via a fully verified process. As far as correctness
-is concerned, this has already formed a verified end-to-end process of Coq's 
-correctness.
+terms. At this point, we already have the tools to start with a Coq term, first
+quoting into TemplateCoq, then converted into a PCUIC term, and eventually has
+its type checked in the Safe Checker via a fully verified process. As far as
+correctness is concerned, this has already formed a verified end-to-end process
+of Coq's correctness.
 
 The MetaCoq has further provided a verified Type and Proof erasure process from
-PCUIC to untyped Lambda Calculus. The equivalence of this erased language is
-can be evaluated in \emph{C-light} semantics, the subset of C accepted by
-the CompCert verified compiler, which completes a maximally safe evaluation
-toolchain for the language of Coq \sidecite{coqcoqcorrect}.
+PCUIC to untyped Lambda Calculus. This erased language is can be evaluated in
+\emph{C-light} semantics, the subset of C accepted by the CompCert verified
+compiler, which completes a maximally safe evaluation toolchain for the language
+of Coq, all the way to machine code \sidecite{coqcoqcorrect}.