Commit 84bb9b46 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

changed soundness

parent 55aa2e99
......@@ -853,7 +853,7 @@ for variables.
The algorithmic system above is sound with respect to the deductive one of Section~\ref{sec:static}
\begin{theorem}[Soundness]
For every $\Gamma$, $e$, $t$, $n_o$, if $\Gamma\vdashA e: t$, then $\Gamma \vdash e:t$.
For every $\Gamma$, $e$, $t$, $n_o$, if $\Gamma\vdashA e: \ts$, then $\Gamma \vdash e:t$ for every $t\in\ts$.
\end{theorem}
We were not able to prove full completeness, just a partial form of it. As
anticipated, the problems are twofold: $(i)$ the recursive nature of
......
......@@ -158,13 +158,13 @@ Whenever a function parameter is the argument of an
overloaded function, we record as possible types for this parameter
all the possible domains of the arrows that type the overloaded
function, restricted by the static type of the parameter. In Code~9,
since, \texttt{or\_} has type\\
since, \texttt{or\_} has type\\[.7mm]
\centerline{$(\True\to\Any\to\True)\land(\Any\to\True\to\True)\land
(\lnot\True\to\lnot\True\to\False)$}
We consider \True, \Any and $\lnot\True$ as candidate types for
(\lnot\True\to\lnot\True\to\False)$}\\[.7mm]
We consider \True, \Any, and $\lnot\True$ as candidate types for
\texttt{x} which, in turn allows us to deduce a precise type given in the table. Finally, thanks to this rule it is no longer necessary to use a type case to force refinement. As a consequence we can define the functions \texttt{and\_} and \texttt{xor\_} more naturally as:
\begin{alltt}\color{darkblue}\morecompact
let and_ = fun (x : Any) -> fun (y : Any) -> not_ (or_ (not_ x) (not_ y))
let xor_ = fun (x : Any) -> fun (y : Any) -> and_ (or_ x y) (not_ (and_ x y))
let and_ = fun (x : Any) -> fun (y : Any) -> not_ (or_ (not_ x) (not_ y))
let xor_ = fun (x : Any) -> fun (y : Any) -> and_ (or_ x y) (not_ (and_ x y))
\end{alltt}
for which the very same types as in Table~\ref{tab:implem} are deduced.
......@@ -44,16 +44,16 @@ for recursive types. Further, as far as we know, a code analysis such as the
one performed by Code 8 for extensible records is not handled by the
current state of the art.
\citet{Kent16} introduced the $\lambda_{RTR}$ core calculus, an
\citet{Kent16} introduce the $\lambda_{RTR}$ core calculus, an
extension of $\lambda_{TR}$ where the logical formulæ embedded in
types are not limited to built-in type predicates, but accepts
types are not limited to built-in type predicates, but accept
predicates of arbitrary theories. This allows them to provide some
form of dependent typing (and in particular they provide an
implementation supporting bitvector and linear arithmetic theories).
The static invariants that can be enforced by such logic goes well
beyond what can be proven with a static ``non depdendent'' type
While static invariants that can be enforced by such logic go well
beyond what can be proven by a static ``non dependent'' type
system, it does so at the cost of having the programmer write logical
annotations (to help the external provers). While this works provide
richer logical statements than \cite{THF10}, it still remains
annotations (to help the external provers). While this work provides
richer logical statements than those by~\citet{THF10}, it still remains
restricted to refining the types of variables, and not of arbitrary
constructs such as pairs, records or recursive types.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment