Loading ...
Sorry, an error occurred while loading the content.

Re: "ocaml_beginners"::[] Does OCaml need proofs?

Expand Messages
  • Christopher Conway
    ... You would imagine so, but I ve never heard of any. OCaml is a popular implementation language in the formal methods community, but the source languages are
    Message 1 of 18 , Feb 19, 2009
    • 0 Attachment
      --- In ocaml_beginners@yahoogroups.com, Thomas Hutchinson
      <thomas.hutchinson@...> wrote:
      > I don't know a lot about formal methods, so I'm not sure what tools are
      > out there to prove things about OCaml code (I would imagine that there
      > are a number of projects to do this).

      You would imagine so, but I've never heard of any. OCaml is a popular
      implementation language in the formal methods community, but the
      source languages are usually things like C, Java, and HDL. I'd be
      interested to hear of any tool to check interesting properties on
      OCaml programs. Even a simple lint-like tool would be nice.

      Chris
    • Christopher Conway
      ... theorem-proved to be sure it does what it is intended. ... translates OCaml code into Coq s input or other theorem provers? If you want to prove a theorem
      Message 2 of 18 , Feb 19, 2009
      • 0 Attachment
        --- In ocaml_beginners@yahoogroups.com, silviu andrica
        <silviu_andrica@...> wrote:
        > I was wondering if a program written in OCaml needs to be
        theorem-proved to be sure it does what it is intended.
        > I mean, is there a theorem prover for OCaml, or a tool that
        translates OCaml code into Coq's input or other theorem provers?

        If you want to prove a theorem about the program which is stronger
        than the theorems you get "for free" from the type checker [1] (e.g.,
        termination, race- and deadlock-freedom) then yes, of course you need
        a separate theorem proving tool. I'm not aware of any such tool for
        OCaml programs. (As others have pointed out, Coq goes in the opposite
        direction: proofs to programs, not programs to proofs.)

        Regards,
        Chris

        [1][http://homepages.inf.ed.ac.uk/wadler/papers/free/free.ps Philip
        Wadler. Theorems for free!]
      • Jon Harrop
        ... I d be interested to know what the bugs were... -- Dr Jon Harrop, Flying Frog Consultancy Ltd. http://www.ffconsultancy.com/?e
        Message 3 of 18 , Feb 19, 2009
        • 0 Attachment
          On Thursday 19 February 2009 14:56:41 Richard Jones wrote:
          > There's also a good paper where the authors translated the OCaml
          > stdlib Map module by hand into Coq, proved it, then automatically
          > extracted the code back to OCaml. (And found a bug or two along the
          > way). Unfortunately I can't find that paper right now.

          I'd be interested to know what the bugs were...

          --
          Dr Jon Harrop, Flying Frog Consultancy Ltd.
          http://www.ffconsultancy.com/?e
        • Mehdi Dogguy
          ... Actually, It was in the Set module. The paper can be found here: Functors for Proofs and Programs (J.-C. Filliâtre and P. Letouzey)
          Message 4 of 18 , Feb 19, 2009
          • 0 Attachment
            Richard Jones wrote:
            >
            > There's also a good paper where the authors translated the OCaml
            > stdlib Map module by hand into Coq, proved it, then automatically
            > extracted the code back to OCaml. (And found a bug or two along the
            > way). Unfortunately I can't find that paper right now.
            >

            Actually, It was in the Set module.
            The paper can be found here:

            Functors for Proofs and Programs
            (J.-C. Filliâtre and P. Letouzey)
            http://www.lri.fr/~filliatr/ftp/publis/fpp.ps.gz

            --
            Mehdi Dogguy مهدي الدقي
            http://www.pps.jussieu.fr/~dogguy
            Tel.: (+33).1.44.27.28.38
          • Stefano Zacchiroli
            ... AVL balancing bugs. Basically what they proved (IIRC the author of the proofs was Jean-Christophe Filliatre) is that the previous implementation did not
            Message 5 of 18 , Feb 19, 2009
            • 0 Attachment
              On Thu, Feb 19, 2009 at 03:59:28PM +0000, Jon Harrop wrote:
              > I'd be interested to know what the bugs were...

              AVL balancing bugs. Basically what they proved (IIRC the author of the
              proofs was Jean-Christophe Filliatre) is that the previous
              implementation did not guarantee maximal balancing at any specific
              time in the internal data structure.

              Out of memory, I don't think there is a paper, but more likely a
              contrib entry in the Coq library.

              Cheers.

              --
              Stefano Zacchiroli -o- PhD in Computer Science \ PostDoc @ Univ. Paris 7
              zack@{upsilon.cc,pps.jussieu.fr,debian.org} -<>- http://upsilon.cc/zack/
              Dietro un grande uomo c'è ..| . |. Et ne m'en veux pas si je te tutoie
              sempre uno zaino ...........| ..: |.... Je dis tu à tous ceux que j'aime
            • Jon Harrop
              ... Hmm, it only says two internal functions were producing incorrectly balanced trees but not what the exact mistakes were in the source code... :-( -- Dr
              Message 6 of 18 , Feb 19, 2009
              • 0 Attachment
                On Thursday 19 February 2009 16:01:11 Mehdi Dogguy wrote:
                > Richard Jones wrote:
                > > There's also a good paper where the authors translated the OCaml
                > > stdlib Map module by hand into Coq, proved it, then automatically
                > > extracted the code back to OCaml. (And found a bug or two along the
                > > way). Unfortunately I can't find that paper right now.
                >
                > Actually, It was in the Set module.
                > The paper can be found here:
                >
                > Functors for Proofs and Programs
                > (J.-C. Filliâtre and P. Letouzey)
                > http://www.lri.fr/~filliatr/ftp/publis/fpp.ps.gz

                Hmm, it only says "two internal functions were producing incorrectly balanced
                trees" but not what the exact mistakes were in the source code... :-(

                --
                Dr Jon Harrop, Flying Frog Consultancy Ltd.
                http://www.ffconsultancy.com/?e
              • François Puitg
                ... The Why tool [1], developed by Jean-Christophe Filliâtre, produces « verification conditions » from annotated Ocaml code. Then , it sends them to
                Message 7 of 18 , Feb 19, 2009
                • 0 Attachment
                  De Christopher Conway (19 February, 15:47) :

                  > --- In ocaml_beginners@yahoogroups.com, silviu andrica
                  > <silviu_andrica@...> wrote:
                  > > I was wondering if a program written in OCaml needs to be
                  > theorem-proved to be sure it does what it is intended.
                  > > I mean, is there a theorem prover for OCaml, or a tool that
                  > translates OCaml code into Coq's input or other theorem provers?
                  >
                  > If you want to prove a theorem about the program which is stronger
                  > than the theorems you get "for free" from the type checker [1] (e.g.,
                  > termination, race- and deadlock-freedom) then yes, of course you need
                  > a separate theorem proving tool. I'm not aware of any such tool for
                  > OCaml programs. (As others have pointed out, Coq goes in the opposite
                  > direction: proofs to programs, not programs to proofs.)

                  The Why tool [1], developed by Jean-Christophe Filliâtre, produces «
                  verification conditions » from annotated Ocaml code. Then , it sends
                  them to external provers (Coq, PVS, ...) and decision procedures
                  (Simplify, ...). Most of the time, human interaction is necessary to
                  complete the proofs.

                  [1] http://why.lri.fr/index.en.html


                  >
                  > Regards,
                  > Chris
                  >
                  > [1][http://homepages.inf.ed.ac.uk/wadler/papers/free/free.ps Philip
                  > Wadler. Theorems for free!]
                  >
                  >
                  >
                  >
                  > <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd">
                  > <html>
                  > <head>
                  > </head>
                  >
                  >
                  >
                  >
                  > <body style="background-color: #ffffff;">
                  >
                  > <!--~-|**|PrettyHtmlStartT|**|-~-->
                  > <div id="ygrp-mlmsg" style="width:655px; position:relative;">
                  > <div id="ygrp-msg" style="width: 470px; margin:0; padding:0 25px 0 0; float:left; z-index:1;">
                  > <!--~-|**|PrettyHtmlEndT|**|-~-->
                  >
                  > <div id="ygrp-text">
                  > <p>--- In <a href="mailto:ocaml_beginners%40yahoogroups.com">ocaml_beginners@<wbr>yahoogroups.<wbr>com</a>, silviu andrica<br>
                  > <silviu_andrica@<wbr>...> wrote:<br>
                  > > I was wondering if a program written in OCaml needs to be<br>
                  > theorem-proved to be sure it does what it is intended.<br>
                  > > I mean, is there a theorem prover for OCaml, or a tool that<br>
                  > translates OCaml code into Coq's input or other theorem provers?<br>
                  > <br>
                  > If you want to prove a theorem about the program which is stronger<br>
                  > than the theorems you get "for free" from the type checker [1] (e.g.,<br>
                  > termination, race- and deadlock-freedom) then yes, of course you need<br>
                  > a separate theorem proving tool. I'm not aware of any such tool for<br>
                  > OCaml programs. (As others have pointed out, Coq goes in the opposite<br>
                  > direction: proofs to programs, not programs to proofs.)<br>
                  > <br>
                  > Regards,<br>
                  > Chris<br>
                  > <br>
                  > [1][<a href="http://homepages.inf.ed.ac.uk/wadler/papers/free/free.ps">http://homepages.<wbr>inf.ed.ac.<wbr>uk/wadler/<wbr>papers/free/<wbr>free.ps</a> Philip<br>
                  > Wadler. Theorems for free!]<br>
                  > <br>
                  > </p>
                  >
                  >
                  > </div>
                  >
                  > <!--~-|**|PrettyHtmlStart|**|-~-->
                  > <div width="1" style="color: white; clear: both;"></div>
                  > <!--~-|**|PrettyHtmlEnd|**|-~-->
                  > </body>
                  > <!--~-|**|PrettyHtmlStart|**|-~-->
                  > <head>
                  > <style type="text/css">
                  > <!--
                  > #ygrp-mkp{
                  > border: 1px solid #d8d8d8;
                  > font-family: Arial;
                  > margin: 14px 0px;
                  > padding: 0px 14px;
                  > }
                  > #ygrp-mkp hr{
                  > border: 1px solid #d8d8d8;
                  > }
                  > #ygrp-mkp #hd{
                  > color: #628c2a;
                  > font-size: 85%;
                  > font-weight: bold;
                  > line-height: 122%;
                  > margin: 10px 0px;
                  > }
                  > #ygrp-mkp #ads{
                  > margin-bottom: 10px;
                  > }
                  > #ygrp-mkp .ad{
                  > padding: 0 0;
                  > }
                  > #ygrp-mkp .ad a{
                  > color: #0000ff;
                  > text-decoration: none;
                  > }
                  > -->
                  > </style>
                  > </head>
                  > <head>
                  > <style type="text/css">
                  > <!--
                  > #ygrp-sponsor #ygrp-lc{
                  > font-family: Arial;
                  > }
                  > #ygrp-sponsor #ygrp-lc #hd{
                  > margin: 10px 0px;
                  > font-weight: bold;
                  > font-size: 78%;
                  > line-height: 122%;
                  > }
                  > #ygrp-sponsor #ygrp-lc .ad{
                  > margin-bottom: 10px;
                  > padding: 0 0;
                  > }
                  > -->
                  > </style>
                  > </head>
                  > <head>
                  > <style type="text/css">
                  > <!--
                  > #ygrp-mlmsg {font-size:13px; font-family: arial,helvetica,clean,sans-serif;*font-size:small;*font:x-small;}
                  > #ygrp-mlmsg table {font-size:inherit;font:100%;}
                  > #ygrp-mlmsg select, input, textarea {font:99% arial,helvetica,clean,sans-serif;}
                  > #ygrp-mlmsg pre, code {font:115% monospace;*font-size:100%;}
                  > #ygrp-mlmsg * {line-height:1.22em;}
                  > #ygrp-text{
                  > font-family: Georgia;
                  > }
                  > #ygrp-text p{
                  > margin: 0 0 1em 0;
                  > }
                  >
                  > dd.last p a {
                  > font-family: Verdana;
                  > font-weight: bold;
                  > }
                  >
                  > #ygrp-vitnav{
                  > padding-top: 10px;
                  > font-family: Verdana;
                  > font-size: 77%;
                  > margin: 0;
                  > }
                  > #ygrp-vitnav a{
                  > padding: 0 1px;
                  > }
                  > #ygrp-mlmsg #logo{
                  > padding-bottom: 10px;
                  > }
                  >
                  > #ygrp-reco {
                  > margin-bottom: 20px;
                  > padding: 0px;
                  > }
                  > #ygrp-reco #reco-head {
                  > font-weight: bold;
                  > color: #ff7900;
                  > }
                  >
                  > #reco-category{
                  > font-size: 77%;
                  > }
                  > #reco-desc{
                  > font-size: 77%;
                  > }
                  >
                  > #ygrp-vital a{
                  > text-decoration: none;
                  > }
                  >
                  > #ygrp-vital a:hover{
                  > text-decoration: underline;
                  > }
                  >
                  > #ygrp-sponsor #ov ul{
                  > padding: 0 0 0 8px;
                  > margin: 0;
                  > }
                  > #ygrp-sponsor #ov li{
                  > list-style-type: square;
                  > padding: 6px 0;
                  > font-size: 77%;
                  > }
                  > #ygrp-sponsor #ov li a{
                  > text-decoration: none;
                  > font-size: 130%;
                  > }
                  > #ygrp-sponsor #nc{
                  > background-color: #eee;
                  > margin-bottom: 20px;
                  > padding: 0 8px;
                  > }
                  > #ygrp-sponsor .ad{
                  > padding: 8px 0;
                  > }
                  > #ygrp-sponsor .ad #hd1{
                  > font-family: Arial;
                  > font-weight: bold;
                  > color: #628c2a;
                  > font-size: 100%;
                  > line-height: 122%;
                  > }
                  > #ygrp-sponsor .ad a{
                  > text-decoration: none;
                  > }
                  > #ygrp-sponsor .ad a:hover{
                  > text-decoration: underline;
                  > }
                  > #ygrp-sponsor .ad p{
                  > margin: 0;
                  > }
                  > o{font-size: 0; }
                  > .MsoNormal{
                  > margin: 0 0 0 0;
                  > }
                  > #ygrp-text tt{
                  > font-size: 120%;
                  > }
                  > blockquote{margin: 0 0 0 4px;}
                  > .replbq{margin:4}
                  >
                  > dd.last p span {
                  > margin-right: 10px;
                  > font-family: Verdana;
                  > font-weight: bold;
                  > }
                  >
                  > dd.last p span.yshortcuts {
                  > margin-right: 0;
                  > }
                  >
                  > div.photo-title a,
                  > div.photo-title a:active,
                  > div.photo-title a:hover,
                  > div.photo-title a:visited {
                  > text-decoration: none;
                  > }
                  >
                  > div.file-title a,
                  > div.file-title a:active,
                  > div.file-title a:hover,
                  > div.file-title a:visited {
                  > text-decoration: none;
                  > }
                  >
                  > #ygrp-msg p {
                  > clear: both;
                  > padding: 15px 0 3px 0;
                  > overflow: hidden;
                  > }
                  >
                  > #ygrp-msg p span {
                  > color: #1E66AE;
                  > font-weight: bold;
                  > }
                  >
                  > div#ygrp-mlmsg #ygrp-msg p a span.yshortcuts {
                  > font-family: Verdana;
                  > font-size: 10px;
                  > font-weight: normal;
                  > }
                  >
                  > #ygrp-msg p a {
                  > font-family: Verdana;
                  > font-size: 10px;
                  > }
                  >
                  > #ygrp-mlmsg a {
                  > color: #1E66AE;
                  > }
                  >
                  > div.attach-table div div a {
                  > text-decoration: none;
                  > }
                  >
                  > div.attach-table {
                  > width: 400px;
                  > }
                  >
                  > -->
                  > </style>
                  > </head>
                  > <!--~-|**|PrettyHtmlEnd|**|-~-->
                  > </html><!--End group email -->
                  >
                • Christopher Conway
                  ... (e.g., ... need ... opposite ... I know about Why, and should have mentioned it, but I didn t realize it works on plain-vanilla OCaml code. Is there a tool
                  Message 8 of 18 , Feb 19, 2009
                  • 0 Attachment
                    --- In ocaml_beginners@yahoogroups.com, "François Puitg"
                    <francois.puitg@...> wrote:
                    >
                    > De Christopher Conway (19 February, 15:47) :
                    >
                    > > --- In ocaml_beginners@yahoogroups.com, silviu andrica
                    > > <silviu_andrica@> wrote:
                    > > > I was wondering if a program written in OCaml needs to be
                    > > theorem-proved to be sure it does what it is intended.
                    > > > I mean, is there a theorem prover for OCaml, or a tool that
                    > > translates OCaml code into Coq's input or other theorem provers?
                    > >
                    > > If you want to prove a theorem about the program which is stronger
                    > > than the theorems you get "for free" from the type checker [1]
                    (e.g.,
                    > > termination, race- and deadlock-freedom) then yes, of course you
                    need
                    > > a separate theorem proving tool. I'm not aware of any such tool for
                    > > OCaml programs. (As others have pointed out, Coq goes in the
                    opposite
                    > > direction: proofs to programs, not programs to proofs.)
                    >
                    > The Why tool [1], developed by Jean-Christophe Filliâtre, produces «
                    > verification conditions » from annotated Ocaml code. Then , it sends
                    > them to external provers (Coq, PVS, ...) and decision procedures
                    > (Simplify, ...). Most of the time, human interaction is necessary to
                    > complete the proofs.
                    >
                    > [1] http://why.lri.fr/index.en.html

                    I know about Why, and should have mentioned it, but I didn't realize
                    it works on plain-vanilla OCaml code. Is there a tool that strips Why
                    annotations from the input and produces an OCaml output parsable by
                    ocamlc?

                    Regards,
                    Chris
                  • Johannes Kanig
                    ... This isn t quite right. While Why s syntax is inspired by OCaml s, it really isn t the same language at all. Why doesn t have variant types, objects,
                    Message 9 of 18 , Feb 20, 2009
                    • 0 Attachment
                      On Thu, Feb 19, 2009 at 8:01 PM, Christopher Conway <cconway@...> wrote:
                      > <francois.puitg@...> wrote:
                      >> The Why tool [1], developed by Jean-Christophe Filliâtre, produces «
                      >> verification conditions » from annotated Ocaml code. Then , it sends
                      >> them to external provers (Coq, PVS, ...) and decision procedures
                      >> (Simplify, ...). Most of the time, human interaction is necessary to
                      >> complete the proofs.
                      > I know about Why, and should have mentioned it, but I didn't realize
                      > it works on plain-vanilla OCaml code. Is there a tool that strips Why
                      > annotations from the input and produces an OCaml output parsable by
                      > ocamlc?

                      This isn't quite right. While Why's syntax is inspired by OCaml's, it
                      really isn't the same language at all. Why doesn't have variant types,
                      objects, polymorphic variants, records, modules. It's references are
                      not really first class values. They can't be returned by functions,
                      for example. Also, support for higher-order programs is very limited;
                      you can write them, but not prove them correct.

                      However you can see Why as a (small) subset of OCaml, and there is
                      indeed an option to output OCaml.

                      --
                      Johannes Kanig
                      johannes.kanig@...
                    • Richard Jones
                      ... As you might have gathered I only have a vague memory of this (sets / maps .. whatever!) but IIRC the bugs were fixed. Rich. -- Richard Jones Red Hat
                      Message 10 of 18 , Feb 23, 2009
                      • 0 Attachment
                        On Thu, Feb 19, 2009 at 04:25:57PM +0000, Jon Harrop wrote:
                        > On Thursday 19 February 2009 16:01:11 Mehdi Dogguy wrote:
                        > > Richard Jones wrote:
                        > > > There's also a good paper where the authors translated the OCaml
                        > > > stdlib Map module by hand into Coq, proved it, then automatically
                        > > > extracted the code back to OCaml. (And found a bug or two along the
                        > > > way). Unfortunately I can't find that paper right now.
                        > >
                        > > Actually, It was in the Set module.
                        > > The paper can be found here:
                        > >
                        > > Functors for Proofs and Programs
                        > > (J.-C. Filliâtre and P. Letouzey)
                        > > http://www.lri.fr/~filliatr/ftp/publis/fpp.ps.gz
                        >
                        > Hmm, it only says "two internal functions were producing incorrectly balanced
                        > trees" but not what the exact mistakes were in the source code... :-(

                        As you might have gathered I only have a vague memory of this
                        (sets / maps .. whatever!) but IIRC the bugs were fixed.

                        Rich.

                        --
                        Richard Jones
                        Red Hat
                      • Guillaume Yziquel
                        ... And is there a way to, sort of semi-automatically, get OCaml code, or a subset of the core language, into Coq? All the best, -- Guillaume Yziquel
                        Message 11 of 18 , Feb 23, 2009
                        • 0 Attachment
                          Richard Jones a écrit :
                          > On Thu, Feb 19, 2009 at 04:25:57PM +0000, Jon Harrop wrote:
                          >> On Thursday 19 February 2009 16:01:11 Mehdi Dogguy wrote:
                          >>
                          >>> Richard Jones wrote:
                          >>>> There's also a good paper where the authors translated the OCaml
                          >>>> stdlib Map module by hand into Coq, proved it, then automatically
                          >>>> extracted the code back to OCaml. (And found a bug or two along the
                          >>>> way). Unfortunately I can't find that paper right now.

                          And is there a way to, sort of semi-automatically, get OCaml code, or a
                          subset of the core language, into Coq?

                          All the best,

                          --
                          Guillaume Yziquel
                          http://yziquel.homelinux.org/
                        • Richard Jones
                          ... No. I have only a very shallow understanding of this, but I ll speculate anyway: It wouldn t make sense. You write your Coq proof, and from that can
                          Message 12 of 18 , Feb 23, 2009
                          • 0 Attachment
                            On Mon, Feb 23, 2009 at 07:02:56PM +0100, Guillaume Yziquel wrote:
                            > And is there a way to, sort of semi-automatically, get OCaml code, or a
                            > subset of the core language, into Coq?

                            No.

                            I have only a very shallow understanding of this, but I'll speculate
                            anyway: It wouldn't make sense. You write your Coq proof, and from
                            that can generate working OCaml code, which directly and correctly
                            implements the proof. But to go from random OCaml code to ... what?

                            You're probably better off asking someone on the Coq mailing list.

                            Rich.

                            --
                            Richard Jones
                            Red Hat
                          • Guillaume Yziquel
                            ... I half agree with wour wouldn t make sense statement. The Coq to Ocaml is indeed the cleanest path. However, I was thinking of something more like:
                            Message 13 of 18 , Feb 23, 2009
                            • 0 Attachment
                              Richard Jones a écrit :
                              > On Mon, Feb 23, 2009 at 07:02:56PM +0100, Guillaume Yziquel wrote:
                              >> And is there a way to, sort of semi-automatically, get OCaml code, or a
                              >> subset of the core language, into Coq?
                              >
                              > No.
                              >
                              > I have only a very shallow understanding of this, but I'll speculate
                              > anyway: It wouldn't make sense. You write your Coq proof, and from
                              > that can generate working OCaml code, which directly and correctly
                              > implements the proof. But to go from random OCaml code to ... what?

                              I half agree with wour "wouldn't make sense" statement. The Coq to Ocaml
                              is indeed the cleanest path. However, I was thinking of something more like:

                              http://www.cl.cam.ac.uk/~so294/ocaml/

                              You get the ocaml code "somehow" into Coq, and then you'd be busy
                              painfully proving the operational semantics of your code. Of course,
                              it's not as neat as the purely functional Coq -> Ocaml way.

                              But the whole painful thing is that, well, there's nothing automated in
                              such an import to Coq. I just hoped there was...

                              > You're probably better off asking someone on the Coq mailing list.

                              OK. I will. Thanks.

                              > Rich.

                              --
                              Guillaume Yziquel
                              http://yziquel.homelinux.org/
                            • Mehdi Dogguy
                              ... There is also PAF, which is a Proof Assistant for ML Programs Verification. PAF lets you prove directly you OCaml (or a subset) program. It has been proven
                              Message 14 of 18 , Feb 24, 2009
                              • 0 Attachment
                                Guillaume Yziquel a écrit :
                                >
                                > And is there a way to, sort of semi-automatically, get OCaml code, or a
                                > subset of the core language, into Coq?
                                >

                                There is also PAF, which is a Proof Assistant for ML Programs
                                Verification. PAF lets you prove directly you OCaml (or a subset)
                                program. It has been proven to be coherent (hopefully).

                                You can check this article:

                                http://www.springerlink.com/content/u3xtkcwdnh3jcvux/

                                But, for more updated news, you may contact Séverine Maingaud[1] who
                                works on PAF.

                                [1] http://www.pps.jussieu.fr/~maingaud/

                                Hope this helps,

                                --
                                Mehdi Dogguy مهدي الدقي
                                http://www.pps.jussieu.fr/~dogguy
                                Tel.: (+33).1.44.27.28.38
                              Your message has been successfully submitted and would be delivered to recipients shortly.