\documentclass[a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{url}
%\newcommand{\url}[2]{#2\footnote{#1}}
\title{University Paris Sud (Orsay) site \\ and ENS Lyon subsite}
%\author{C. Paulin}
\date{1/08/2002-31/07/2003}
\newcommand{\coq}{\textsf{Coq}}
\begin{document}
\maketitle
\section{Participants}
The following people participated to the TYPES project in association with
Laboratoire de Recherche en Informatique, UMR 8623, CNRS-Universit\'e
Paris Sud, Orsay.
\begin{description}
\item[Permanent researchers] ~
  \begin{itemize}
  \item Judica\"el Courant
  \item Jean Duprat (ENS Lyon)
  \item Jean-Christophe Filli\^atre
  \item Claude March\'e
  \item Christine Paulin (Site leader)
  \end{itemize}
\item[Post-Doc researchers] ~
  \begin{itemize}
  \item Alexandre Miquel
  \item Benjamin Monate (\'Ecole Polytechnique)
  \item Xavier Urbain
  \end{itemize}
\item[PhD students] ~
  \begin{itemize}
  \item Pierre Corbineau
  \item Pierre Letouzey
  \item Nicolas Oury
  \item Julien Signoles
  \end{itemize}
\end{description}

\section{Results}
\subsection{The Coq proof assistant}

The \coq{} Proof assistant~\cite{CoqProofAssistant,CoqManual03}
 is conjointly developed by the Paris Sud
University and the INRIA Rocquencourt site.  A new version V7.4 integrating
the module system developed by Jacek Chr\k{z}aszcz during his PhD at both 
LRI and Warsaw University was released in February 2003.

\paragraph{\textsf{CoqIde} a Gtk graphical interface for \coq}
B. Monate developed a new interface \textsf{coqide} for the \coq{}
system. This interface is developed in Ocaml using the lablgtk
library. It is integrated with the \coq{} system and provides in
particular a good localization of errors and integration of notations
using unicode characters.


\paragraph{Program extraction}
P. Letouzey~\cite{letouzey2002types} worked on program extraction
in \coq{}. He designed a method to assign simple types which are
approximations of \coq{} types to extracted program. He extended the
extraction mechanism to \coq{} modules and functors which are
extracted towards Ocaml modules or functors. 

At the TLCA'03 international conference, 
N. Oury~\cite{oury03} presented his work on a generic scheme to
substitute efficient data-structures within programs extracted from
\coq{} proofs, while preserving both the correctness of the extraction
process and the computational behavior of data structures on the
\coq{} side.

\paragraph{Automation of proofs}
J. Courant and P. Corbineau worked on proof automation in
\textsf{Coq}. P. Corbineau designed the new tactic \texttt{Ground} which
extends the decision procedure for intuitionistic propositional
calculus to solve some first-order problems. He also integrated his
tactic \texttt{CC} for congruence closure to the \coq{} system.


\subsection{Developments}

\paragraph{Finite sets library}
P. Letouzey and J.-C. Filli\^atre formalized in the \coq{}
proof assistant a finite sets library%
\footnote{see \url{http://www.lri.fr/~filliatr/fsets/}}. 
It actually contains three
different implementations of finite sets: using ordered lists,
red-black trees and AVLs. This formalization makes a heavy use of  modules and
functors, a novelty in \coq{} 7.4, thus demonstrating their power in the
context of proof, as well as in the context of programming. These
developments are available as \coq{} contributions.

\paragraph{Vectors} J. Duprat developed a theory of bit-vectors 
with their interpretation as numeric values in order to modelize
types of bounded integers in programming languages. It is integrated
to the standard \coq{} theories.

\paragraph{Timed automata}
A new version of a theory of timed automata using the functor system
of \coq{} V7.4 has been designed by C. Paulin and is used in the Calife
tool\footnote{\url{http://www.loria.fr/projets/calife/}}, an
environment for formal proofs and tests of algorithms used in
telecommunication which uses both proof assistants and model-checkers.
These developments are available as \coq{} contributions.

\subsection{Proof of programs}
\paragraph{Why}
Jean-Christophe Filli{\^a}tre continued the development of the 
\textsf{Why} tool~\cite{why} to certify
imperative programs using proof assistants \coq{}, \textsf{PVS} or
\textsf{HOL Light}.
He extended the tool with an output for the 
\textsf{haRVey}\footnote{\url{http://www.loria.fr/~ranise/haRVey/}} 
decision procedure which
was able to discharge automatically proof obligations for the heapsort
algorithm. 

Another extension is the possibility to use a large subset of \textsf{C}
programs as input for the \textsf{Why} tool.  The \textsf{Why} tool
has been presented at the TYPES'2003 meeting. The theoretical
background appeared in~\cite{Filliatre00a}.

\paragraph{Krakatoa}
E. Contejean, J. Duprat, J.-C. Filli\^atre, C. March{\'e}, X. Urbain
and C. Paulin are working on the \textsf{Krakatoa} project for 
modelization, specification and proof of Java(Card) programs in \coq{}.


A tool \textsf{Krakatoa}~\cite{krakatoa02} has been developed. 
It takes Java(Card) programs, annotated with JML specifications as input
and produces \coq{} theories and \textsf{Why} programs from which
proof obligations are 
automatically generated. This work is described
in~\cite{marche03jlap}. It has been developed as part of the
VERIFICARD\footnote{\url{http://www.verificard.org}} project.

\subsection{Meta-theory}
The work of A. Miquel together with Benjamin Werner from INRIA
site on proof irrelevance model of the Calculus of
Constructions has been published in~\cite{miquel03types}.

A. Miquel proposed a method for realising the proofs of
Intuitionistic Zermelo-Fraenkel set theory (IZF) by strongly
normalizing lambda-terms. This method relies on the introduction of a
Curry-style type theory extended with specific subtyping principles,
which is then used as a low-level language to interpret IZF via a
representation of sets as pointed graphs inspired by Aczel's hyperset
theory. As a consequence, this work refines a classical result of
Myhill and Friedman by showing how a strongly normalizing lambda-term
that computes a function of type $N\rightarrow N$ can be extracted
from the proof of its existence in IZF.  This work is published
in~\cite{miquel03csl}.

\subsection{Modules}
J. Signoles applied general results on modules in Pure Type Systems to
design a tool,
\textsf{ocamldefun}\footnote{\url{http://www.lri.fr/~signoles/ocamldefun/}},
which unfolds functor applications in Objective Caml programs. This
work is described in~\cite{signoles03jfla}.

\section{Collaborations}
\paragraph{Math in \coq}
Orsay collaborates with the Nijmegen site in the domain of development
of mathematical theories in \coq{}. Orsay organized a first meeting on
december 18th and a two days workshop on April 23rd and 24th.
This workshop\footnote{\url{http://www.lri.fr/~paulin/MathinCoq/}}
included nine presentations from researchers of Bologna, INRIA
Sophia-Antipolis, Nijmegen, Orsay, Trusted Logic\ldots \\
A mailing
list\footnote{\url{http://coq.inria.fr/mailman/listinfo/mathincoq}}
  has been created for this specialized subject.  P. Letouzey from
  Orsay collaborates with L. Cruz-Filipe, B. Spitters and F.  Wiedijk
  from Nijmegen
  in order to improve efficiency of programs extracted from the proof
  of the Fundamental Theorem of Algebra (FTA).\\
J.-C. Filli\^atre modified 
the \texttt{coqdoc} documentation
tool\footnote{\url{http://www.lri.fr/~filliatr/coqdoc}} in order to
fulfill the requirements of presentation of the FTA development.

\paragraph{Geometry}
J. Duprat organized at ENS Lyon a one-day workshop (June 11th) 
on Geometry and Proof on Computer.

\paragraph{}

Orsay and Lyon sites have strong interactions with the INRIA sites in
Rocquencourt (now at INRIA Futurs) and Sophia-Antipolis. They
participate together to common seminar and one-day workshops.

Orsay collaborates with the industrial site France Telecom R\&D on
proof environments for the development of critical algorithms in
Telecommunication applications. 

C. Paulin visited University of Warsaw
for Daria Walukiewicz's PhD defense in April 2003.

A. Miquel joined the Orsay group for one year (2002-2003) 
after his thesis
at INRIA Rocquencourt and a one year post-doc at Chalmers University.

%\bibliographystyle{plain}
%\input{biblio-demons}

\begin{thebibliography}{10}

\bibitem{CoqProofAssistant}
{The Coq Proof Assistant}.
\newblock \url{http://coq.inria.fr/}.

\bibitem{CoqManual03}
{Coq} development team.
\newblock {\em {The Coq Proof Assistant Reference Manual -- Version V7.4}},
  February 2003.
\newblock \url{http://coq.inria.fr/doc/main.html}.

\bibitem{Filliatre99}
J.-C. Filli{\^a}tre.
\newblock {\em {Preuve de programmes imp{\'e}ratifs en th{\'e}orie des types}}.
\newblock Th{\`e}se de doctorat, Universit{\'e} Paris-Sud, July 1999.

\bibitem{Filliatre00a}
J.-C. Filli{\^a}tre.
\newblock {Verification of Non-Functional Programs using Interpretations in
  Type Theory}.
\newblock {\em Journal of Functional Programming}, 13(4):709--745, July 2003.
\newblock [English translation of \cite{Filliatre99}].

\bibitem{why}
Jean-Christophe Filli{\^a}tre.
\newblock The {Why} certification tool.
\newblock \url{http://why.lri.fr/}.

\bibitem{types02}
Herman Geuvers and Freek Wiedijk, editors.
\newblock {\em Types for Proofs and Programs Second International Workshop,
  TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected
  Papers}, volume 2646 of {\em Lecture Notes in Computer Science}. Springer,
  2003.

\bibitem{letouzey2002types}
Pierre Letouzey.
\newblock A new extraction for {Coq}.
\newblock In Geuvers and Wiedijk \cite{types02}.

\bibitem{krakatoa02}
Claude March\'e, Christine Paulin, and Xavier Urbain.
\newblock The \textsc{Krakatoa} proof tool, 2002.
\newblock \url{http://krakatoa.lri.fr/}.

\bibitem{marche03jlap}
Claude March{\'e}, Christine Paulin-Mohring, and Xavier Urbain.
\newblock The \textsc{Krakatoa} tool for certification of
  \textsc{Java/JavaCard} programs annotated in \textsc{JML}.
\newblock {\em Journal of Logic and Algebraic Programming}, 2003.
\newblock To appear.

\bibitem{miquel03csl}
Alexandre Miquel.
\newblock A strongly normalising {Curry-Howard} correspondence for {IZF} set
  theory.
\newblock In {\em Computer Science Logic, CSL'03}, Lecture Notes in Computer
  Science. {Sprin\-ger-Verlag}, 2003.

\bibitem{miquel03types}
Alexandre Miquel and Benjamin Werner.
\newblock The not so simple proof-irrelevant model of {CC}.
\newblock In Geuvers and Wiedijk \cite{types02}, pages 240--258.

\bibitem{oury03}
Nicolas Oury.
\newblock Observational equivalence and program extraction in the {Coq Proof
  Assistant}.
\newblock In Martin Hofmann, editor, {\em TLCA}, volume 2701 of {\em Lecture
  Notes in Computer Science}, pages 271--285. Springer, 2003.

\bibitem{signoles03jfla}
Julien Signoles.
\newblock Calcul statique des applications de modules paramétrés.
\newblock In {\em Journées Francophones des Langages Applicatifs}, 2003.

\end{thebibliography}

\end{document}


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 
