text:
\section{Introduction}
In computer science,
an exception is an abnormal event occurring during the execution
of a program. A mechanism for handling exceptions consists of
two parts: an exception is \emph{raised} when an abnormal event occurs,
and it can be \emph{handled} later, by switching the execution to
a specific subprogram.
Such a mechanism is very helpful, but it is difficult
for programmers to reason about it.
A difficulty for reasoning about programs involving exceptions
is that they are \emph{computational effects},
in the sense that their syntax does not look like their interpretation:%
typically,
a piece of program with arguments in $X$ that returns a value in $Y$
is interpreted as a function from $X+E$ to $Y+E$ where $E$ is
the set of exceptions.
On the one hand, reasoning with $f:X\to Y$ is close to the syntax,
but it is error-prone because it is not sound with respect to the semantics.
On the other hand, reasoning with $f:X+E\to Y+E$ is sound but
it loses most of the interest of the exception mechanism,
where the propagation of exceptions is implicit:
syntactically, $f:X\to Y$ may be followed by any $g:Y\to Z$,
since the mechanism of exceptions will take care of propagating
the exceptions raised by $f$, if any.
Another difficulty for reasoning about programs involving exceptions
is that the handling mechanism is encapsulated in a $\mathtt{try}\texttt{-}\mathtt{catch}$ block,
while the behaviour of this mechanism is easier to explain
in two parts (see for instance~\cite[Ch. 14]{java} for Java
or~\cite[\S 15]{cpp} for C++):
the $\catch$ part may recover from exceptions,
so that its interpretation may be any $f:X+E\to Y+E$,
but the $\mathtt{try}\texttt{-}\mathtt{catch}$ block must propagate exceptions,
so that its interpretation is determined by some $f:X\to Y+E$.

In \cite{DDER14-exc} we defined a logical system
for reasoning about states and exceptions and we used it for getting
certified proofs of properties of programs in computer algebra,
with an application to exact linear algebra.
This logical system is called the \emph{decorated logic}
for states and exceptions. Here we focus on exceptions.
The decorated logic for exceptions
deals with $f:X\to Y$, without any mention of~$E$,
however it is sound thanks to a classification of the terms and the equations.
Terms are classified, as in a programming language,
according to the way they may interact with exceptions: a term
either has no interaction with exceptions (it is ``pure''),
or it may raise exceptions and must propagate them,
or it is allowed to catch exceptions
(which may occur only inside the $\catch$ part of a $\mathtt{try}\texttt{-}\mathtt{catch}$ block).
The classification of equations follows a line that was introduced
in \cite{DD10}:
besides the usual ``strong'' equations, interpreted as equalities of functions,
in the decorated logic for exceptions there are also ``weak'' equations,
interpreted as equalities of functions on non-exceptional arguments.
This logic has been built so as to be sound,
but little was known about its completeness.
In this paper we prove a novel completeness result:
the decorated logic for exceptions is \emph{relatively Hilbert-Post complete},
which means that adding exceptions to a programming language can be done
in such a way that the completeness of the language is not made worse.
For this purpose, we first define and study the novel notion
of {\em relative} Hilbert-Post completeness, which seems to be
a relevant notion for the completeness of various computational
effects:
indeed, we prove that this notion is preserved when combining
effects.
Practically, this means that we have defined a decorated framework
where reasoning about programs with and without exceptions are
equivalent, in the following sense:
if there exists an unprovable equation not contradicting the given
decorated rules, then this equation is equivalent to a set of
unprovable equations of the pure sublogic not contradicting its rules.

Informally, in classical logic, a consistent theory is one that does not
contain a contradiction and a theory is complete if it is
consistent, and none of its proper extensions is consistent.
Now, the usual (``\emph{absolute}'') Hilbert-Post completeness,
also called Post completeness, is a syntactic notion of completeness
which does not use any notion of negation,
so that it is well-suited for equational logic.
In a given logic $L$, we call \emph{theory} a set of sentences
which is deductively closed: everything you can derive from it
(using the rules of $L$) is already in it.
Then, more formally, a theory is \emph{(Hilbert-Post) consistent} if it
does not contain  all sentences,
and it is \emph{(Hilbert-Post) complete} if it is consistent
and if any sentence which is added to it generates an inconsistent
theory~\cite[Def. 4]{Tarski30}.

All our completeness proofs have been verified with the Coq proof
assistant.
First, this shows that it is possible to formally prove that programs
involving exceptions comply to their specifications.
Second, this is of help for improving the confidence in the
results.
Indeed, for a human prover, proofs in a decorated logic require some care:
they look very much like familiar equational proofs,
but the application of a rule may be subject to restrictions
on the decoration of the premises of the rule.
The use of a proof assistant in order to
check that these unusual restrictions were never violated has thus
proven to be quite useful.
Then, many of the proofs we give in this paper require a structural
induction. There, the correspondence between our proofs and their Coq
counterpart was eased, as structural induction is also at the core of
the design of Coq.

A major difficulty for reasoning about programs involving exceptions,
and more generally computational effects,
is that their syntax does not look like their interpretation: typically,
a piece of program from $X$ to $Y$
is not interpreted as a function from $X$ to $Y$, because of the effects.
The best-known algebraic approach for dealing with this problem has been
initiated by Moggi:
an effect is associated to a monad $T$, in such a way that
the interpretation of a program from $X$ to $Y$ is a function
from $X$ to $T(Y)$~\cite{Moggi91}:
typically, for exceptions, $T(Y)=Y+E$.
Other algebraic approaches include effect systems~\cite{LucassenGifford88},
Lawvere theories~\cite{PlotkinPower02},
algebraic handlers~\cite{PP09},
comonads~\cite{UV08,POM14},
dynamic logic~\cite{MSG10}, among others.
Some completeness results have been obtained, for instance
for (global) states~\cite{Pretnar10} and
for local states~\cite{Staton10-fossacs}.
The aim of these approaches is to extend functional languages
with tools for programming and proving side-effecting programs;
implementations include Haskell \cite{BHM00}, Idris \cite{Idris},
Eff \cite{BauerP15},
while Ynot \cite{Ynot} is a Coq library for writing and verifying
imperative programs.

Differently, our aim is to build a logical system for proving
properties of some families of programs written in widely used
non-functional languages like Java or C++\footnote{For instance, a
  denotational semantics of our framework for exceptions, which relies
  on the common semantics of exceptions in these languages, was given
  in~\cite[\S~4]{DDER14-exc}.}.
The salient features of our approach are that:
\\{\bf (1)}
The syntax of our logic is kept close to the syntax of
programming languages. This is made possible by starting from a simple
syntax without effect and by adding decorations, which often
correspond to keywords of the languages, for taking the effects into
account.
\\{\bf (2)}
We consider exceptions in two settings, the programming
  language and the core language. This enables for instance to
  separate the treatment, in proofs, of the matching between normal or
  exceptional  behavior from the actual recovery after an exceptional
  behavior.

In Section~\ref{sec:hpc} we introduce a \emph{relative} notion of
Hilbert-Post completeness in a logic $L$ with respect to a sublogic
$L_0$.
Then in Section~\ref{sec:exc} we prove the relative Hilbert-Post completeness
of a theory of exceptions based on the usual $\throw$ and
$\mathtt{try}\texttt{-}\mathtt{catch}$ statement constructors.
We go further in Section~\ref{sec:excore} by establishing
the relative Hilbert-Post completeness
of a \emph{core} theory for exceptions with individualized
$\trycore$ and $\catchcore$ statement constructors,
which is useful for expressing the behaviour of the $\mathtt{try}\texttt{-}\mathtt{catch}$
blocks.
All our completeness proofs have been verified with the Coq proof
assistant and we therefore give the main ingredients of the framework
used for this verification and the correspondence between our Coq
package and the theorems and propositions of this paper in
Section~\ref{sec:coq}.

\section{Relative Hilbert-Post completeness}
\label{sec:hpc}

Each logic in this paper comes with a \emph{language},
which is a set of \emph{formulas},
and with \emph{deduction rules}.
Deduction rules are used for deriving (or generating) \emph{theorems},
which are some formulas, from some chosen formulas called \emph{axioms}.
A \emph{theory} $T$ is a set of theorems
which is \emph{deductively closed}, in the sense that
every theorem which can be derived from $T$ using the rules of the logic
is already in $T$.
We describe a set-theoretic \emph{intended model}
for each logic we introduce;
the rules of the logic are designed so as to
be \emph{sound} with respect to this intended model.
Given a logic $L$, the theories of $L$ are partially ordered by inclusion.
There is a maximal theory $T_\mymax$, where all formulas are theorems.
There is a minimal theory $T_\mymin$, which is generated by
the empty set of axioms.
For all theories $T$ and $T'$, we denote by $T+T'$ the theory
generated from $T$ and~$T'$.

\begin{example}
\label{ex:eqn}
With this point of view there are many different
\emph{equational logics}, with the same deduction rules
but with different languages, depending on the definition of \emph{terms}.
In an equational logic, formulas are \emph{pairs of parallel terms}
$(f,g):X\to Y$
and theorems are \emph{equations} $f\equiv g:X\to Y$.
Typically, the language of an equational logic
may be defined from a \emph{signature} (made of sorts and operations).
The deduction rules are such that the equations in a theory form
a \emph{congruence}, i.e., an equivalence relation compatible with
the structure of the terms.
For instance, we may consider the logic ``of naturals'' $L_\nat$,
with its language generated from the signature made of a sort $N$,
a constant $0:\unit\to N$ and an operation $s:N\to N$.
For this logic, the minimal theory is the theory ``of naturals'' $T_\nat$,
the maximal theory is such that $s^k\equiv s^\ell$
and $s^k\circ0\equiv s^\ell\circ0$ for all natural numbers $k$ and $\ell$,
and (for instance) the theory ``of naturals modulo~6'' $T_\modsix$
can be generated from the equation $s^6\equiv \id_N$.
We consider models of equational logics in sets:
each type $X$ is interpreted as a set (still denoted $X$),
which is a singleton when $X$ is $\unit$,
each term $f:X\to Y$ as a function from $X$ to $Y$
(still denoted $f:X\to Y$),
and each equation as an equality of functions.
\end{example}

\begin{definition}
\label{defi:hpc}
Given a logic $L$ and its maximal theory $T_\mymax$,
a theory $T$ is \emph{consistent} if $T\ne T_\mymax$,
and it is \emph{Hilbert-Post complete}
if it is consistent
and if any theory containing $T$
coincides with~$T_\mymax$ or with~$T$.
\end{definition}

\begin{example}
\label{ex:hpc-eqn}
In Example~\ref{ex:eqn} we considered two theories for the logic $L_\nat$:
the theory ``of naturals'' $T_\nat$
and the theory ``of naturals modulo~6'' $T_\modsix$.
Since both are consistent and $T_\modsix$ contains $T_\nat$,
the theory $T_\nat$ is not Hilbert-Post complete.
A Hilbert-Post complete theory for $L_\nat$ is made of
all equations but $s\equiv \id_N$, it can be generated from the axioms
$s\!\circ\! 0 \!\equiv\! 0$ and $s\!\circ\! s \!\equiv\! s$.
\end{example}

If a logic $L$ is an extension of a sublogic $L_0$,
each theory $T_0$ of $L_0$ generates a theory $F(T_0)$ of $L$.
Conversely, each theory $T$ of $L$ determines a theory $G(T)$ of $L_0$,
made of the theorems of $T$ which are formulas of $L_0$,
so that $G(T_\mymax)=T_\mymaxz$.
The functions $F$ and $G$ are monotone and
they form a \emph{Galois connection}, denoted $F\dashv G$:
for each theory $T$ of $L$ and each theory $T_0$ of $L_0$ we have
$F(T_0)\subseteq T$ if and only if $T_0\subseteq G(T)$.
It follows that $T_0\subseteq G(F(T_0))$ and $F(G(T))\subseteq T$.
Until the end of Section~\ref{sec:hpc}, we consider:
\emph{a logic $L_0$, an extension $L$ of $L_0$,
and the associated Galois connection $F\dashv G$.}
\begin{definition}
\label{defi:hpc-rel}
A theory $T'$ of~$L$ is \emph{$L_0$-derivable}
from a theory $T$ of~$L$ if $T'=T+F(T'_0)$
for some theory $T'_0$ of~$L_0$.
A theory $T$ of~$L$ is \emph{(relatively) Hilbert-Post complete with respect to} $L_0$
if it is consistent
and if any theory of~$L$ containing $T$
is $L_0$-derivable from~$T$.
\end{definition}

Each theory $T$ is $L_0$-derivable from itself,
as $T=T+F(T_\myminz)$, where $T_\myminz$
is the minimal theory of $L_0$.
In addition, Theorem~\ref{theo:hpc} shows that
relative completeness
lifts the usual ``absolute'' completeness from $L_0$ to $L$,
and Proposition~\ref{prop:hpc-compose} proves that
relative completeness is well-suited to the combination of effects.
\begin{lemma}
\label{lemm:hpc-rel}
For each theory $T$ of $L$,
a theory $T'$ of $L$ is $L_0$-derivable from $T$
if and only if $T'=T+F(G(T'))$.
As a special case, $T_\mymax$ is $L_0$-derivable from $T$
if and only if $T_\mymax=T+F(T_\mymaxz)$.
A theory $T$ of $L$ is Hilbert-Post complete with respect to $L_0$
if and only if it is consistent
and every theory $T'$ of~$L$ containing $T$
is such that $T'=T+F(G(T'))$.
\end{lemma}
\begin{proof}
Clearly, if $T'=T+F(G(T'))$ then $T'$ is $L_0$-derivable from $T$.
So, let $T'_0$ be a theory of~$L_0$ such that $T'=T+F(T'_0)$,
and let us prove that $T'=T+F(G(T'))$.
For each theory $T'$ we know that $F(G(T')) \subseteq T'$;
since here $T \subseteq T'$ we get $T+F(G(T')) \subseteq T'$.
Conversely,
for each theory $T'_0$ we know that $T'_0 \subseteq G(F(T'_0))$
and that $G(F(T'_0)) \subseteq  G(T)+ G(F(T'_0)) \subseteq  G(T+F(T'_0)) $,
so that $T'_0 \subseteq G(T+F(T'_0)) $;
since here $T'=T+F(T'_0)$ we get first $T'_0 \subseteq G(T')$
and then $T'\subseteq T+F(G(T')) $.
Then, the result for $T_\mymax$ comes from the fact that $G(T_\mymax)=T_\mymaxz $.
The last point follows immediately.
\end{proof}

\begin{theorem}
\label{theo:hpc}
Let $T_0$ be a theory of $L_0$ and $T=F(T_0)$.
If $T_0$ is Hilbert-Post complete (in $L_0$)
and $T$ is Hilbert-Post complete with respect to $L_0$,
then $T$ is Hilbert-Post complete (in $L$).
\end{theorem}

\begin{proof}
Since $T$ is complete with respect to $L_0$, it is consistent.
Since $T=F(T_0)$ we have $T_0 \subseteq G(T)$.
Let $T'$ be a theory such that $T\subseteq T'$.
Since $T$ is complete with respect to $L_0$,
by Lemma~\ref{lemm:hpc-rel} we have $T'=T+F(T'_0)$ where $T'_0=G(T')$.
Since $T\subseteq T'$, $T_0 \subseteq G(T)$ and $T'_0=G(T')$,
we get $T_0 \subseteq T'_0$.
Thus, since $T_0$ is complete, either $T'_0=T_0$ or $T'_0=T_\mymaxz$;
let us check that then either $T'=T$ or $T'=T_\mymax$.
If $T'_0=T_0$ then $F(T'_0)=F(T_0)=T$, so that $T'=T+F(T'_0)=T$.
If $T'_0=T_\mymaxz$ then $F(T'_0)=F(T_\mymaxz)$;
since $T$ is complete with respect to $L_0$,
the theory $T_\mymax$ is $L_0$-derivable from $T$,
which implies (by Lemma~\ref{lemm:hpc-rel}) that
$T_\mymax=T+F(T_\mymaxz)=T'$.
\end{proof}

\begin{proposition}
\label{prop:hpc-compose}
Let $L_1$ be an intermediate logic between $L_0$ and $L$,
let $F_1\dashv G_1$ and $F_2\dashv G_2$ be the Galois connections
associated to the extensions $L_1$ of $L_0$ and $L$ of $L_1$,
respectively.
Let $T_1=F_1(T_0)$.
If $T_1$ is Hilbert-Post complete with respect to $L_0$
and $T$ is Hilbert-Post complete with respect to $L_1$
then $T$ is Hilbert-Post complete with respect to $L_0$.
\end{proposition}

\begin{proof}
This is an easy consequence of the fact that $F=F_2\circ F_1$.
\end{proof}

Corollary~\ref{coro:hpc-equations} provides a characterization
of relative Hilbert-Post completeness which is used
in the next Sections and in the Coq implementation.

\begin{definition}
\label{defi:hpc-equations}
For each set $E$ of formulas let $\Th(E)$ be the theory generated by $E$;
and when $E=\{e\}$ let $\Th(e)=\Th(\{e\})$.
Then two sets $E_1$, $E_2$ of formulas are \emph{$T$-equivalent}
if $T+\Th(E_1)=T+\Th(E_2)$;
and a formula $e$ of~$L$ is \emph{$L_0$-derivable}
from a theory $T$ of~$L$ if $\{e\}$ is $T$-equivalent to $E_0$
for some set $E_0$ of formulas of~$L_0$.
\end{definition}

\begin{proposition}
\label{prop:hpc-equations}
Let $T$ be a theory of $L$.
Each theory $T'$ of $L$ containing $T$ is $L_0$-derivable from $T$
if and only if each formula $e$ in $L$ is $L_0$-derivable from $T$.
\end{proposition}

\begin{proof}
Let us assume that each theory $T'$ of $L$ containing $T$
is $L_0$-derivable from $T$.
Let $e$ be a formula in $L$, let $T'=T+\Th(e)$,
and let $T'_0$ be a theory of $L_0$ such that $T'=T+F(T'_0)$.
The definition of $\Th(-)$ is such that $\Th(T'_0)=F(T'_0)$,
so that we get $T+\Th(e)=T+\Th(E_0)$ where $E_0= T'_0$.
Conversely,
let us assume that each formula $e$ in $L$ is $L_0$-derivable from $T$.
Let $T'$ be a theory containing $T$.
Let $T''=T+F(G(T'))$, so that $T\subseteq T''\subseteq T'$
(because $F(G(T'))\subseteq T'$ for any $T'$).
Let us consider an arbitrary formula $e$ in $T'$,
by assumption there is a set $E_0$ of formulas of $L_0$ such that
$T+\Th(e)=T+\Th(E_0)$.
Since $e$ is in $T'$ and $T\subseteq T'$ we have $T+\Th(e)\subseteq T'$,
so that $T+\Th(E_0)\subseteq T'$.
It follows that $E_0$ is a set of theorems of $T'$ which are formulas of $L_0$,
which means that $E_0\subseteq G(T')$,
and consequently $\Th(E_0)\subseteq F(G(T'))$,
so that $T+\Th(E_0)\subseteq T''$.
Since $T+\Th(e)=T+\Th(E_0)$ we get $e\in T''$.
We have proved that $T'=T''$, so that $T'$ is $L_0$-derivable from~$T$.
\end{proof}

\begin{corollary}
\label{coro:hpc-equations}
A theory $T$ of $L$ is Hilbert-Post complete with respect to $L_0$
if and only if it is consistent and for each formula $e$ of $L$
there is a set $E_0$ of formulas of~$L_0$ such that
$\{e\}$ is $T$-equivalent to $E_0$.
\end{corollary}

\section{Completeness for exceptions}
\label{sec:exc}

Exception handling is provided by most modern programming
languages. It allows to deal with anomalous or exceptional events
which require special processing. E.g., one can easily
and simultaneously compute dynamic evaluation in exact linear algebra
using exceptions \cite{DDER14-exc}.
There, we proposed to deal with exceptions as a decorated effect:
a term $f:X\to Y$ is not interpreted as a function $f: X\to Y$ unless it is
pure. A term which may raise an exception is instead
interpreted as a function $f: X\to Y + E$
where ``+'' is the disjoint union operator and $E$ is the set of exceptions.
In this section, we prove the relative Hilbert-Post completeness
of the decorated theory of exceptions in Theorem~\ref{theo:exc-complete}.

As in \cite{DDER14-exc}, decorated logics for exceptions
are obtained from equational logics by classifying terms.
Terms are classified as \emph{pure} terms or \emph{propagators},
which is expressed by adding a \emph{decoration}
or superscript, respectively $\pure$ or $\ppg$;
decoration and type information about terms
may be omitted when they are clear from the context
or when they do not matter.
All terms must propagate exceptions,
and propagators are allowed to raise an exception while pure terms are not.
The fact of catching exceptions is hidden:
it is embedded into the $\mathtt{try}\texttt{-}\mathtt{catch}$ construction, as explained below.
In Section~\ref{sec:excore}
we consider a translation
of the $\mathtt{try}\texttt{-}\mathtt{catch}$ construction in a more elementary language
where some terms are \emph{catchers},
which means that they may recover from an exception,
i.e., they do not have to propagate exceptions.

Let us describe informally a decorated theory for exceptions
and its intended model.
Each type $X$ is interpreted as a set, still denoted $X$.
The intended model is described with respect to a set $E$
called the \emph{set of exceptions}, which does not appear in the syntax.
A pure term $u^\pure:X\to Y$ is interpreted as a function $u:X\to Y$
and a propagator $a^\ppg:X\to Y$ as a function $a:X\to Y+E$;
equations are interpreted as equalities of functions.
There is an obvious conversion from pure terms to propagators,
which allows to consider all terms as propagators whenever needed;
if a propagator $a^\ppg:X\to Y$ ``is'' a pure term,
in the sense that it has been obtained by conversion from a pure term,
then the function $a:X\to Y+E$ is such that $a(x)\in Y$ for each $x\in
X$.
This means that exceptions
are always propagated: the interpretation of
$(b\circ a)^\ppg:X\to Z$ where $a^\ppg:X\to Y$ and $b^\ppg:Y\to Z$
is such that $(b\circ a)(x)=b(a(x))$ when $a(x)$ is not an exception
and $(b\circ a)(x)=e$ when $a(x)$ is the exception $e$
(more precisely, the composition of propagators is the Kleisli composition
associated to the monad $X+E$ \cite[\S~1]{Moggi91}).
Then, exceptions may be classified according to their \emph{name},
as in \cite{DDER14-exc}.
Here, in order to focus on the main features of the
proof of completeness, we assume that there is only one exception name.
Each exception is built by \emph{encapsulating} a parameter.
Let $P$ denote the type of parameters for exceptions.
The fundamental operations for raising exceptions are the propagators
$\throw_Y^\ppg :P\to Y$ for each type $Y$:
this operation throws an exception with a parameter $p$ of type $P$
and pretends that this exception has type $Y$.
The interpretation of the term $\throw_Y^\ppg :P\to Y$
is a function $\throw_Y :P\to Y+E$ such that $\throw_Y(p) \in E$
for each $p\in P$.
The fundamental operations for handling exceptions are the propagators
$(\try (a) \catch (b))^\ppg:X\to Y$
for each terms $a:X\to Y$ and $b:P\to Y$:
this operation first runs $a$ until an exception with parameter $p$
is raised (if any), then, if such an exception has been raised,
it runs $b(p)$.
The interpretation of the term $(\try (a) \catch (b))^\ppg:X\to Y$
is a function $\try (a) \catch (b) :X\to Y+E$ such that
$(\try (a) \catch (b))(x)=a(x)$ when $a$ is pure and
$(\try (a) \catch (b))(x)=b(p)$ when $a(x)$ throws an exception
with parameter $p$.

More precisely, first the definition of the
\emph{monadic equational logic} $L_\eqn$ is recalled in Fig.~\ref{fig:eqn},
(as in~\cite{Moggi91}, this terminology might be misleading:
the logic is called \emph{monadic} because all its operations are have
exactly one argument, this is unrelated to the use of the \emph{monad}
of exceptions).
\begin{figure}[ht]
\vspace{-5pt}
\begin{framed}
\small
\renewcommand{\arraystretch}{1.5}
\begin{tabular}{l}
Terms are closed under composition: \\
$u_k\circ \dots \circ u_1:X_0\!\!\to\!\! X_k$
for each $(u_i:X_{i-1}\!\!\to\!\! X_i)_{1\leq i\leq k}$,
and $\id_X:X\!\!\to\!\! X$ when $k=0$ \\
Rules:
\quad (equiv) \squad
  $\dfrac{u}{u \eqs u} \quad
  \dfrac{u \eqs v}{v \eqs u}  \quad
  \dfrac{u \eqs v \squad v \eqs w}{u \eqs w}$ \\
\quad (subs) \;
  $\dfrac{u\colon X\to Y \squad v_1 \eqs v_2 \colon Y\to Z}
    {v_1 \circ u \eqs v_2\circ u } $ \squad
(repl) \;
  $ \dfrac{v_1\eqs v_2\colon X\to Y \squad w\colon Y\to Z}
    {w\circ v_1 \eqs w\circ v_2} $ \\
Empty type $\empt$ with terms $\copa_Y:\empt\to Y$ and rule:
\quad (initial) \;
  $ \dfrac{u\colon \empt\to Y }
    {u \eqs \copa_Y} $   \\
\end{tabular}
\renewcommand{\arraystretch}{1}
\normalsize
\vspace{-2mm}
\end{framed}
\vspace{-5pt}
\caption{Monadic equational logic $L_\eqn$ (with empty type)}
\label{fig:eqn}
\end{figure}

A monadic equational logic is made of types, terms and operations,
where all operations are unary, so that terms are simply paths.
This constraint on arity
will make it easier to focus on the completeness issue.
For the same reason, we also assume that there is an \emph{empty type}
$\empt$, which is defined as an \emph{initial object}:
for each $Y$ there is a unique term $\copa_Y:\empt\to Y$
and each term $u^\pure:Y\to\empt$ is the inverse of $\copa_Y^\pure$.
In the intended model, $\empt$ is interpreted as the empty set.

Then, the monadic equational logic $L_\eqn$ is extended to form the
\emph{decorated logic for exceptions} $L_\exc$
by applying the rules in Fig.~\ref{fig:exc},
with the following intended meaning:
\begin{itemize}
\item (initial$_1$): the term $\![\,]_Y\!\!$ is
unique as a propagator, not only as a pure term.
\item (propagate): exceptions are always propagated.
\item (recover): the parameter used for throwing an exception
  may be recovered.
\item (try): equations are preserved by the exceptions mechanism.
\item (try$_0$): pure code inside $\try$ never triggers
  the code inside $\catch$.
\item (try$_1$): code inside $\catch$ is executed when
  an exception is thrown inside~$\try$.
\end{itemize}
\begin{figure}[ht]
\vspace{-5pt}
\begin{framed}
\small
\renewcommand{\arraystretch}{1.5}
\begin{tabular}{l}
Pure part: the logic $L_\eqn$ with a distinguished type $P$ \\
Decorated terms: $\throw_Y^\ppg:P\to Y$ for each type $Y$, \\
\quad $(\try (a) \catch (b))^\ppg:X\to Y$ for each $a^\ppg:X\to Y$
and $b^\ppg:P\to Y$, and \\
\quad $(a_k\circ \dots \circ a_1)^{(\max(d_1,...,d_k))}:X_0\to X_k$
for each $(a_i^{(d_i)}:X_{i-1}\to X_i)_{1\leq i\leq k}$ \\
\quad with conversion from $u^\pure:X\to Y$ to $u^\ppg:X\to Y$ \\
Rules:  \\
\quad (equiv), (subs), (repl) for all decorations  \qquad
(initial$_1$) \;
  $ \dfrac{a^\ppg\colon \empt\to Y }
    {a \eqs \copa_Y} $ \\
\quad (recover) \squad
  $\dfrac{u_1^\pure,u_2^\pure:X\to P \squad
  \throw_Y\circ u_1 \eqs \throw_Y\circ u_2}{u_1 \eqs u_2} $ \\
\quad (propagate)
  $\dfrac{a^\ppg:X\to Y}{a\circ \throw_X \eqs\throw_Y} $
\quad (try)
  $\dfrac{a_1^\ppg \eqs a_2^\ppg\!:\!X\to Y \squad b^\ppg\!:\!P\to Y}{
  \try (a_1) \catch (b) \eqs \try (a_2) \catch (b) } $ \\
\quad (try$_0$) \squad
  $\dfrac{u^\pure\!:\!X\to Y \squad b^\ppg\!:\!P\to Y}{
  \try (u) \catch (b) \eqs u} $  \quad
(try$_1$) \squad
  $\dfrac{u^\pure\!:\!X\to P \squad b^\ppg\!:\!P\to Y}{
  \try (\throw_Y \!\circ u) \catch (b) \eqs b\circ u} $ \\
\end{tabular}
\renewcommand{\arraystretch}{1}
\normalsize
\vspace{-2mm}
\end{framed}
\vspace{-5pt}
\caption{Decorated logic for exceptions $L_\exc$}
\label{fig:exc}
\end{figure}
The \emph{theory of exceptions} $T_\exc$ is the theory of $L_\exc$
generated from some arbitrary consistent theory $T_\eqn$ of $L_\eqn$;
with the notations of Section~\ref{sec:hpc}, $T_\exc=F(T_\eqn)$.
The soundness of the intended model follows: see
\cite[\S 5.1]{DDER14-exc} and~\cite{DDFR12-dual},
which are based on the description
of exceptions in Java~\cite[Ch. 14]{java} or in C++~\cite[\S 15]{cpp}.

\begin{example}\label{ex:trycatch}
Using the naturals for $P$ and the
successor and predecessor functions (resp. denoted $\mathtt{s}$ and
$\mathtt{p}$) we can prove, e.g., that
$\try(\mathtt{s}(\throw~3))\catch(\mathtt{p})$ is equivalent to $2$.
Indeed, first the rule (propagate) shows that
$\mathtt{s}(\throw~3))\equiv\throw~3$,
then the rules (try) and (try$_1$) rewrite the given term into
$\mathtt{p}(3)$.
\end{example}

Now, in order to prove the completeness of the
decorated theory for exceptions, we follow a classical method (see,
e.g., \cite[Prop 2.37~\&~2.40]{Pretnar10}):
we first determine canonical forms in Proposition~\ref{prop:exc-canonical},
then we study the equations between terms in canonical form
in Proposition~\ref{prop:exc-equations}.

\begin{proposition}
\label{prop:exc-canonical}
For each $a^\ppg\!:\!X\!\to\! Y$,
either there is a pure term $u^\pure\!:\!X\!\to\! Y$ such that $a\!\eqs\! u$
or there is a pure term $u^\pure\!:\!X\!\to\! P$ such that
$a\!\eqs\! \throw_Y \!\circ\! u$.
\end{proposition}

\begin{proof}
The proof proceeds by structural induction.
If $a$ is pure the result is obvious, otherwise
$a$ can be written in a unique way as
$a = b \circ \mathtt{op} \circ v$ where $v$ is pure, $\mathtt{op}$
is either $\throw_Z$ for some $Z$ or $\try(c)\catch(d)$
for some $c$ and $d$, and $b$ is the remaining part of $a$.
If $a = b^\ppg \circ \throw_Z \circ v^\pure$, then by (propagate)
$a \eqs \throw_Y \circ v^\pure$.
Otherwise, $a = b^\ppg \circ (\try(c^\ppg)\catch(d^\ppg)) \circ v^\pure$,
then by induction we consider two cases.
  \begin{itemize}
  \item If $c \eqs w^\pure$ then by (try$_0$)
  $a \eqs b^\ppg \circ w^\pure \circ v^\pure$ and
  by induction we consider two subcases:
    if $b \eqs t^\pure$ then $a \eqs (t \circ w \circ v)^\pure$
    and if $b \eqs \throw_Y\circ t^\pure$ then
    $a \eqs \throw_Y \circ (t \circ w \circ v)^\pure$.
    \item If $c \eqs \throw_Z \circ w^\pure$ then by (try$_1$)
  $a \eqs b^\ppg \circ d^\ppg \circ w^\pure \circ v^\pure$ and
  by induction we consider two subcases:
    if $b \circ d \eqs t^\pure$ then $a \eqs (t \circ w \circ v)^\pure$
    and if $b \circ d \eqs \throw_Y \circ t^\pure$ then
    $a \eqs \throw_Y\circ (t \circ w \circ v)^\pure$.
  \end{itemize}
\end{proof}

Thanks to Proposition~\ref{prop:exc-canonical},
the study of  equations in the logic $L_\exc$
can be restricted to pure terms
and to propagators of the form $\throw_Y \circ v$ where $v$ is pure.

\begin{proposition}
\label{prop:exc-equations}
For all $v_1^\pure,v_2^\pure:X\to P$
let $a_1^\ppg = \throw_Y \circ v_1 :X\to Y$
and $a_2^\ppg = \throw_Y \circ v_2 :X\to Y$.
Then
$ a_1^\ppg \eqs a_2^\ppg $ is $T_\exc$-equivalent to
$v_1^\pure \eqs v_2^\pure $.
\end{proposition}

\begin{proof}
Clearly, if $v_1\eqs v_2$ then $a_1\eqs a_2 $.
Conversely, if $a_1\eqs a_2 $, i.e., if
$\throw_Y \circ v_1\eqs \throw_Y \circ v_2$,
then by rule (recover) it follows that $v_1 \eqs v_2$.
\end{proof}

In the intended model, for all $v_1^\pure:X\to P$ and $v_2^\pure: X\to Y$,
it is impossible to have $\throw_Y(v_1(x))=v_2(x)$ for some $x\in X$,
because $\throw_Y(v_1(x))$ is in the $E$ summand
and $v_2(x)$ in the $Y$ summand of the disjoint union $Y+E$.
This means that the functions $\throw_Y \circ v_1$ and $v_2$
are distinct, as soon as their domain $X$ is a non-empty set.
For this reason, it is sound to make the following
Assumption~\ref{ass:exc-equations}.

\begin{assumption}
\label{ass:exc-equations}
In the logic $L_\exc$,
the type of parameters $P$ is non-empty, and
for all $v_1^\pure:X\to P$ and $v_2^\pure: X\to Y$ with $X$ non-empty,
let $a_1^\ppg = \throw_Y \circ v_1 :X\to Y$.
Then
$ a_1^\ppg \eqs v_2^\pure$ is $T_\exc$-equivalent to $T_\mymaxz$.
\end{assumption}

\begin{theorem}
\label{theo:exc-complete}
Under Assumption~\ref{ass:exc-equations},
the theory of exceptions $T_\exc$ is Hilbert-Post complete
with respect to the pure sublogic $L_\eqn$ of $L_\exc$.
\end{theorem}

\begin{proof}
Using Corollary~\ref{coro:hpc-equations},
the proof relies upon Propositions~\ref{prop:exc-canonical} and
\ref{prop:exc-equations}.
The theory $T_\exc$ is consistent, because (by soundness)
it cannot be proved that $\throw_P^\ppg \eqs \id_P^\pure$.
Now, let us consider an equation between terms with domain $X$
and let us prove that it is $T_\exc$-equivalent to a set of pure equations.
When $X$ is non-empty,
Propositions~\ref{prop:exc-canonical} and~\ref{prop:exc-equations},
together with Assumption~\ref{ass:exc-equations},
prove that the given equation is $T_\exc$-equivalent to a
set of pure equations.
When $X$ is empty, then all terms from $X$ to $Y$ are equivalent to $\copa_Y$
so that the given equation
is $T_\exc$-equivalent to the empty set of pure equations.
\end{proof}

\section{Completeness of the core language for exceptions}
\label{sec:excore}

In this section, following~\cite{DDER14-exc},
we describe a translation of the language for exceptions
from Section~\ref{sec:exc} in a \emph{core} language with
\emph{catchers}.
Thereafter, in Theorem~\ref{theo:excore-complete}, we state the
relative Hilbert-Post completeness of this core language.
Let us call the usual language for exceptions with $\throw$ and $\mathtt{try}\texttt{-}\mathtt{catch}$,
as described in Section~\ref{sec:exc},
the \emph{programmers' language} for exceptions.
The documentation on the behaviour of exceptions in many languages
(for instance in Java \cite{java})
makes use of a \emph{core language} for exceptions
which is studied in \cite{DDER14-exc}.
In this language, the empty type plays an important role and
the fundamental operations for dealing with exceptions
are $\tagg^\ppg:P\to \empt$ for encapsulating a parameter inside an exception
and $\untag^\ctc:\empt\to P$ for recovering its parameter
from any given exception. The new decoration $\ctc$ corresponds to
\emph{catchers}: a catcher may recover from an exception,
it does not have to propagate it.
Moreover, the equations also are decorated:
in addition to the equations '$\eqs$' as in Section~\ref{sec:exc},
now called \emph{strong equations}, there are
\emph{weak equations} denoted '$\eqw$'.

As in Section~\ref{sec:exc}, a set $E$ of exceptions is chosen;
the interpretation is extended as follows:
each catcher $f^\ctc:X\to Y$ is interpreted as a function $f:X+E\to Y+E$,
and there is an obvious conversion from propagators to catchers;
the interpretation of the composition of catchers is straightforward,
and it is compatible with the Kleisli composition for propagators.
Weak and strong equations coincide on propagators,
where they are interpreted as equalities,
but they differ on catchers:
$f^\ctc \eqw g^\ctc:X\to Y$ means that the functions
$f,g:X+E\to Y+E$ coincide on $X$, but maybe not on $E$.
The interpretation of $\tagg^\ppg:P\to \empt$
is an injective function $\tagg:P\to E$ and the interpretation of
$\untag^\ctc:\empt\to P$ is a function $\untag:E\to P+E$ such that
$\untag(\tagg(p))=p$ for each parameter $p$.
Thus, the fundamental axiom relating $\tagg^\ppg$ and $\untag^\ctc$
is the weak equation $ \untag \circ \tagg \eqw \id_P$.

\begin{figure}[ht]
\vspace{-5pt}
\begin{framed}
\small
\renewcommand{\arraystretch}{1.5}
\begin{tabular}{l}
Pure part: the logic $L_\eqn$ with a distinguished type $P$ \\
Decorated terms: $\tagg^\acc \colon P\to \empt$,
$\untag^\ctc \colon \empt\to P$, and \\
\quad $(f_k\circ \dots \circ f_1)^{(\max(d_1,...,d_k))}:X_0\to X_k$
for each $(f_i^{(d_i)}:X_{i-1}\to X_i)_{1\leq i\leq k}$ \\
\quad with conversions from $f^\pure$ to $f^\ppg$
and from $f^\ppg$ to $f^\ctc$ \\
Rules:  \\
\quad (equiv$_\eqs$), (subs$_\eqs$), (repl$_\eqs$) for all decorations  \\
\quad (equiv$_\eqw$), (repl$_\eqw$) for all decorations,
  (subs$_\eqw$) only when $h$ is pure \\
\quad (empty$_\eqw$) \squad
  $\dfrac{f\colon \empt\to Y}{f \eqw \copa_Y}$
\quad ($\eqs$-to-$\eqw$) \squad
  $\dfrac{f\eqs g}{f\eqw g} $
\quad (ax) \squad
  $\dfrac{}{\untag \circ \tagg \eqw \id_P} $  \\
\quad (eq$_1$) \squad
  $\dfrac{f_1^{(d_1)}\eqw f_2^{(d_2)}}{f_1\eqs f_2}$
  only when $d_1\leq 1$ and $d_2\leq 1$ \\
\quad (eq$_2$) \squad
  $\dfrac{f_1,f_2\colon X\to Y \;\;
  f_1\eqw f_2 \;\; f_1 \circ \copa_X \eqs f_2 \circ \copa_X}{f_1\eqs f_2}$ \\
\quad (eq$_3$) \squad
  $\dfrac{f_1,f_2\colon \empt\to X \quad f_1 \circ \tagg \eqw f_2 \circ \tagg}
    {f_1\eqs f_2}$ \\
\end{tabular}
\renewcommand{\arraystretch}{1}
\normalsize
\vspace{-2mm}
\end{framed}
\vspace{-5pt}
\caption{Decorated logic for the core language for exceptions $L_\excore$}
\label{fig:excore}
\end{figure}

More precisely, the
\emph{decorated logic for the core language for exceptions}
$L_\excore$
is defined in Fig.~\ref{fig:excore} as an extension of the
monadic equational logic $L_\eqn$.
There is an obvious conversion from strong to weak equations ($\eqs$-to-$\eqw$),
and in addition strong and weak equations coincide on propagators
by rule (eq$_1$).
Two catchers $f_1^\ctc,f_2^\ctc:X\to Y$ behave in the same way on exceptions
if and only if $f_1\circ\copa_X \eqs f_2\circ\copa_X :\empt\to Y$, where
$\copa_X:\empt\to X$ builds a term of type $X$ from any exception.
Then rule (eq$_2$) expresses the fact that weak and strong equations
are related by the property that $f_1\eqs f_2$ if and only if
$f_1\eqw f_2$ and $f_1\circ\copa_X \eqs f_2\circ\copa_X$.
This can also be expressed as a pair of weak equations:
$f_1\eqs f_2$ if and only if
$f_1\eqw f_2$ and $f_1\circ\copa_X\circ\tagg \eqw f_2\circ\copa_X\circ\tagg$
by rule (eq$_3$).
The \emph{core theory of exceptions} $T_\excore$ is the theory of $L_\excore$
generated from the theory $T_\eqn$ of $L_\eqn$.
Some easily derived properties are stated in Lemma~\ref{lemm:excore-ul};
which will be used repeatedly.
\begin{lemma}
\label{lemm:excore-ul}
\begin{enumerate}
\item \label{pt:excore-ul-lulu}
For all pure terms $u_1^\pure,u_2^\pure:X\to P$, the equation
  $ u_1 \eqs u_2 $ is $T_\excore$-equivalent to
  $\tagg \circ u_1 \eqs \tagg \circ u_2 $ and also to
  $\untag \circ \tagg \circ u_1 \eqs \untag \circ \tagg \circ u_2 $.
\item \label{pt:excore-ul-l}
For all pure terms $u^\pure:X\to P$, $v^\pure:X\to\empt$, the equation
  $ u \eqs \copa_P \circ v$ is $T_\excore$-equivalent to
  $\tagg \circ u \eqs v $.
\end{enumerate}
\end{lemma}

\begin{proof}
\begin{enumerate}
\item %
Implications from left to right are clear. Conversely, if
$\untag \circ \tagg \circ u_1 \eqs \untag \circ \tagg \circ u_2 $,
then using the axiom (ax) and the rule (subs$_\eqw$) we get $u_1 \eqw u_2$.
Since $u_1$ and $u_2$ are pure this means that $u_1 \eqs u_2$.
\item %
First, since $\tagg \circ \copa_P :\empt\to\empt $ is a propagator
we have $\tagg \circ \copa_P \eqs \id_\empt$.
Now, if $ u \eqs \copa_P \circ v$ then
$ \tagg \circ u \eqs \tagg \circ \copa_P \circ v \eqs v$.
Conversely, if $\tagg \circ u \eqs v$ then
$\tagg \circ u \eqs \tagg \circ \copa_P \circ v$,
and by Point~\ref{pt:excore-ul-lulu} this means that $u \eqs \copa_P \circ v$.
\end{enumerate}
\end{proof}

The operation $\untag$ in the core language can be used for decomposing
the $\mathtt{try}\texttt{-}\mathtt{catch}$ construction in the programmer's language
in two steps: a step for catching the exception,
which is nested into a second step inside the $\mathtt{try}\texttt{-}\mathtt{catch}$ block:
this corresponds to a translation
of the programmer's language in the core language,
as in \cite{DDER14-exc}, which is reminded below;
then Proposition~\ref{prop:excore-impl} proves the correctness
of this translation.
In view of this translation we extend the core language with:
\begin{itemize}
\item for each $b^\ppg:P\to Y$, a catcher $(\catchcore(b))^\ctc:Y\to Y$
such that $\catchcore(b) \eqw \id_Y $ and
$\catchcore(b)\circ\copa_Y \eqs b\circ\untag$:
if the argument of $\catchcore(b)$ is non-exceptional then nothing is done,
otherwise the parameter $p$ of the exception is recovered and $b(p)$ is ran.
\item for each $a^\ppg\!:\!X\to Y$ and $k^\ctc\!:\!Y\to Y$,
a propagator $ (\trycore(a,k))^\ppg :X\to Y$
such that $ \trycore(a,k) \eqw k\circ a$:
thus $\trycore(a,k)$ behaves as $k\circ a$ on non-exceptional arguments,
but it does always propagate exceptions.
\end{itemize}
Then, a translation of the programmer's language of exceptions
in the core language is easily obtained:
for each type $Y$, $\throw_Y^\ppg \!=\! \copa_Y \circ \tagg :P\to Y$.
and for each $a^\ppg\!:\!X\!\to\! Y$, $b^\ppg\!:\!P\!\to\! Y$,
$(\try (a) \catch (b))^\ppg \!=\! \trycore(a,\catchcore(b))\!:\!X\!\to\! Y$.
This translation is correct: see Proposition~\ref{prop:excore-impl}.

\begin{proposition}
\label{prop:excore-impl}
If the pure term $\copa_Y:\empt\to Y$ is a monomorphism with respect
to propagators for each type $Y$,
the above translation of the programmers' language for exceptions
in the core language is correct.
\end{proposition}

\begin{proof}
We have to prove that the image of each rule of $L_\exc$ is satisfied.
It should be reminded that strong and weak equations coincide on $L_\exc$.
\begin{itemize}
\item (propagate) For each $a^\ppg:X\to Y$,
the rules of $L_\excore$ imply that $a\circ \copa_X \eqs \copa_Y$, so that
$a\circ \copa_X \circ \tagg \eqs \copa_Y \circ \tagg $.
\item (recover) For each $u_1^\pure,u_2^\pure:X\to P$,
if $\copa_Y \circ \tagg \circ u_1 \eqs \copa_Y \circ \tagg \circ u_2 $
since $\copa_Y$ is a monomorphism with respect to propagators
we have $\tagg \circ u_1 \eqs \tagg \circ u_2 $,
so that,
by Point~\ref{pt:excore-ul-lulu} in Lemma~\ref{lemm:excore-ul},
we get $u_1 \eqs u_2 $.
\item (try)
Since $\try(a_i)\catch(b) \eqw \catch(b) \circ a_i$
for $i\in\{1,2\}$, we get $\try(a_1)\catch(b) \eqw \try(a_2)\catch(b)$
as soon as $a_1\eqs a_2$.
\item (try$_0$) For each $u^\pure:X\to Y$ and $b^\ppg:P\to Y$,
we have $\trycore(u,\catchcore(b)) \eqw \catchcore(b) \circ u$
and $\catchcore(b) \circ u \eqw u $
(because $\catchcore(b)\eqw\id $ and $u$ is pure),
so that $\trycore(u,\catchcore(b)) \eqw u $.
\item (try$_1$) For each $u^\pure:X\to P$ and $b^\ppg:P\to Y$,
we have $\trycore(\copa_Y \circ \tagg \circ u,\catchcore(b)) \eqw
\catchcore(b) \circ \copa_Y \circ \tagg \circ u$
and $ \catchcore(b) \circ \copa_Y \eqs b \circ \untag$
so that $\trycore(\copa_Y \circ \tagg \circ u,\catchcore(b)) \eqw
b \circ \untag \circ \tagg \circ u$.
We have also $ \untag \circ \tagg \circ u \eqw u$
(because $\untag \circ \tagg \eqw\id $ and $u$ is pure),
so that $\trycore(\copa_Y \circ \tagg \circ u,\catchcore(b)) \eqw
b \circ u$.
\end{itemize}
\end{proof}

\begin{example}[Continuation of
  Example~\ref{ex:trycatch}]\label{ex:taguntag}
We here show that it is possible to separate the matching between
normal or exceptional
behavior from the recovery after an
exceptional behavior: to prove that
$\try(\mathtt{s}(\throw~3))\catch(\mathtt{p})$ is equivalent to $2$
in the core language, we first use the translation to get:
$\trycore(\mathtt{s}\circ\copa\circ\tagg\circ{}3,\catchcore(\mathtt{p}))$.
Then
(empty$_\eqw$) shows that
$\mathtt{s}\circ\copa\tagg\circ{}3\eqw\copa\circ\tagg\circ{}3$.
Now,
the $\trycore$ and $\catchcore$ translations show that
$\trycore(\copa\circ\tagg\circ{}3,\catchcore(\mathtt{p})) \eqw
\catchcore(\mathtt{p})\circ\copa\circ\tagg\circ{}3 \eqw
\mathtt{p}\circ\untag\circ\tagg\circ{}3$.
Finally the axiom (ax) and (eq$_1$) give
$\mathtt{p}\circ{}3\eqs{}2$.
\end{example}

In order to prove the completeness of
the core decorated theory for exceptions,
as for the proof of Theorem~\ref{theo:exc-complete},
we first determine canonical forms
in Proposition~\ref{prop:excore-canonical},
then we study the equations between terms in canonical form
in Proposition~\ref{prop:excore-equations}.
Let us begin by proving the
\emph{fundamental strong equation for exceptions}~(\ref{eq:excore-fundamental}):
by replacement in the axiom (ax)
we get $\tagg \circ \untag \circ \tagg \eqw \tagg $,
then by rule (eq$_3$):
\begin{equation}
\label{eq:excore-fundamental}
 \tagg \circ \untag \eqs \id_\empt
\end{equation}

\begin{proposition}
\label{prop:excore-canonical}
\begin{enumerate}
\item \label{pt:excore-canonical-acc}
For each propagator $a^\ppg:X\to Y$, either $a$ is pure or
there is a pure term $v^\pure:X\to P$ such that
$ a^\ppg \eqs \copa_Y^\pure \circ \tagg^\ppg \circ v^\pure $.
And for each propagator $a^\ppg:X\to \empt$ (either pure or not),
there is a pure term $v^\pure:X\to P$ such that
$ a^\ppg \eqs \tagg^\ppg \circ v^\pure $.
\item \label{pt:excore-canonical-ctc}
For each catcher $f^\ctc:X\to Y$, either $f$ is a propagator or
there is an propagator $a^\acc:P\to Y$ and a pure term $u^\pure:X\to P$
such that
$ f^\ctc \eqs a^\ppg \circ \untag^\ctc \circ \tagg^\ppg \circ u^\pure $.
\end{enumerate}
\end{proposition}

\begin{proof}
\begin{enumerate}
\item %
If the propagator $a^\ppg:X\to Y$ is not pure then it contains
at least one occurrence of $\tagg^\ppg$.
Thus, it can be written in a unique way as
$ a = b \circ \tagg \circ v$ for some propagator $b^\ppg:\empt\to Y$
and some pure term $v^\pure:X\to P$.
Since $b^\ppg:\empt\to Y$ we have $b^\ppg\eqs\copa_Y^\pure$,
and the first result follows.
When $X=\empt$, it follows that $a^\ppg \eqs \tagg^\ppg \circ v^\pure$.
When $a:X\to \empt$ is pure, one has
$a \eqs \tagg^\ppg \circ (\copa_P \circ a)^\pure$.
\item %
The proof proceeds by structural induction.
If $f$ is pure the result is obvious, otherwise
$f$ can be written in a unique way as
$f = g \circ \mathtt{op} \circ u$ where $u$ is pure, $\mathtt{op}$
is either $\tagg$ or $\untag$ and $g$ is the remaining part of $f$.
By induction, either $g$ is a propagator or
$g \eqs b\circ \untag \circ \tagg \circ v$
for some pure term $v$ and some propagator $b$.
So, there are four cases to consider.
(1) If $\mathtt{op}=\tagg$ and $g$ is a propagator then
$f$ is a propagator.
(2) If $\mathtt{op}=\untag$ and $g$ is a propagator then
by Point~\ref{pt:excore-canonical-acc}
there is a pure term $w$ such that $u \eqs \tagg \circ w$,
so that $f \eqs g^\ppg \circ \untag \circ \tagg \circ w^\pure$.
(3) If $\mathtt{op}=\tagg$ and
$g \eqs b^\ppg\circ \untag \circ \tagg \circ v^\pure$ then
$f \eqs b\circ \untag \circ \tagg \circ v \circ \tagg \circ u$.
Since $v: \empt\to P$ is pure we have $\tagg \circ v \eqs \id_\empt$,
so that $f \eqs b^\ppg\circ \untag \circ \tagg \circ u^\pure$.
(4) If $\mathtt{op}=\untag$ and
$g \eqs b^\ppg \circ \untag \circ \tagg \circ v^\pure$ then
$f \eqs b \circ \untag \circ \tagg \circ v \circ \untag \circ u$.
Since $v$ is pure, by (ax) and (subs$_\eqw$) we have
$ \untag \circ \tagg \circ v \eqw v $.
Besides, by (ax) and (repl$_\eqw$) we have
$ v \circ \untag \circ \tagg \eqw v $ and
$ \untag \circ \tagg \circ v \circ \untag \circ \tagg \eqw
\untag \circ \tagg \circ v $. %
Since $\eqw$ is an equivalence relation these three weak equations imply
$ \untag \circ \tagg \circ v \circ \untag \circ \tagg \eqw
v \circ \untag \circ \tagg $.
By rule (eq$_3$) we get
$ \untag \circ \tagg \circ v \circ \untag \eqs v \circ \untag$,
and by Point~\ref{pt:excore-canonical-acc} there is
a pure term $w$ such that $u \eqs \tagg \circ w$,
so that
$f \eqs (b \circ v)^\ppg \circ \untag \circ \tagg \circ w^\pure$.
\end{enumerate}
\end{proof}

Thanks to Proposition~\ref{prop:excore-canonical},
in order to study equations in the logic $L_\excore$
we may restrict our study to pure terms,
propagators of the form $\copa_Y^\pure \circ \tagg^\ppg \circ v^\pure$
and catchers of the form
$a^\ppg \circ \untag^\ctc \circ \tagg^\ppg \circ u^\pure$.

\begin{proposition}
\label{prop:excore-equations}
\begin{enumerate}
\item
\label{prop:excore-equations-ctc-ctc}
For all $a_1^\ppg,a_2^\ppg:P\to Y$ and $u_1^\pure,u_2^\pure:X\to P$,
let $f_1^\ctc = a_1\circ \untag\circ \tagg\circ u_1:X\to Y$
and $f_2^\ctc = a_2\circ \untag\circ \tagg\circ u_2:X\to Y$,
then $f_1 \eqw f_2 $ is $T_\excore$-equivalent to
$ a_1\circ u_1 \eqs a_2\circ u_2 $
and $ f_1\eqs f_2 $ is $T_\excore$-equivalent to
$ \{ a_1\eqs a_2 \;,\; a_1\circ u_1 \eqs a_2\circ u_2 \}$.
\item
\label{prop:excore-equations-ctc-ppg}
For all $a_1^\ppg:P\to Y$, $u_1^\pure:X\to P$ and $a_2^\ppg:X\to Y$,
let $ f_1^\ctc = a_1\circ \untag\circ \tagg\circ u_1:X\to Y$,
then
$f_1 \eqw a_2$ is $T_\excore$-equivalent to
$ a_1\circ u_1 \eqs a_2 $ and
$f_1 \eqs a_2$ is $T_\excore$-equivalent to
$ \{ a_1\circ u_1 \eqs a_2 \;,\; a_1\eqs \copa_Y \circ \tagg \}$.
\item
\label{pt:excorec-equations-ppg-ppg}
Let us assume that $\copa_Y^\pure$ is a monomorphism with respect
to propagators.
For all $v_1^\pure,v_2^\pure:X\to P$,
let $a_1^\ppg = \copa_Y\circ \tagg \circ v_1:X\to Y$
and $a_2^\ppg = \copa_Y\circ \tagg \circ v_2:X\to Y$.
Then
$ a_1\eqs a_2 $ is $T_\excore$-equivalent to
$ v_1\eqs v_2 $.
\end{enumerate}
\end{proposition}

\begin{proof}
\begin{enumerate}
\item %
Rule (eq$_2$) implies that $f_1\eqs f_2$ if and only if
$f_1\eqw f2$ and $f_1 \circ \copa_X \eqs f_2 \circ \copa_X$.
On the one hand, $f_1\eqw f_2$ if and only if $a_1\circ u_1 \eqs a_2\circ u_2$:
indeed, for each $i\in\{1,2\}$, by (ax) and (subs$_\eqw$), since $u_i$ is pure
we have $f_i \eqw a_i \circ u_i$.
On the other hand, let us prove that
$f_1 \circ \copa_X \eqs f_2 \circ \copa_X$ if and only if $a_1 \eqs a_2$.
For each $i\in\{1,2\}$,
the propagator $\tagg \circ u_i \circ \copa_X : \empt\to\empt$ satisfies
$\tagg \circ u_i \circ \copa_X \eqs \id_\empt$,
so that $f_i \circ \copa_X \eqs a_i \circ \untag $.
Thus, $f_1 \circ \copa_X \eqs f_2 \circ \copa_X$ if and only if
$a_1 \circ \untag \eqs a_2 \circ \untag$.
Clearly, if $a_1 \eqs a_2$ then $a_1 \circ \untag \eqs a_2 \circ \untag$.
Conversely, if $a_1 \circ \untag \eqs a_2 \circ \untag$
then $a_1 \circ \untag \circ \tagg \eqs a_2 \circ \untag \circ \tagg $,
so that by (ax) and (repl$_\eqw$) we get $a_1 \eqw a_2$,
which means that $a_1 \eqs a_2$ because $a_1$ and $a_2$ are propagators.
\item %
Rule (eq$_2$) implies that $f_1\eqs a_2$ if and only if
$f_1\eqw a_2$ and $f_1 \circ \copa_X \eqs a_2 \circ \copa_X$.
On the one hand, $f_1\eqw a_2$ if and only if $a_1\circ u_1 \eqs a_2$:
indeed, by (ax) and (subs$_\eqw$), since $u_1$ is pure
we have $f_1 \eqw a_1 \circ u_1$.
On the other hand, let us prove that
$f_1 \circ \copa_X \eqs a_2 \circ \copa_X$ if and only if
$a_1\eqs \copa_Y \circ \tagg$, in two steps.
Since $ a_2 \circ \copa_X : \empt\to Y$ is a propagator,
we have $ a_2 \circ \copa_X \eqs \copa_Y$.
Since $f_1 \circ \copa_X =
a_1\circ \untag\circ \tagg\circ u_1 \circ \copa_X$
with $\tagg\circ u_1 \circ \copa_X:\empt\to\empt $ a propagator,
we have $\tagg\circ u_1 \circ \copa_X \eqs \id_\empt$
and thus we get $ f_1 \circ \copa_X \eqs a_1\circ \untag$.
Thus, $f_1 \circ \copa_X \eqs a_2 \circ \copa_X$ if and only if
$a_1\circ \untag \eqs \copa_Y$.
If $a_1\circ \untag \eqs \copa_Y$ then
$a_1\circ \untag\circ \tagg \eqs \copa_Y\circ \tagg$,
by (ax) and (repl$_\eqw$) this implies
$a_1 \eqw \copa_Y\circ \tagg$, which is a strong equality because
both members are propagators.
Conversely, if $a_1 \eqs \copa_Y\circ \tagg $
then $a_1 \circ \untag \eqs \copa_Y\circ \tagg \circ \untag $,
by the fundamental equation~(\ref{eq:excore-fundamental})
this implies $a_1 \circ \untag \eqs \copa_Y$.
Thus, $a_1\circ \untag \eqs \copa_Y$ if and only if
$a_1 \eqs \copa_Y\circ \tagg $.
\item
Clearly, if $ v_1\eqs v_2 $ then
$ \copa_Y\circ \tagg \circ v_1\eqs \copa_Y\circ \tagg \circ v_2$.
Conversely, if $ \copa_Y\circ \tagg \circ v_1\eqs \copa_Y\circ \tagg \circ v_2$
then since $\copa_Y$ is a monomorphism with respect to propagators
we get $ \tagg \circ v_1\eqs \tagg \circ v_2$,
so that $ \untag \circ \tagg \circ v_1\eqs \untag \circ \tagg \circ v_2$.
Now, from (ax) we get $ v_1\eqw v_2 $, which means that
$ v_1\eqs v_2 $ because $v_1$ and $v_2$ are pure.
\end{enumerate}
\end{proof}

Assumption~\ref{ass:excore-equations}
is the image of Assumption~\ref{ass:exc-equations}
by the above translation.

\begin{assumption}
\label{ass:excore-equations}
In the logic $L_\excore$,
the type of parameters $P$ is non-empty, and
for all $v_1^\pure:X\to P$ and $v_2^\pure: X\to Y$ with $X$ non-empty,
let $a_1^\ppg = \copa_Y\circ \tagg \circ v_1 :X\to Y$.
Then
$ a_1^\ppg \eqs v_2^\pure$ is $T_\exc$-equivalent to $T_\mymaxz$.
\end{assumption}

\begin{theorem}
\label{theo:excore-complete}
Under Assumption~\ref{ass:excore-equations},
the theory of exceptions $T_\excore$ is Hilbert-Post complete
with respect to the pure sublogic $L_\eqn$ of $L_\excore$.
\end{theorem}

\begin{proof}
Using Corollary~\ref{coro:hpc-equations},
the proof is based upon Propositions~\ref{prop:excore-canonical} and
\ref{prop:excore-equations}.
It follows the same lines as the proof of Theorem~\ref{theo:exc-complete},
except when $X$ is empty: because of catchers the proof here
is slightly more subtle.
First, the theory $T_\excore$ is consistent, because (by soundness)
it cannot be proved that $\untag^\ctc \eqs \copa_P^\pure$.
Now, let us consider an equation between terms $f_1,f_2:X\to Y$,
and let us prove that it is $T_\excore$-equivalent to a set of pure equations.
When $X$ is non-empty,
Propositions~\ref{prop:excore-canonical} and~\ref{prop:excore-equations},
together with Assumption~\ref{ass:excore-equations},
prove that the given equation is $T_\excore$-equivalent to a
set of pure equations.
When $X$ is empty, then $f_1\eqw \copa_Y$ and $f_2\eqw \copa_Y$,
so that if the equation is weak or if both $f_1$ and $f_2$ are propagators
then the given equation is
$T_\excore$-equivalent to the empty set of equations between pure terms.
When $X$ is empty and the equation is $f_1 \eqs f_2$ with
at least one of $f_1$ and $f_2$ a catcher, then
by Point~\ref{prop:excore-equations-ctc-ctc}
or~\ref{prop:excore-equations-ctc-ppg}
of Proposition~\ref{prop:excore-equations},
the given equation is $T_\excore$-equivalent to a set of
equations between propagators;
but we have seen that each equation between propagators
(whether $X$ is empty or not) is
$T_\excore$-equivalent to a set of equations between pure terms,
so that $f_1\eqs f_2$ is $T_\excore$-equivalent to the union of
these sets of pure equations.
\end{proof}

\section{Verification of Hilbert-Post Completeness in Coq}
\label{sec:coq}

All the statements of Sections~\ref{sec:exc} and~\ref{sec:excore}
have been checked in Coq.
The proofs can be found in
\url{http://forge.imag.fr/frs/download.php/680/hp-0.7.tar.gz},
as well as an almost dual proof for the completeness of the state.
They share the same framework, defined  in~\cite{DDEP13-coq}:
\begin{enumerate}
\item the terms of each logic are inductively
defined through the dependent type named $\mathtt{term}$ which builds
a new \texttt{Type} out of two input \texttt{Type}s.
For instance, $\mathtt{term \ Y \ X}$ is the \texttt{Type} of all terms
of the form $\mathtt{f\colon X\to Y}$;
\item the decorations are enumerated:
\texttt{pure} and \texttt{propagator} for both languages,
and \texttt{catcher} for the core language;
\item decorations are inductively assigned to the terms via the
dependent type called $\mathtt{is}$. The latter builds a proposition
(a \texttt{Prop} instance in Coq) out of a \texttt{term} and a
decoration. Accordingly, \texttt{is pure (id X)} is a \texttt{Prop}
instance;
\item for the core language,
we state the rules with respect to weak and strong equalities
by defining them in a mutually inductive way.
\end{enumerate}

The completeness proof for the exceptions core language
is 950 SLOC in Coq where it is 460 SLOC in \LaTeX.
Full certification runs in 6.745s on a Intel i7-3630QM @2.40GHz
using the Coq Proof Assistant, v. 8.4pl3.
Below table details the proof lengths and timings for each library.

\begin{center}
\begin{tabular}{ |l||l|l|l|l|}
 \hline
 \multicolumn{5}{|c|}{Proof lengths \& Benchmarks} \\
 \hline
 package    & source  & length  & length  & execution time \\
   &   &  in Coq  & in \LaTeX  & in Coq \\
  \hline
 exc\_cl-hp  \;  & HPCompleteCoq.v \;  &40 KB&   15 KB&6.745 sec. \\
 exc\_pl-hp &   HPCompleteCoq.v  & 8 KB   &6 KB&1.704 sec. \\
 exc\_trans & Translation.v & 4 KB&  2 KB&1.696 sec. \\
 st-hp & HPCompleteCoq.v & 48 KB&  15 KB &7.183 sec.\\
 \hline
\end{tabular}
\end{center}

The correspondence between the propositions and theorems
in this paper and their proofs in Coq is given in Fig.~\ref{fig:coq-table},
and the dependency chart for the main results in Fig.~\ref{fig:coq-chart}.
For instance,
Proposition~\ref{prop:exc-equations} is expressed in Coq as:
\scriptsize
\begin{verbatim}
forall {X Y} (a1 a2: term X Y) (v1 v2: term (Val e) Y),
    (is pure v1) /\ (is pure v2) /\
    (a1 = ((@throw X e) o v1)) /\ (a2 = ((@throw X e) o v2)) -> ((a1 == a2) <-> (v1 == v2)).
\end{verbatim}
\normalsize

\begin{figure}[ht]

\renewcommand{\arraystretch}{1}
\begin{center}
\begin{tabular}{ |l|l|}
\hline
\multicolumn{2}{|c|}{ hp-0.7/exc$\_$trans/Translation.v} \\
\hline
Proposition~\ref{prop:excore-impl} (propagate) & \texttt{propagate} \\
Proposition~\ref{prop:excore-impl} (recover) & \texttt{recover} \\
Proposition~\ref{prop:excore-impl} (try) & \texttt{try} \\
Proposition~\ref{prop:excore-impl} (try$_0$) & \texttt{try$_0$} \\
Proposition~\ref{prop:excore-impl} (try$_1$) & \texttt{try$_1$} \\
\hline
\end{tabular}  \\
\vspace{15pt}
\begin{tabular}{ |l|l|}
\hline
\multicolumn{2}{|c|}{ hp-0.7/exc$\_$pl-hp/HPCompleteCoq.v} \\
\hline
Proposition~\ref{prop:exc-canonical} \; & \texttt{can$\_$form$\_$th} \\
Proposition~\ref{prop:exc-equations}
& \texttt{eq$\_$th$\_$1$\_$eq$\_$pu} \\
Assumption~\ref{ass:exc-equations} \; & \texttt{eq$\_$th$\_$pu$\_$abs} \\
Theorem~\ref{theo:exc-complete} & \texttt{HPC$\_$exc$\_$pl} \\
\hline
\end{tabular}\\

\begin{tabular}{ |l|l|}
\multicolumn{2}{c}{ \null } \\
\hline
\multicolumn{2}{|c|}{ hp-0.7/exc$\_$cl-hp/HPCompleteCoq.v} \\
\hline
Proposition~\ref{prop:excore-canonical}~Point~\ref{pt:excore-canonical-acc}
& \texttt{can$\_$form$\_$pr} \\
Proposition~\ref{prop:excore-canonical}~Point~\ref{pt:excore-canonical-ctc}
& \texttt{can$\_$form$\_$ca} \\
Assumption~\ref{ass:excore-equations} & \texttt{eq$\_$pr$\_$pu$\_$abs} \\
Proposition~\ref{prop:excore-equations}~Point~\ref{prop:excore-equations-ctc-ctc} & \texttt{eq$\_$ca$\_$2$\_$eq$\_$pr} \\
Proposition~\ref{prop:excore-equations}~Point~\ref{prop:excore-equations-ctc-ppg} & \texttt{eq$\_$ca$\_$pr$\_$2$\_$eq$\_$pr} \\
Proposition~\ref{prop:excore-equations}~Point~\ref{pt:excorec-equations-ppg-ppg} & \texttt{eq$\_$pr$\_$1$\_$eq$\_$pu} \\
Theorem~\ref{theo:excore-complete} & \texttt{HPC$\_$exc$\_$core} \\
\hline
\end{tabular}
\end{center}
\renewcommand{\arraystretch}{1}
\vspace{-15pt}
\caption{Correspondence between theorems in this paper and
  their Coq counterparts}
\label{fig:coq-table}
\end{figure}
\begin{figure}[H]
\begin{framed}
\hspace{-5mm}
\small
$ \xymatrix@C=.2pc@R=-.3pc{
\mathtt{can\_form\_ca} \ar[dr] &\\
& \mathtt{eq\_ca\_1\_or\_2\_eq\_pr} \ar[ddr] \ar[ddddddr]\\
\mathtt{eq\_ca\_pr\_2\_eq\_pr} \ar[ur] &\\
& & \mathtt{eq\_ca\_abs\_or\_2\_eq\_pu} \ar[ddr]\\
\mathtt{can\_form\_pr} \ar[dr]\\
\mathtt{eq\_pr\_1\_eq\_pu} \ar[r] & \mathtt{eq\_pr\_abs\_or\_1\_eq\_pu} \ar[uur] \ar[ddr] & &\mathtt{HPC\_exc}\\
\mathtt{eq\_pr\_pu\_abs} \ar[ur]&\\
& & \mathtt{eq\_ca\_abs\_2\_eq\_pu\_dom\_emp}\ar[uur]\\
& \mathtt{eq\_pr\_dom\_emp}\ar[ur]\\
} $
\normalsize
\vspace{-2mm}
\end{framed}
\vspace{-15pt}
\caption{Dependency chart for the main results}
\label{fig:coq-chart}
\end{figure}

\section{Conclusion and future work}

This paper is a first step towards the proof of completeness
of decorated logics for computer languages.
It has to be extended in several directions:
adding basic features to the language (arity, conditionals, loops, \dots),
proving completeness of the decorated approach for other effects
(not only states and exceptions);
the combination of effects should easily follow,
thanks to Proposition~\ref{prop:hpc-compose}.

redpajama_set_name: RedPajamaArXiv


At Bruce M. Bieber, DDS, we strive to provide the best possible care and service for our patients. Please leave a review to let us know how we are doing and to share your experience with others.
Dr. Bruce was very professional and made me feel comfortable throughout the whole process. Would highly recommend!
I had 2 visits with Dr. Bieber when he did work on my teeth. I found him to be very professional. His work was very organized and he seemed very efficient. The office was clean and Dr. Bieber is a very punctual dentist. You get to see him right away. All in all, it was a favorable experience. I would recommend him as a dentist.
Dr. Bieber is pleasant, he makes one feel comfortable immediately. Would definitely recommend.
Continue to have great experience at DR Biebers office. They just put a new hardwood floor in the office and it makes the place look very bright and comfortable. Already was a nice office but looks even better Did whitening today for my wife and she was thrilled. Thanks.
Dr. Bieber is a great dentist! Experienced, fast and pain free. I have been to many dental offices and have had dental work by other dentist, Dr. Bieber is the best by far.
Just saw Dr Bieber yesterday with my entire family...Saw us right on time...Was totally Painless and explained everything to my wife and I .......My kids loved him . His office was very comfortable, and clean and he just had a nice professional manner about him. We need to go back for treatment so i'm definitely comfortable we made the right choice. His fees are very reasonable for the area as well. Thanks Google !!!
Fabulous Dentist and Great staff.....Nice Super Clean office in great neighborhood ..........I left my other dental office and found Dr Bieber through his great reviews on google.......... Was taken right on time. He explained everything to me and answered all of my questions. I scheduled follow up appts and am actually looking forward to getting all my work done.
Dr. Bieber is hands down the best dentist that I have ever had. Your appointment is your appointment, you won't show up and wait around for hours like other dental facilities. Dr. Bieber is very knowledgeable, professional, and efficient.
Have been a patient for 15 years. I am very happy and wouldn't considering going anyplace else. He is never overbooked and your wait is very short. Always attentive and willing to answer any questions you have.
My family and I have been seeing Dr. Bieber for over 25 years and would never consider another dentist. Courteous and professional in all respects.
Dr. B is a great dentist, I've been going to him for the past 25+ years. He always welcomes me with a big smile, has a great bedside manner, and is gentle with his care. He runs on time which is very important to me and my busy schedule. I highly recommend him to anyone looking for a dentist who genuinely cares about his patients and delivering the highest quality of care!
I would highly recommend Dr. Bieber. He has been our family dentist for over 15 years! Fantastic dentist, attentive to the patient's needs and provides quality care.
Dr. Bieber has been providing me and my family excellent dental care for over 20 years. Courteous and professional in all respects!
Dr. Bieber has been my dentist since childhood and I highly recommend him. Bruce always greets me with a smile, has great bedside manner, and does professional work.
I'm a fairly new patient and so far I am very happy with his services. Very attentive and his staff are very nice.
Dr. Bieber has been our family dentist for years and it's always been efficient, quality service with a smile. He made great referrals when our kids needed braces and always made time to confer about how they were doing. We've been happy and well taken care of.


In this raw food, superfood, live food, detox, you will initiate the cleansing process in your body and discover how specific foods can increase vitality and energy and prevent and heal disease. Enjoy alkalizing juices, smoothies, and gazpachos prepared in creative, delicious ways and filled with raw, vegan, nutrient-dense foods to ensure that you do not feel deprived.
This cleanse is designed to improve metabolism and digestion, cleanse internal organs, reduce inflammation, increase energy, recalibrate the taste buds, reset the appetite, educate, inspire, and clear the mind. Guided by an experienced health professional within the ashram's supportive and relaxing environment, you will have the opportunity to focus on healing and learning without distractions. You'll also take home practical tips, tools and recipes to implement a healthy lifestyle.
Three detox meals** at 10:00 am, 1:30 pm, and 6:00 pm that include additional pre-yoga healing, herbal elixirs and teas.
Optional but highly encouraged: twice daily Sivananda Yoga classes to compliment the cleansing process.
Twice-daily satsangs for mental detox, inspiration, and community connection.
**All meals are anti-inflammatory and free of wheat, gluten, sugar, dairy, and soy. A complimentary Gracious Living recipe book is included in the cost of the retreat.
Tuition: $425. Add 5 nights accommodation (plan to arrive on or before May 15, 2019 and depart on May 20, 2019 or later).


text:
The trucks ditching diesel and drivers
Most American Cars | Mostly domestics, plus Honda in the top 10
The car with the most American/Canadian content for 2022 is … cue the drumroll … the Lincoln Corsair, in both standard gasoline-fueled and plug-in hybrid guise. Both versions of Lincoln's compact luxury crossover earned a score of 86 — due to 72% of its parts coming from one of the two aforementioned countries — in the American University Kogod Business School's annual "Made in America Auto Index." Last year's leader, the 2021 Ford Mustang GT (when equipped with a manual transmission) fell all the way to 22nd place with a 50% rating due to a switch in transmissions sourced from Mexico. In case you're interested, that puts Ford's red-blooded American ponycar below vehicles like the Kia Sorento, Mercedes-Benz GLE-Class SUV and Lexus ES.
If you're wondering how an American car that's assembled within the borders of the United States could rank below a model from a Korean, German or Japanese automaker, well, we'll let Kogod explain: "The components of the index are based on research performed by the Center for Automotive Research in Ann Arbor Michigan regarding the economic value of different components of auto manufacturing. For example, the highest ranked cars are made by U.S.-based manufacturers using American engines and transmissions, and with a high AALA percentage of U.S. and Canadian parts."
There are 25 total vehicles listed in the Top 10 (there are lots of ties this year). Here's the full list:
There's a whole long list of reasons for the above scores, with seven criteria that include factory location, headquarters location and where its various bits and pieces come from. For more on the rankings, how they compare with prior years and to see the full 37-page list of results, head on over to Kogod Business School's site.
Read Complete Coverage Here
Disclaimer: This story is generated from RSS Feed and has not been created or edited by Waba News. Publisher: Autoblog
Previous articleTom Brady, Bucs rally late to score two touchdowns, beat Saints 17-16
Next articleGoogle Felix Possibly Pixel Fold With 12GB RAM Surfaces on Geekbench
TV & Web Series February 1, 2023
Gemma Collins has shared a very racy video ahead of Valentine's Day where the stunning blonde beauty can be...

redpajama_set_name: RedPajamaCommonCrawl


Employers providing health benefits or workers' compensation packages for their employees have to choose between fully insured and self-insured plans. There are marked differences between the two and and the decision of which option to choose will generally depend on the number of employees, the risks involved, the particular industry being served and previous claims history. There are numerous requirements that vary by state, which may also be contributing factors in determining which option is the most cost-effective.
In a fully insured scenario, the insurance company is the one assuming the risk for paying all claim-related expenses, including the cost of plan administration. As a result, the employer has limited its risks by either paying out only premiums - or premiums plus a predetermined deductible amount. If no or little claims are paid out, the insurance carrier will stand to benefit by increasing the premium profits.
In a self-insured plan, the owner of the plan - which is managed by a hired TPA (Third-Party Administrator) - pays the claim costs himself, instead of the insurance company. As such, the client assumes the risk, but if no or little claims are paid out, the client will stand to benefit by saving any money they would have paid in premiums over the amount their claims cost. Depending on the type of rating, insurance carriers will make various determinations in rating premiums that will allow them to cover projected risk and still have a substantial profit margin.
Broad Coverage Service works with every client to evaluate whether a fully insured or self-insured plan will best meet their needs, based on their specific combination of factors including but not limited to demographics, industry, previous loss history, state guidelines, and number of employees. When a self-insured plan is appropriate, Broad Coverage Service will assist the client in choosing a suitable TPA to manage the plan in the most cost-effective manner and oversee the entire process. When a fully insured plan is required, Broad Coverage Service will work with clients to choose the appropriate carriers and plans that meet their specific needs - all at the lowest price possible.
Please click on the links below to better understand the differences of fully insured and self-insured plans for both group coverage and workers' compensation packages.


Born from a love of long-distance touring, Horizons is a fully dynamic location-based photo gallery displaying adventure photography within the context of its geographical location. Populated with over 50,000 map tiles custom processed from NASA's Blue Marble project and raw LandSAT-7 data, Horizons covers the entire world down to 15m resolution with spatial regions that zoom in even closer.
Above: a fully dynamic search panel reveals different types of photography in Georgian Bay.
Featuring a fully scaleable and dynamic interface, Horizons can take advantage of everything that the largest displays have to offer. Powered by XML, adding photography, maps, and regions is as simple as changing a few lines of text — no modifications to the core Flash movie are necessary, so site updates are near-instantaneous.
Click here to launch Horizons Beta in a new window.
This entry was posted on Thursday, October 27th, 2011 at 2:27 pm.	It is filed under Visual Application Development and tagged with ActionScript 2.0, Adobe Flash 8, XML. You can follow any responses to this entry through the RSS 2.0 feed.


Seeking copyright valuation firms can seem daunting as much of the literature today concerns patent valuation, despite copyright litigation being more prevalent than patent litigation. Copyright valuations are complex as copyrightable items span many forms. Copyrights cover a wide range of forms such as bronze sculptures, books, movies, music, and computer software, to name a few. Microsoft Office, the Harry Potter novel series, Adele's latest album, and the Star Wars film series are all example of copyrightable forms.
Because each type of item brings various nuances to the market, the process for determining copyright value varies with each type of form. At Pellegrino & Associates, we have proven history with copyright valuation. Our experience includes valuing the copyrights associated with the Kurt Vonnegut's work, digital signage software, speech analytics software, and others.
Since the first U.S. Copyright Law passed in 1790, copyright protection has changed significantly, covering many more forms. Today, more than ever, protecting copyrights proves challenging with technological advances that make it simple to infringe copyrights with a click of a button. This means it is more difficult for copyright owners to maintain value of their copyrights, as theft may go undetected. In fact, copyright takedown requests continue to increase annually as Google reported 12.1 million requests in just the first week of 2016.
Copyright law protects the expression of an item, but not the item itself, which patents and trademarks usually protect. Therefore, it may not always be clear to infringers what constitutes infringement. In turn, copyright owners may not always understand what their copyrights actually protect. However, copyright owners can seek a qualified copyright valuation firm that can provide owners with a clear understanding of what their copyrights actually protect.
Does fair use erode value?
Is the work made for hire?
Does the copyright provide notice?
Is the copyright in the public domain?
Is the work covered by the Visual Artists Rights Act of 1990?
We consider historic and prospective data to determine economic life. We spend time assessing the risk for future economic income attributable to the copyright and general market conditions.
Contact us today to learn more about obtaining a copyright valuation and what your copyrights can protect.


Unparalleled service. You'd be crazy to go anywhere else.
Have been a customer of Roberts since he commenced his Tyrepower business in Hastings. A few observations: Robert is one of the most straightforward and honest persons that I have ever done business with. I highly regard his advice in all matters relating to tyres etc. I have never, nor will I question his prices. I have absolute faith in his integrity. He manages a highly efficient business. His staff are always helpful, and will go the extra yard for you. I have held the position of customer service manager in the past. As such I always observe how businesses operate. There are countless businesses that would do well to take a leaf from Robert's example.
Nice to see there are still places around that believe in the old fashioned service.
No matter who serves you at tucketts you always get the hands down best service possible! If anyone needs tyres head in and see the guys!
Rob and the boys do an awesome job and have been very helpful in a bad time. Good old fashion customer service goes along way and tucketts is not in short supply of it!
Great experience today, friendly staff and a quick job done at totally reasonable cost - even came in under quote. Thank you all very much!!
Had an early Christmas present from Tyrepower Hastings today. The friendly staff replaced a faulty tyre quickly and easily and at zero cost. I was back on the road in no time. This was totally unexpected but much appreciated. Wishing a Merry Xmas and happy new year to all the staff. I\u2019ll be back to see you guys when I need a full set of tyres.
Our car had a screw in the tyre so it went flat as a tack. I put the spare on but it had a slow leak. Off to Tucketts Tyrepower for the first time. I had heard they do good service. They repaired the flat, put it on the car. Repaired the spare tyre and put it back in the boot and screwed it down. Now here is the amazing part. It was all done for $35.00! (including GST). My other car needs new tyres. Guess where I'm going? Thanks Tucketts. I hope that you get to read this review!
Fantastic crew, could not be any more friendly or helpful. Glad to have found someone who still takes the time to do a job properly and with care, no matter how big or small the job.
Have been using these guys for over 20 years and would not go anywhere else. Always helpful and do the job properly!
Have to agree with the other reviews. These guys go the extra distance every time. I think it is a family owned business and they really take pride in doing a perfect job. Same price as everyone else so it is a bit of a no brainer to go here.


text:
Log in or register to download
ICAA Record ID
In this review, Maritza Jiménez discusses Variaciones sobre Reticuláreas [Variations on Reticuláreas], the book of poems by Alfredo Silva Estrada, illustrated with five of Gego's drawings. Jiménez reports that the book, designed by Gerd Leufert, will be presented that night at eight o'clock at the Sala Cadafe in Caracas. The review includes comments by both artists on the process of producing this volume of poems. Gego claims that she was unaware of the book's existence until the very last moment. Silva Estrada confirms that and explains that it is a fortuitous, unplanned project, and a spontaneous celebration of Gego's work. In her opinion, the work is not an "illustrated poem," but a joint creative project that respects the autonomy of both artists and enriches them both.
Among the various creative responses to Reticulárea—the work by the German-born Venezuelan artist Gego (Gertrud Goldschmidt, 1912–1994)—one of the most relevant was the long poem by Alfredo Silva Estrada (1933–2009), Variaciones sobre Reticuláreas [Variations on Reticuláreas]. Published to celebrate the tenth anniversary of the work's creation, it is illustrated with five drawings by Gego and designed by the well-known artist and designer Gerd Leufert, Gego's companion. The poet and the artist had worked together once before, in 1964, on a project that also combined their two artistic languages—words and visual arts—in a handmade book of poems by Silva Estrada called Lo nunca proyectado [What is Never Projected] with illustrations by Gego.
Translated into English by Paulette Pagani in 2010, this review is among the documents chosen for the bilingual book Desenredando la red. La Reticulárea de Gego. Una antología de respuestas críticas / Untangling the Web: Gego's Reticulárea, An Anthology of Critical Response, María Elena Huizi and Ester Crespin (organizers)—to be published by The Museum of Fine, Houston, and the Fundación Gego, Caracas.
El Universal (Caracas, Venezuela). -- No. 25.458, May. 7, 1980
Related Works at the MFAH
Gego, Aplique de Reticularea (1969)
Gego, Reticularea (1975)
Gego
Silva Estrada, Alfredo, 1933-2009
Digitized from
Jiménez, Maritza. "Variaciones sobre reticuláreas : una comunión de artistas para celebrar a Gego." El Universal (Caracas, Venezuela), May 7, 1980.
Courtesy of Maritza Jiménez, Caracas, Venezuela
ICAA Team
Fundación Mercantil, Caracas
María Elena Huizi
By downloading or printing this document, you expressly agree that your intended use is private, non-commercial, and educational in nature; that you have reviewed the United States Copyright Office circular on fair use of copyright, located at the website: http://www.copyright.gov/fls/fl102.html; and that you shall indemnify, defend, and hold MFAH and ICAA and their representatives harmless from all claims, allegations, costs, expenses, fees, judgments, liabilities, losses, and damages arising from or relating to your intended use of the downloaded or printed document.
Or cancel the download.


text:
Evaluating the US Programme
A new report looks at the broad impact of the Sutton Trust US Programme on participants, including on their ambitions and outlook.
The report, by the Bridge Group, was commissioned to look at the impact of the programme beyond progression to highly selective US colleges. Through surveys and interviews, the report gives insights into programme participants' experience of studying in the US, the merits of a digitally delivered programme and the benefits of the programme on students who don't go on to study in the US.
The Sutton Trust US Programme, run in conjunction with the US-UK Fulbright Commission, was launched in 2012 to support state school students to explore studying the US. Each year it gives a cohort of young people a taste of what it's like being an international student in the US to see if it could be the right fit for you. Participants who decide to apply to a US university receive support to navigate the application and financial aid process.
Since 2012, the Sutton Trust has supported 1500 students through the US Programme. Of those 514 have gone on to study in the US, benefitting from over $125M in financial aid.
Key findings from today's report include:
Across all cohorts, participants reported a highly positive impact of the programme. They were most likely to say that the programme impacted their broader outlook and ambitions and their understanding of US culture, politics and society.
Programme participants who decided not to apply to US colleges cited a preference for the UK higher education system as a key reason.
Interviewees reported that participation in the programme had a broad positive impact on personal development, international outlook and skill development – regardless of whether they went on to a US or UK university.
Interviewees reported life at US colleges as being tough but rewarding, with many interviewees appreciating the freedoms of a liberal arts education. However, participants reported having to navigate issues of racism and socio-economic inequality on campus; as well as mental health problems.
Participants said that future participants would benefit from more support through the programme after starting their studies. This would help them to navigate some of the challenges they identified.
The findings will inform future delivery of the programme and help to ensure that the programme offers the best possible experience for participants. The Sutton Trust and the Fulbright Commission have already begun offering more support for UK applicants through the Sutton Trust Online platform, developed and delivered bespoke programming on race and mental health, and are exploring further collaboration to support students once in the US through our respective alumni networks. This work will continue over the coming year to address the findings of the report and strengthen the programme as we continue to deliver to new cohorts of young people.
Many thanks to the generosity of donors to the US Programme who have enabled this work and impact.
To see the full report, please click here.
Were 2021's sporting successes also wins for social mobility?
Our Research and Policy Officer Erica Holt-White looks back at this year's sporting successes, and...
Reflecting back on 2021 and looking forward to 2022
Our CEO, James Turner, sets out the Sutton Trust priorities for the new year.
The Sutton Trust submits its representation to the Comprehensive Spending Review
We call for more support for young people in the wake of the pandemic.
If you're a journalist with a question about our work, get in touch with Hilary or Ruby. If it's out of office hours, you can call or text 07917 462 164.
E: [email protected] T: 020 7802 1660
Subscribe to our monthly update


text:
Granny's Flags (2013)
5 min | Documentary, Short, Family
Haja Fatma, a mother to eight children, tells the tale of family life in Tripoli during the Libyan Revolution. Women, young and old, all contributed during these hostile months in their own... See full summary »
Naziha Arebi
Documentary | Short | Family | History | War
02 October 2012 | The Guardian - Film News
Lights, camera, revolution: the birth of Libyan cinema after Gaddafi's fall
Before they starred in Marriage Story and Once Upon a Time in Hollywood, they were up-and-coming stars. Take a look back at the early roles of some of Hollywood's heavy hitters.
Check out the gallery


text:
Brad Pitt surprises graduates, the Met Gala is canceled, Rita Wilson makes new music and more news
All the latest trending news on the coronavirus pandemic in the worlds of entertainment and royalty
By Daniela Galvez
May 19, 2020 10:20 AM EDTUpdated on May 19, 2020 5:44 PM EDT
After initially being postponed, the Met Gala 2020 has been officially canceled. Viewed as the most star-studded fashion event in NYC, the Metropolitan Museum of Art made the announcement on May 19. The exhibition About Time: Fashion and Duration is still set to open on October 29 until February 7, 2021, but fashion enthusiasts will have to wait another year to see Kim Kardashian, her siblings, Jennifer Lopez and many more walk the coveted red carpet.
©GettyImages
JLo and the Kardashian-Jenner ladies are staples at the Met Gala
For many college and high school students, walking across the stage to receive a diploma symbolizes all their hard work has paid off. With the pandemic canceling graduation ceremonies, Brad Pitt is making sure graduates are still proud of their accomplishments. The actor surprised graduates from Missouri State University with a sweet video message posted on the university's social account. "Hi everyone, Brad here from quarantine with a shout out to the graduating class of Missouri State University," Brad says. "It must be very strange doing this in these trying times, but no, we're rooting for you. Our money's on you to make this world a better place. And we wish you all the best in your future endeavors. You did it, you made it! Enjoy, congrats again, and think big!"
We have one more surprise for our #BearGrads: A special message from one of Springfield's own.
Thanks, Brad. pic.twitter.com/tCtWgzhozI
— Missouri State (@MissouriState) May 19, 2020
Cardi B, Bad Bunny and more Latinx stars' words of encouragement for the class of 2020
While most Friends' fans are using the extra time at home to binge watch the infamous sitcom, one super fan got the surprise of a lifestyle when meeting actress Courteney Cox. Thirteen-year-old Naftali had a virtual Friends-themed Bar Mitzvah in Borehamwood, England that was viewed by thousands online. James Corden invited the teen to his late night show and had Cox call into the video chat. Watch the sweet surprise below!
Legally Blonde 3 may soon be hitting the big screens thanks to Mindy Kaling and Dan Goor. The Office actress and Goor will be writing the script for the third installment of the film.
Good news, JLo lovers! If you've ever wanted to own one of Jennifer Lopez's gown, now you can do so. Georges Chakra, the designer behind the singers bright pink dress she wore to the 2018 American Music Awards, is teaming ups with EBay to auction the gown for COVID-19 relief.
Pedro Zamora, founder of MECENAS and President of Zamora Entertainment, the largest Latin entertainment event company in the States, is teaming up with the beloved brand Goya for a city-wide food drive initiative to feed families affected by COVID-19. The food drive and announcement will take place on Wednesday, May 20, 2020 at 11:30 pm at La Boom, Woodside, NY.
On Tuesday, government spokesperson Maria Jesus Montero announced that Spain is looking to extend the country's month-long state of emergency for 14 days to June 7.
It's a sad day in music! Green Day, Fall Out Boy and Weezer will not be performing at their Hella Mega Tour this summer due to safety concerns. The bands revealed dates will be rescheduled for 2021.
BTS member tests for coronavirus, Serena Williams talks mental health and more
JLo's American Music Award dress will be auction for coronavirus relief.
Social distancing did not stop Karol G and the Jonas brother from dropping a fun video for their latest collab, X. Watch the highly-anticipated video here.
Rita Wilson is getting creative during quarantine. The singer told Entertainment Tonight that she has been using the extra time at home to create new music. "In some ways, it's been a very creative time and in some ways, it's been a very reflective time. I've been writing songs almost every day," she said. Rita also revealed that her latest single Where's My Country Song, which was inspired by her mother, was produced while self-isolating. "It really was inspired by my mom who was an amazing mother and she did everything for us," Rita explained. "Music sometimes portrays an idealized version of women in music, and I wanted to shine the spotlight on the women who are maybe just doing their jobs with grace and dignity and perhaps asking, 'Does anybody ever see me? Does anybody want to write a song about me?' And that's really what the inspiration was."
Pedro Martinez and his wife Carolina launched a new PSA to raise awareness for their 'Step Up To The Plate for the DR' campaign to combat COVID-19 in the Dominican Republic. Watch it here.
Coronavirus Daily Updates
Larry King is hospitalized battling COVID-19
Macaulay Culkin surprises fans recreating 'Home Alone' moment
Robert Pattinson has COVID-19, halting The Batman production
Cuomo's emotional goodbye and first Saturday 'off', Nick Cordero's wife sees him for first time and more


All essential information relating to the Tranzfuser 2019 competition (including who can apply!) can be found here.
All applicants must read through the Competition Information before applying to Tranzfuser.
On receipt of your link you must upload your pitch video by noon Friday 26th April 2019.
Before starting your application, we strongly advise you read the guidance provided below.


Dark cherry and vanilla aromatics lead into a palate complimented by flavors of white pepper and cocoa. Silky smooth tannins round out a robust, leathery finish. Whole berry fermented and aged in French oak.


The design concept of Sutherland Elementary School resulted from the collective vision of the school facilities committee that included teachers, students, administrative support staff, and community representatives. The new school took historic clues from the original Dinwiddie Elementary School building, providing a visual link to the community's past while introducing more contemporary details that clearly reflect the path of educational facilities in Dinwiddie. Traditional red brick and stone pilaster detailing was used to tie the new elementary school to the community's favorite elementary school, and other design elements soften the scale of the building. The school site was master planned in coordination with county recreation facilities, ball fields, and other future Dinwiddie County facilities.


text:
How old is Karan Brar?
Karan Brar was born on 18 January 1999.
Karan Brar is 20 years old.
How old is Karan Brar in days now?
Karan Brar is 20 years 11 months 30 days old.
When is the next birthday of Karan Brar?
Karan Brar's next birthday is in 1 day.
What is the zodiac sign of Karan Brar?
Zodiac sign of Karan Brar is Capricorn.
Karan Brar is a popular young actor who became famous and began taking part in various TV and cinema-related projects since his early ages. Born in 1999 in Washington to the parents of Indian origins, Karan grew up in Washington, alongside his elder sister. Since his childhood, he learned to speak Hindu and English. He has been keen on acting and performing on stage since his early ages, and in 2010 he was invited to join the TV project named "Diaries of a Wimpy Kid". It is a series of movies where Brar portrayed Chirag Gupta. He can be also seen in such TV series as "Bunk'd", where he played one of the main roles, "Pass the Plate", "Youth & Consequences", and a few more. Karan Brar is currently living in LA and used to share his flat with his fellow actor, Cameron Boyce, who has recently passed away at a really young age...
Please add your comment...I love your performance in kikiwaka(oh, and I love your sick burns)
Dan Jones 2019-12-20 07:53:36
Love ur wrk


In a couple of weeks A Glamour Affair (hair and makeup) and I will be heading to the gorgeous gulf coast for a destination senior session! I am excited to announce that we have opened up a couple of more dates for the class of 2015!! Contact us above to reserve your spot!


text:
Two patients treated with Novartis Zolgensma gene therapy died due to acute liver injury.
Two children who received a Novartis gene therapy for their neuromuscular disease died following treatment, spotlighting its risks and renewing questions about the safety of genetic medicines like it.
The patients developed acute liver failure between five and six weeks after infusion with the gene therapy, called Zolgensma and approved to treat spinal muscular atrophy, a rare, inherited condition that in its most severe form is often fatal by age two.
While acute liver injury is a known risk of treatment with Zolgensma, these are the first cases that led to patients' deaths, Novartis said in a statement emailed to BioPharma Dive. News of the deaths was first reported by STAT.
The company said it has notified regulators, including the Food and Drug Administration, in all countries where Zolgensma is used, and will inform physicians where allowed by health agencies. Novartis will also update the therapy's labeling to include mention of the deaths, which occurred in Russia and Kazakhstan.
The deaths followed tapering of steroids that are used alongside treatment to manage safety risks, Novartis said.
"While this is important safety information, it is not a new safety signal and we firmly believe in the overall favorable risk/benefit profile of Zolgensma, which to date has been used to treat more than 2,300 patients worldwide across clinical trials, managed access programs, and in the commercial setting," said Novartis in its statement.
Zolgensma was approved in the U.S. in May 2019, becoming just the second gene therapy for an inherited disease cleared by the FDA. It offers dramatic benefits, keeping alive children who otherwise would be expected to die. In clinical testing, treatment also helped patients sit and stand, as well as reach other developmental milestones that typically wouldn't be achieved.
Along with two other drugs from Biogen and Roche, Zolgensma has helped transform the outlook for infants born with spinal muscular atrophy, which is caused by mutations in a key gene and leads to severe muscle weakness. Prior to the three medicines' approval, there were no treatments for the disease.
But, like other gene therapies, Zolgensma comes with safety risks as well as questions about how long its benefits will last.
The risk of liver injury, in particular, is mentioned on the FDA's product labeling, which instructs doctors to assess liver function before infusing Zolgensma and to administer steroids before and after to manage increases in liver enzyme counts.
Two previous cases of acute liver failure have been reported following Zolgensma treatment, but the affected individuals were treated with steroids and continued to make developmental gains months later.
Liver damage is also a broader concern for gene replacement therapy, which involves infusing billions of inactivated viruses loaded with a functional copy of the gene that's missing or mutated in inherited diseases like spinal muscular atrophy. These gene-carrying viruses often end up in the liver, which has raised alarms among researchers about the use of particularly high doses.
In a separate trial testing an Astellas gene therapy for another neuromuscular condition known as X-linked myotubular myopathy, four boys died after developing liver damage following treatment. Elevated liver enzyme counts have also been reported in trials of gene therapies for hemophilia and Duchenne muscular dystrophy.
An FDA meeting last September focused on liver risks with these kinds of gene therapies, but experts on the agency's advisory committee stopped short of recommending research be slowed or redirected.
The two deaths reported by Novartis could further shape discussion of gene therapy safety, as well as how regulators view the balance between a treatment's benefits and risks.
No Comments InADVANCED THERAPY MEDICINAL PRODUCT GENE THERAPY RARE DISEASES


Buy and import Volvo S60 to Kenya from Japan. We are now importing year 2012, 2013, 2014, 2015, 2016, 2017, 2018, and 2019 Volvo S60 to Kenya. Compare Volvo S60 prices, specifications and get a six month warranty on all cars imported to Kenya through us.
Can the 2019 Volvo S60 Take on the Best From Germany?


Track/beach length: 40km+ from the entrance which is more or less the middle it's a 20km beach run north and south.
Lucky Bay Kalbarri, such a fitting name as this area is jaw dropping gorges! Australia should really be called "Lucky Country".
There are some many beautiful places in W.A. alone and Lucky Bay Kalbarri is easily up there!
It's a place where you can still camp legally on the actual beach which is sadly starting to become a unique thing.
Our first ever visit to this place was just after one hell of an adventure to Murchison Off-road park so our trucks were well covered in red dirt.
Coming straight from the outback to the coast was an experience in itself, even just the contrast of the red dirt trucks on the beautiful white sand of Lucky Bay was a site to see!
Lucky Bay Kalbarri is quite a long beach area with plenty of dunes to setup camp behind should the wind be a bit strong, now all beaches are prone to rough swells and at times are not safe to swim in; however with Lucky Bay there is a perfect area where the waters are calm about 90% of the year round.
This is due to a rock and reef running for over 2 kilometres which makes a great place for the kids to swim, throw in a line, kayak, you can name the rest!
Just like Wedge and Grey the area has its fishing & holiday shacks just at the beach entrance, at the shacks are a few big rubbish bins which are more than likely why the beaches are so clean.
The sand can be real soft and if you travel by solo vehicle some recovery boards (i.e. Maxtrax/Treds) can be a real holiday saver, tyre psi of around 15 should be ideal but as always sand can change overnight.
Don't get this confused with Lucky Bay near Esperance; this is Lucky Bay between Geraldton & Kalbarri! Yes we have two Lucky Bays in W.A. and they are both just as awesome but in different ways, (so if you were looking for the other Lucky Bay then click here).
The dunes at Lucky Bay Kalbarri are great for exploring as they are huge in areas and make for great challengers, just make sure you hit the dunes straight on of and down never sideways or on angles.
We had plenty of fun out there and we were just 2kms away from camp most of the time, however it did get very windy out in the dunes but that's pretty normal for the afternoon.
The dune system stretches quite far north from the entrance.
Camping just 30-50 meters from the shoreline is nearly possible for the entire length of the beach; we found a great place which was occupied already however they were just starting to pack up.
This area was surrounded on three sides by dunes and with some clever parking of the 4 Wheel Drives we had perfect wind cover on a very windy day.
Soft sand, moving tides and steep dune systems, take care bring recovery gear and lower the tyres to 15psi as a start. If you are traveling solo don't drive the shore line! It might be a harder surface but you will get caught out somewhere, we pulled out 3 girls who did this exact thing and the waves were starting to lick the vehicle.
Any time other than winter is good. Mid-summer on the hottest days this is the place I'd love to be!
Leave Lucky Bay Kalbarri And Go 4 Wheeling In Western Australia.


98.7FM ESPN New York's The Michael Kay Show Beats WFAN's Afternoon Show During the Winter Ratings Book - ESPN Press Room U.S.
98.7FM ESPN New York's The Michael Kay Show beat WFAN's longtime leader in afternoon drive, Mike's On with Mike Francesa, among men 25-54 from 3-6:30 p.m. ET in the New York market, according to data provided by Nielson Audio. This marks the first time The Michael Kay Show has defeated WFAN's show for a ratings book, scoring a 5.9 share compared to 5.5 for WFAN for the winter ratings book, January 3 – March 27.
98.7FM ESPN New York is the flagship station of ESPN Radio, providing sports talk, news and local and national play-by-play coverage. It's the official radio home of three of the New York market's most iconic teams: New York Knicks, New York Rangers and New York Jets game broadcasts in addition to national rights for the entire NBA season from tip through The Finals, Major League Baseball from Opening Day through the World Series and a slate of top college football including the entire College Football Playoff. 98.7FM ESPN New York is also streamed live at www.ESPNNewYork.com & The ESPN App.