Skip to content
Snippets Groups Projects
Commit 54da8ccd authored by Max New's avatar Max New
Browse files

discuss Siek-Chen

parent 9e71c25f
No related branches found
No related tags found
No related merge requests found
......@@ -15,8 +15,15 @@ However, they do not give a denotational semantics to term precision and it is u
how to prove the gradual guarantee in this setting.
The work includes a formalization of the syntactic model in Guarded Cubical Agda.
% Discuss Jeremy Siek's work on graduality in Agda
Siek and Chen \cite{siekchen2021} give a proof in Agda of graduality
for an operational semantics. While they do not use the Guarded
Cubical extension, they do use a guarded logic of propositions
shallowly embedded in Agda. Our denotational approach requires full
guarded type theory not just guarded logic. An advantage of the
denotational approach is that it easily validates equational
reasoning, not just graduality, and it is completely independent of
any particular syntax of gradual typing.
\subsection{Mechanization}
% Discuss Guarded Cubical Agda and mechanization efforts
......
......@@ -119,8 +119,8 @@ model}. A strict homomorphism of CBPV models from $(\mathcal
V,\mathcal E,\ldots)$ to $(\mathcal V', \mathcal E',\ldots)$ consists
of functors $G_v : \mathcal V \to \mathcal V'$ and $G_e : \mathcal E
\to \mathcal E'$ that strictly preserve all CBPV constructions, see
the appendix for a more detailed definition.
Some of that data can be visualized as follows:
the appendix for a more detailed definition. We call this a strict morphism in contrast to a \emph{lax} morphism, which only preserves CBPV constructions up to transformation.
Some of the data of a double CBPV model can be visualized as follows:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJcXHZzcSJdLFsyLDAsIlxcZXNxIl0sWzAsMiwiXFx2ZiJdLFsyLDIsIlxcZWYiXSxbMiwzLCJcXEZmIiwwLHsiY3VydmUiOi0yfV0sWzMsMiwiXFxVZiIsMCx7ImN1cnZlIjotMn1dLFswLDEsIlxcRnNxIiwwLHsiY3VydmUiOi0yfV0sWzEsMCwiXFxVc3EiLDAseyJjdXJ2ZSI6LTJ9XSxbMiwwLCJcXHJ2Il0sWzAsMiwiXFxzdiIsMCx7ImN1cnZlIjotMn1dLFswLDIsIlxcdHYiLDIseyJjdXJ2ZSI6Mn1dLFsxLDMsIlxcc2UiLDAseyJjdXJ2ZSI6LTJ9XSxbMSwzLCJcXHRlIiwyLHsiY3VydmUiOjJ9XSxbMywxLCJcXHJlIl0sWzQsNSwiXFxib3QiLDEseyJzaG9ydGVuIjp7InNvdXJjZSI6MjAsInRhcmdldCI6MjB9LCJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJub25lIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbNiw3LCJcXGJvdCIsMSx7InNob3J0ZW4iOnsic291cmNlIjoyMCwidGFyZ2V0IjoyMH0sInN0eWxlIjp7ImJvZHkiOnsibmFtZSI6Im5vbmUifSwiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dXQ==
\[\begin{tikzcd}[ampersand replacement=\&]
\vsq \&\& \esq \\
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment