\subsection{Contributions and technical acknowledgments}

The original contribution of the thesis are:
\bit

\item
a complement algorithm for \ho patterns internalized into a relevant 
theory of simple types
\item
a practical treatment of negation for second-order hereditary harrop formulae
\enit

Excusatio non petita: Though the topics addressed are maybe not too 
deep and somehow not general enough, they required an extensive 
knowledge and expertise in several fields as negation in \lp and type 
theories that are pretty difficult to manage for their sheer size.  We 
contend that our approach is the first one to give a realistic 
analysis of negation in logical frameworks with an emphasis to the 
development of a practical tool to incorporate this operator in 
existing languages.

This work has benefited enormously from the large ensemble of 
research collected in the Elf and offspring projects: not only form 
the existence of the Elf language and environment, but also from 
specific contributions which we have imported (and somehow 
trivialized) in this thesis.  Let me mention only the most recent 
ones: linear unification (Cervesato and Pfenning), subordination 
(Virga), mode and termination analysis (Rohwedder and Pfenning), 
induction schemata and splitting (Schurmann and Pfenning).

Finally I want to point out that Frank Pfenning orginally suggested, 
among others, the ideas of using relevant types for variables 
occurences and of augmentation by disequalities.
