\section{ABC}

Suppose we are giving a formal definition of a programming language in
the style of natural semantics \cite{KAHN87}; after we have specified
the abstract syntax, the type system ($e\hastype \tau$)and a small
step evaluation semantics ($e\mapsto e'$), it is time to check their
consistency via a proof of type soundness. We start by attempting the
\emph{Progress} lemma, which will eventually guarantee that well-typed
expressing cannot go wrong; in symbols, this could go like this: for
every expressions $e$ such that $e\hastype\tau$ and $e$ is
\texttt{not} a value, there exists an expression $e'$ such that
$e\mapsto e'$. Now, imagine that our language is fairly sophisticated
and our funding agency requires a formal verification of our results.
Thus, we decide to use an automated reasoning tool, possibly an
interactive one. A proof of progress is a rather trivial structural
induction for a human, but in order to be machine checked, it needs to
be spelled out in every detail. We have implemented judgments defining
expressions, values, typing and evaluation: but what about the notion
of \emph{not} being a value? We may try to reason in a strictly
intuitionistic way and view $\neg value(e)$ as the derivation of a
contradiction $\perp$ from the assumption $value(e)$. This is
possible, but certainly not in the spirit of the proof; $\neg
value(e)$ is just a test, a way to sift out expressions that are
already fully evaluated.  What we really need is a \emph{positive}
(inductive) definition of ``not being a value'', say $nonvalue(e)$;
indeed, this should be possible, since non-values are exactly those
expressions which are not values.  Nevertheless, manually coding this
notion may be tedious and error-prone, especially considering
evolution of our initial specification. Moreover, we will also have
the obligation of \emph{proving}, at least to our satisfaction, that
the explicit definition of `non-value' coincide with the negation of
`value'. Lacking this, your formal verification cannot be entirely
trusted.



\smallskip
For another example consider a simple instance of reasoning about
process algebra, such as Peterson's algorithm for mutual exclusion
\cite{Peterson81}. The problem is to ensure that two process can never be
simultaneously in their critical section. Process can be in
several (possibly many) states, such as \texttt{sleeping, trying,
  critical}; a transition 
relation describes how the system moves  from a state to another
according to whether a process is allowed to change its status.
Suppose we want to 
verify some property of the system as \emph{safety}: for any
possible sequence of transitions if the initial state is \emph{safe} so is the
final one. Now, from the description of the problem, it is apparent
that a state is safe if both process are \emph{not} in their critical
section.  It would benefit the verification attempt to have a \emph{positive}
explicit specification of being a safe state, rather than working
with an implicit negative one. The number of states can be not only
fairly large, but consider the natural extension of the same problem
to $n$-processes: a hand-written positive
specification of safety can be incomplete or plain wrong. Again, over
time, the number of states will increase or possibly decrease and the
safety specification needs to evolve accordingly.


\smallskip

The bottom line is that negation is a very common connective in a
specification -- and rightly so, since it is one of the most basic
logic operator. Formalizations that use negation are often sharper and
more concise. Nevertheless, not every automated reasoning tool 
avaliable nowadays is able to provide an appropriate handling of this
connective. This is particularly problematic for \emph{logical
  frameworks} with a \lp interpretation such as \emph{Twelf} or
$\l$Prolog. Whole the latter provide a very advanced unified
environment for the specification, implementation and verification of
deductive systems, they inherit the traditional problems with
negation, which Prolog has struggled with since its inception. There
problems are further augmented by some of their more beneficial
features; namely by being `higher-order' and being based on
intuitionistic provability. Those characteristics are the main key
elements of the success of those frameworks and should be preserved
under every extensions. This dissertation presents an approach to
endow those languages with a logically sound notion of negation
without sacrifying any part of their representation power.





