diff --git a/paper-new/discussion.tex b/paper-new/discussion.tex new file mode 100644 index 0000000000000000000000000000000000000000..3e392feb902d211b632c3d482c50bcee65790365 --- /dev/null +++ b/paper-new/discussion.tex @@ -0,0 +1,26 @@ +\section{Discussion} + +\subsection{Related Work} +% Discuss Joey Eremondi's thesis on gradual dependent types + +\subsection{Mechanization} +% Discuss Guarded Cubical Agda and mechanization efforts + +\subsection{Benefits and Drawbacks of the Synthetic Approach} + +\subsection{Synthetic Ordering} + +While the use of synthetic guarded domain theory allows us to very +conveniently work with non-well-founded recursive constructions while +abstracting away the precise details of step-indexing, we do work with +the error ordering in a mostly analytic fashion in that gradual types +are interpreted as sets equipped with an ordering relation, and all +terms must be proven to be monotone. +% +It is possible that a combination of synthetic guarded domain theory +with \emph{directed} type theory would allow for an a synthetic +treatment of the error ordering as well. + +\subsection{Future Work} + +% Cite GrEff paper \ No newline at end of file diff --git a/paper-new/paper.tex b/paper-new/paper.tex index f499375e33bacd2a2b3ae8181899ad5ffc078f6f..2083da00ab5eb4102ada6232b8bf4561845bda84 100644 --- a/paper-new/paper.tex +++ b/paper-new/paper.tex @@ -144,6 +144,8 @@ %\input{denotational-model} \input{concrete-model} +\input{discussion} + % \section{Discussion}\label{sec:discussion} % \subsection{Synthetic Ordering}