[Caml-list] Call for Papers: PLPV 2010

[Jean-Christophe Filliâtre]

   Call For Papers

 Programming Languages meets Program Verification (PLPV) 2010

  http://slang.soe.ucsc.edu/plpv10/

  Tuesday, January 19, 2010
Madrid, Spain
  Affiliated with POPL 2010


Overview: The goal of PLPV is to foster and stimulate research at the
intersection of programming languages and program verification. Work
in this area typically attempts to reduce the burden of program
verification by taking advantage of particular semantic and/or
structural properties of the programming language. One example is
dependently typed programming languages, which leverage a language's
type system to specify and check richer than usual specifications,
possibly with programmer-provided proof terms. Another example is
extended static checking systems like Spec#, which extends C# with
pre- and postconditions along with a static verifier for these
contracts.

We invite submissions on all aspects, both theoretical and practical,
of the integration of programming language and program verification
technology. To encourage cross-pollination between different
communities, we seek a broad the scope for PLPV.  In particular,
submissions may have diverse foundations for verification (type-based,
Hoare-logic-based, etc), target diverse kinds of programming languages
(functional, imperative, object-oriented, etc), and apply to diverse
kinds of program properties (data structure invariants, security
properties, temporal protocols, etc).

Submissions: Submissions should fall into one of the following three
categories:

   1. Regular research papers that describe new work on the above or
  related topics. Submissions in this category have an upper limit
  of 12 pages, but shorter submissions are also encouraged.

   2. Work-in-progress reports should describe new work that is
  ongoing and may not be fully completed or evaluated. Submissions
  in this category should be at most 6 pages in total length.

   3. Proposals for challenge problems which the author believes is
  are useful benchmarks or important domains for language-based
  program verification techniques.  Submissions in this category
  should be at most 6 pages in total length.

Submissions should be prepared with SIGPLAN two-column conference
format. Submitted papers must adhere to the SIGPLAN republication
policy. Concurrent submissions to other workshops, conferences,
journals, or similar forums of publication are not allowed.

Publication: Accepted papers will be published by the ACM and appear
in the ACM digital library.

Student Attendees: Students with accepted papers or posters are
encouraged to apply for a SIGPLAN PAC grant that will help to cover
travel expenses to PLPV. Details on the PAC program and the
application can be found on the workshop web page. PAC also offers
support for companion travel.

Important Dates:

* Electronic submission: October 8, 2009, 11:59pm Samoa time (UTC-11)
* Notification: November 8, 2009
* Final version: November 17, 2009
* Workshop: January 19, 2010

Organizers:

* Cormac Flanagan (University of California, Santa Cruz)
* Jean-Christophe Filliâtre (CNRS)

Program Committee:

* Adam Chlipala (Harvard University)
* Ranjit Jhala (University of California, San Diego)
* Joseph Kiniry (University College Dublin)
* Rustan Leino (Microsoft Research)
* Xavier Leroy (INRIA Paris-Rocquencourt)
* Conor McBride (University of Strathclyde)
* Andrey Rybalchenko (Max Planck Institute for Software Systems)
* Tim Sheard (Portland State University)
* Stephanie Weirich (University of Pennsylvania)

___
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

Re: [Caml-list] how to use c wrapper files in libraries

[Erik de Castro Lopo]

Aaron Bohannon wrote:

> I am trying to use the wrapper for libsndfile contributed by Erik de
> Castro Lopo (http://caml.inria.fr/cgi-bin/hump.en.cgi?contrib=556).
> The wrapper code compiles just fine.

Oh wow, I never realised that made it into the Hump.

I did the wrapper as part of an experiement which I never followed
through on.

If you or anyone else is interested in maintaining it, please do
so.

Cheers,
Erik
-- 
--
Erik de Castro Lopo
http://www.mega-nerd.com/

___
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

Re: [Caml-list] how to use c wrapper files in libraries

[Aaron Bohannon]

Thank you.  This does clarify some things.  Everything works like
clockwork after reworking things this way.

Based on the output of "ocamlc -verbose", it seems that if you pass
"file.o" file to "ocamlc -a", it does nothing except remember the name
"file.o" and pass it to gcc when the OCaml library is later used,
which is a pretty useless and confusing behavior---in general, you
will not be in the same directory that contains "file.o" when you use
the OCaml library and I don't know of any gcc options that will make
gcc look in other directories for object files.  It would seem better
for "ocamlc -a" to ignore ".o" files and display an appropriate
warning.

 - Aaron

On Mon, Jul 20, 2009 at 10:58 AM,  wrote:
> I am not familiar with this specific library.
> In the general approach, you compile your c code, and package it into a 
> library, let's say libA.a
>
> Then while building your sndfile.cma, you should pass the option
> ocamlc -a -o sndfile.cma -cclib -lA ...
>
> A caml executable linked with your library will have also libA.a passed in 
> the linking phase.
>
> Using ocamlc -verbose could give you a hint to which files are missing.
>
> Hope this helps,
>
> Rabih
>
> -Message d'origine-
> De : caml-list-boun...@yquem.inria.fr 
> [mailto:caml-list-boun...@yquem.inria.fr] De la part de Aaron Bohannon
> Envoyé : lundi 20 juillet 2009 16:28
> À : caml-list@yquem.inria.fr
> Objet : [Caml-list] how to use c wrapper files in libraries
>
> Hello,
>
> I am trying to use the wrapper for libsndfile contributed by Erik de
> Castro Lopo (http://caml.inria.fr/cgi-bin/hump.en.cgi?contrib=556).
> The wrapper code compiles just fine.  And the tests that use the OCaml
> library it builds work just fine.  However, I am having a frustrating
> compile-time error when I try to compile my program in a different
> directory.
>
> The wrapper code is being packaged into an OCaml library using the
> following command:
>
> ocamlc -a -o sndfile.cma -custom sndfile_stub.o sndfile.cmo \
>  -ccopt -L/usr/local/lib -cclib -lsndfile
>
> Within the same directory, the test program can be successfully compiled with:
>
> ocamlc -o test_sndfile sndfile.cma test_sndfile.ml
>
> Within a different directory, I used:
>
> ocamlc -o mytest -I /path/to/libsndfile-ocaml/files/   sndfile.cma   mytest.ml
>
> And I get:
>
> powerpc-apple-darwin8-gcc-4.0.1: sndfile_stub.o: No such file or directory
> Error while building custom runtime system
>
> I have tried setting every path-related option I could find, and
> nothing helped.  I tried reading everything I could find about
> compiling and using c wrappers for OCaml, but there is a severe lack
> of documentation on the topic.  In particular, I could find no example
> of a c object file being given as an argument to an "ocamlc -a"
> command, so I am not sure what that is supposed to do, which makes it
> impossible for me to understand this error message.
>
> I am using OCaml 3.10.1 on OS X 10.4.  Any help would be appreciated.
>
>  - Aaron
>
> ___
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
> This message and any attachments (the "message") are confidential, intended 
> solely for the addressee(s), and may contain legally privileged information.
> Any unauthorised use or dissemination is prohibited.
> E-mails are susceptible to alteration.
> Neither Societe Generale Asset Management nor any of its subsidiaries or 
> affiliates shall be liable for the message if altered, changed or falsified.
>
> Find out more about Societe Generale Asset Management's proposal on 
> www.sgam.com
>
>                                
>
> Ce message et toutes les pieces jointes (ci-apres le "message") sont 
> confidentiels et susceptibles de contenir des informations couvertes par le 
> secret professionnel.
> Ce message est etabli a l'intention exclusive de ses destinataires.
> Toute utilisation ou diffusion non autorisee est interdite.
> Tout message electronique est susceptible d'alteration. Societe Generale 
> Asset Management et ses filiales declinent toute responsabilite au titre de 
> ce message s'il a ete altere, deforme ou falsifie.
>
> Decouvrez l'offre et les services de Societe Generale Asset Management sur le 
> site www.sgam.fr
>
>

___
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

RE: [Caml-list] how to use c wrapper files in libraries

[RABIH.ELCHAAR]

I am not familiar with this specific library.
In the general approach, you compile your c code, and package it into a 
library, let's say libA.a

Then while building your sndfile.cma, you should pass the option
ocamlc -a -o sndfile.cma -cclib -lA ...

A caml executable linked with your library will have also libA.a passed in the 
linking phase.

Using ocamlc -verbose could give you a hint to which files are missing.

Hope this helps,

Rabih

-Message d'origine-
De : caml-list-boun...@yquem.inria.fr [mailto:caml-list-boun...@yquem.inria.fr] 
De la part de Aaron Bohannon
Envoyé : lundi 20 juillet 2009 16:28
À : caml-list@yquem.inria.fr
Objet : [Caml-list] how to use c wrapper files in libraries

Hello,

I am trying to use the wrapper for libsndfile contributed by Erik de
Castro Lopo (http://caml.inria.fr/cgi-bin/hump.en.cgi?contrib=556).
The wrapper code compiles just fine.  And the tests that use the OCaml
library it builds work just fine.  However, I am having a frustrating
compile-time error when I try to compile my program in a different
directory.

The wrapper code is being packaged into an OCaml library using the
following command:

ocamlc -a -o sndfile.cma -custom sndfile_stub.o sndfile.cmo \
  -ccopt -L/usr/local/lib -cclib -lsndfile

Within the same directory, the test program can be successfully compiled with:

ocamlc -o test_sndfile sndfile.cma test_sndfile.ml

Within a different directory, I used:

ocamlc -o mytest -I /path/to/libsndfile-ocaml/files/   sndfile.cma   mytest.ml

And I get:

powerpc-apple-darwin8-gcc-4.0.1: sndfile_stub.o: No such file or directory
Error while building custom runtime system

I have tried setting every path-related option I could find, and
nothing helped.  I tried reading everything I could find about
compiling and using c wrappers for OCaml, but there is a severe lack
of documentation on the topic.  In particular, I could find no example
of a c object file being given as an argument to an "ocamlc -a"
command, so I am not sure what that is supposed to do, which makes it
impossible for me to understand this error message.

I am using OCaml 3.10.1 on OS X 10.4.  Any help would be appreciated.

 - Aaron

___
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
This message and any attachments (the "message") are confidential, intended 
solely for the addressee(s), and may contain legally privileged information. 
Any unauthorised use or dissemination is prohibited. 
E-mails are susceptible to alteration. 
Neither Societe Generale Asset Management nor any of its subsidiaries or 
affiliates shall be liable for the message if altered, changed or falsified. 
  
Find out more about Societe Generale Asset Management's proposal on www.sgam.com
  
 
  
Ce message et toutes les pieces jointes (ci-apres le "message") sont 
confidentiels et susceptibles de contenir des informations couvertes par le 
secret professionnel.
Ce message est etabli a l'intention exclusive de ses destinataires.
Toute utilisation ou diffusion non autorisee est interdite. 
Tout message electronique est susceptible d'alteration. Societe Generale Asset 
Management et ses filiales declinent toute responsabilite au titre de ce 
message s'il a ete altere, deforme ou falsifie. 

Decouvrez l'offre et les services de Societe Generale Asset Management sur le 
site www.sgam.fr

___
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Caml-list] how to use c wrapper files in libraries

[Aaron Bohannon]

Hello,

I am trying to use the wrapper for libsndfile contributed by Erik de
Castro Lopo (http://caml.inria.fr/cgi-bin/hump.en.cgi?contrib=556).
The wrapper code compiles just fine.  And the tests that use the OCaml
library it builds work just fine.  However, I am having a frustrating
compile-time error when I try to compile my program in a different
directory.

The wrapper code is being packaged into an OCaml library using the
following command:

ocamlc -a -o sndfile.cma -custom sndfile_stub.o sndfile.cmo \
  -ccopt -L/usr/local/lib -cclib -lsndfile

Within the same directory, the test program can be successfully compiled with:

ocamlc -o test_sndfile sndfile.cma test_sndfile.ml

Within a different directory, I used:

ocamlc -o mytest -I /path/to/libsndfile-ocaml/files/   sndfile.cma   mytest.ml

And I get:

powerpc-apple-darwin8-gcc-4.0.1: sndfile_stub.o: No such file or directory
Error while building custom runtime system

I have tried setting every path-related option I could find, and
nothing helped.  I tried reading everything I could find about
compiling and using c wrappers for OCaml, but there is a severe lack
of documentation on the topic.  In particular, I could find no example
of a c object file being given as an argument to an "ocamlc -a"
command, so I am not sure what that is supposed to do, which makes it
impossible for me to understand this error message.

I am using OCaml 3.10.1 on OS X 10.4.  Any help would be appreciated.

 - Aaron

___
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

Re: [Caml-list] Caml Light 0.8 and -fstrict-aliasing build issue

[Alexis ROBERT]

philippe esperet a écrit :

francois.bois...@prepas.org 
%
/dosc/esperet/tex/email/@ocaml9.tex lun. juil. 20 2009 15:01:49

% As the MPSI programme force us to use Caml Light instead of OCaml (our
% teachers hit us each time we pronounce ocaml :) ), I tried to build
% the sources on my computer, but during the build, I got this :

We use Ocaml in henri IV for three years, nevertheless I try for fun
to keep the old camllight each time I change my linux config. At home,
on a 64 bits platform:

camllight_0.80_amd64.deb from the guru François Boisson
makes the trick with something like (suse 11.1)

dpkg-deb -x camllight_0.80_amd64.deb /
At Fenelon, my teachers tell us they don't want us to have problems with 
examiners who are not familiar with OCaml, but we can use it if we want, 
even if everything is under Caml Light there.


Thanks for the trick, I was used to manually uncompress it with ar x and 
then untar data.tar.gz in / :)


I've looked into the strings of the binaries bundled in the package and 
it shows "GCC: (GNU) 3.4.6 (Ubuntu 3.4.6-8ubuntu2)", and 
-fstrict-aliasing seems disabled in GCC 3.4.


The strange thing is that even if gcc-3.4 is in build-dep of the 
dpkg-source package, I don't see where it uses it in debian/rules or any 
Makefile (and debuild fails at building the package, it doesn't execute 
the build step of rules for a reason I don't understand, but if I 
manually launch the step, I get the same error).


Thanks

Alexis

___
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

Re: [Caml-list] book "Le langage Caml"

[blue storm]

On Mon, Jul 20, 2009 at 11:06 AM, Xavier Leroy wrote:
> A few months ago, there was a discussion on this list about
> "Le langage Caml", an early book on Caml (Light) programming written
> by Pierre Weis and I.  The book was out of print, but the publisher,
> Dunod Éditions, graciously agreed to relinquish its rights and give
> them back to the authors.
>
> Pierre and I are therefore happy to announce that the full text of the
> book (2nd edition) is now available freely:
>
>   http://caml.inria.fr/pub/distrib/books/llc.pdf
>
> There was a companion book, "Manuel de référence du langage Caml",
> which is the French translation of the Caml Light 0.7 reference
> manual.  For completeness, we also made it available:
>
>  http://caml.inria.fr/pub/distrib/books/manuel-cl.pdf
>
> Both texts are distributed under the Creative Commons BY-NC-SA
> license.
>
> Enjoy,
>
> - Xavier Leroy

That's great. This book is still, in my opinion, the best introduction
to Caml for programming beginners.

When we discussed the matter a few months ago [1], there was an
interest in an english translation, or an update to Objective Caml. A
translation would be a huge undertaking, but I suspect that updating
the book to Objective Caml should not be so difficult, and I would be
happy to collaborate to such an effort.

Is there a possibility to get the document in an editable format ?

[1] archive : 
http://groups.google.com/group/fa.caml/browse_thread/thread/acbd0dfaec8f1e8e/8884d70558fa8ea2?lnk=gst&q=LLC+book#8884d70558fa8ea2

___
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

Re: [Caml-list] Caml Light 0.8 and -fstrict-aliasing build issue

[philippe esperet]

francois.bois...@prepas.org
%
/dosc/esperet/tex/email/@ocaml9.tex lun. juil. 20 2009 15:01:49

% As the MPSI programme force us to use Caml Light instead of OCaml (our
% teachers hit us each time we pronounce ocaml :) ), I tried to build
% the sources on my computer, but during the build, I got this :

We use Ocaml in henri IV for three years, nevertheless I try for fun
to keep the old camllight each time I change my linux config. At home,
on a 64 bits platform:

camllight_0.80_amd64.deb from the guru François Boisson
makes the trick with something like (suse 11.1)

dpkg-deb -x camllight_0.80_amd64.deb /

I guess François has built a camlllight package for everyone.
(http://boisson.homeip.net)

Regards


-- 
philippe.espe...@gmail.com
___
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Caml-list] Caml Light 0.8 and -fstrict-aliasing build issue

[Alexis ROBERT]

Hello,

As the MPSI programme force us to use Caml Light instead of OCaml (our 
teachers hit us each time we pronounce ocaml :) ), I tried to build the 
sources on my computer, but during the build, I got this :


make[1]: Entering directory `/home/alexis/camllight/src/lib'
../camlrun ../camlcomp -stdlib . -O none -g -W string.mli
make[1]: *** [string.zi] Segmentation fault

More precisely, gdb told me that :

(gdb) run ../camlcomp -stdlib . -O none -g -W string.mli
Starting program: /home/alexis/camllight/src/camlrun ../camlcomp -stdlib 
. -O none -g -W arg.mli


Program received signal SIGSEGV, Segmentation fault.
interprete (prog=0xe0e960 "\006\016") at interp.c:508
508  cur_instr = *pc++; <= In the real source code, that's Next; 
I changed it with the macro content for more lisibility :)

(gdb) info locals
pc = (code_t) 0x9 
cur_instr = 
[...]

The reason of the segfaults seems to be linked with -fstrict-aliasing 
(included in -O2, I discovered it when disabling gcc optimizations to 
get cur_instr value). In fact, the weird thing is that pc pointer 
suddently decreases to 0x09, which doesn't seem to be a very sweet 
memory address, and causes a segfault in the Next macro when it 
deferences pc.


I've tried to follow pc using a watchpoint before the magic change, but 
it disables the watchpoint every time it reaches a segment of code where 
pc is not defined which makes the debugging process *very* annoying :)


A workaround would be to use OPTS="-fno-strict-aliasing" in 
runtime/Makefile line 5, but I don't know if it's very clean (or to 
disable direct jumping but that's even worse :D ).


My computer is running Ubuntu 9.04 with gcc 4.3.3 and a x86_64 cpu (I 
used the CVS version of caml light). It _MAY_ be a x86_64 only issue as 
I vaguely remember a friend having the same configuration as mine using 
Ubuntu x86 who has successfully built caml light, but I may have forgot 
some details.


Thanks !

Alexis ROBERT

___
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

Re: [Caml-list] book "Le langage Caml"

[Gregory BELLIER]

Wonderful announcement !

This is a good news ! Thank you Dunod Éditions.
I guess those links will be easily accessible from the website from now on.

Grégory.


Xavier Leroy a écrit :

A few months ago, there was a discussion on this list about
"Le langage Caml", an early book on Caml (Light) programming written
by Pierre Weis and I.  The book was out of print, but the publisher,
Dunod Éditions, graciously agreed to relinquish its rights and give
them back to the authors.

Pierre and I are therefore happy to announce that the full text of the
book (2nd edition) is now available freely:

   http://caml.inria.fr/pub/distrib/books/llc.pdf

There was a companion book, "Manuel de référence du langage Caml",
which is the French translation of the Caml Light 0.7 reference
manual.  For completeness, we also made it available:

  http://caml.inria.fr/pub/distrib/books/manuel-cl.pdf

Both texts are distributed under the Creative Commons BY-NC-SA
license.

Enjoy,

- Xavier Leroy

___
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs


___
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Caml-list] book "Le langage Caml"

[Xavier Leroy]

A few months ago, there was a discussion on this list about
"Le langage Caml", an early book on Caml (Light) programming written
by Pierre Weis and I.  The book was out of print, but the publisher,
Dunod Éditions, graciously agreed to relinquish its rights and give
them back to the authors.

Pierre and I are therefore happy to announce that the full text of the
book (2nd edition) is now available freely:

   http://caml.inria.fr/pub/distrib/books/llc.pdf

There was a companion book, "Manuel de référence du langage Caml",
which is the French translation of the Caml Light 0.7 reference
manual.  For completeness, we also made it available:

  http://caml.inria.fr/pub/distrib/books/manuel-cl.pdf

Both texts are distributed under the Creative Commons BY-NC-SA
license.

Enjoy,

- Xavier Leroy

___
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs