Hello
Here is the latest Caml Weekly News, for the week of June 09 to 16, 2009.
Archive: http://caml.inria.fr/pub/ml-archives/caml-list/2009/06/0977ec89bb1d8c0e89c28ce32fcfcee3.en.html
Venanzio Capretta announced:PhD position in Type Theory at Nottingham ----------------------------------------- A new PhD position is available in the Functional Programming Laboratory at the University of Nottingham. The topic of research for the project is "Programming and Reasoning with Infinite Structures": it consists in the theoretical study and development of software tools for coinductive types and structured corecursion. The candidate must be a UK resident with an excellent degree in Computer Science or Mathematics at MSc (preferred) or BSc level (first class or equivalent). The applicant should have a good background in mathematical logic, theoretical computer science or functional programming. (S)he should be interested doing research in type theory, constructive mathematics, category theory and foundations of formal reasoning. We offer: PhD place with living expenses (standard UK level) for 3 years. The grants also provide laptops and travel expenses for conference and workshop visits. Nottingham University provides a vibrant research environment in the Functional Programming Laboratory. Deadline for applications: 20 June 2009. Send a cover letter and your CV to Venanzio Capretta (vxc@cs.nott.ac.uk). Please contact me for any additional information that you need.
Archive: http://caml.inria.fr/pub/ml-archives/caml-list/2009/06/e11553d5273f4782ad247ef9dbf7366b.en.html
Sylvain Conchon announced:
Offre d'emploi: Ingénieur de développement
Dans le cadre d'une action de développement technologique (ADT), le
centre de recherche INRIA Saclay souhaite recruter un programmeur
OCaml en tant qu'ingénieur de développement pour une durée d'un an
(renouvelable une fois) à partir de l'automne 2009.
Mots clés: vérification de programmes, démonstration automatique, OCaml
Lieu de travail:
----------------
Centre de recherche INRIA Saclay - Ile de France
Parc Orsay Université
ZAC des vignes
32, rue Jean Rostand - Bât K
91893 Orsay Cedex France Cedex
Contexte:
---------
L'équipe de recherche ProVal propose des méthodes et outils de
développement logiciel faisant une large place à la preuve de
programmes assistée par ordinateurs. Des applications logicielles
critiques dans les domaines du transport, des transactions bancaires
ou des télécommunications sont mises rapidement sur le marché. Pour
garantir aux utilisateurs un comportement acceptable, il est
nécessaire qu'une large part de vérification soit réalisée de manière
mécanique. Nous développons des environnements qui à partir d'une
description formelle du comportement attendu du programme, exprimée
par le développeur dans un langage adapté à son problème, engendre des
formules logiques (obligations de preuve) suffisantes pour garantir la
correction du programme. Ces formules peuvent ensuite être traitées
par des démonstrateurs adaptés tel que Alt-ergo[1].
Ces activités de l'équipe se déroulent dans le cadre de contrats ANR
Decert (Déduction certifiée) et U3CAT (Unification de techniques
d'analyse statique de codes C critiques). Ce dernier associant en
particulier les partenaires industriels Airbus France et Dassault
aviation.
Activité:
---------
L'ingénieur réalisera des outils et des expérimentations scientifiques
autour du démonstrateur Alt-Ergo afin d'améliorer son efficacité dans
le domaine de la certification de codes critiques.
* Améliorations des performances d'Alt-Ergo comme prouveur de la
plate-forme de certification Caveat/Frama-C/Why[2]
* Traitement des cas d'échecs par génération de contre-exemples et
traitement semi-interactif
* Augmentation de la visibilité d'Alt-Ergo (e.g participation à la
compétition internationale SMT-Comp)
Compétences:
------------
* Formation en informatique et connaissances du développement
logiciel et des outils associés (cvs/svn, Makefile, documentation,
tests, débogage,...) ;
* Langages de programmation : Ocaml;
* Connaissances appréciées (non obligatoires): logique,
démonstration automatique, compilation;
* Maîtrise de l'anglais technique et scientifique;
* Bonnes aptitudes rédactionnelles.
Contacts:
---------
Sylvain Conchon et Evelyne Contejean
{sylvain.conchon, evelyne.contejean}@lri.fr
[1] http://alt-ergo.lri.fr
[2] http://frama-c.cea.fr/
Archive: http://caml.inria.fr/pub/ml-archives/caml-list/2009/06/6fbfcec1c38412bbe5f65e119d55962f.en.html
Damien Doligez announced:Research team: Tools for Proofs, MSR-INRIA Joint Centre The Microsoft Research-INRIA Joint Centre is offering a 2-year position for a post-doctoral researcher to work on a proof development environment for TLA+ in the Tools for Proofs project-team (see http://www.msr-inria.inria.fr). Research Context TLA+ is a language for formal specifications and proofs designed by Leslie Lamport. It is based on first-order logic, set theory, temporal logic, and a module system. While the specification part of TLA+ has existed for several years, the proof language is more recent, and we want to develop tools for writing and checking proofs. The main program of our development environment is called the Proof Manager (PM). The PM translates TLA+ source files to low-level proofs that are checked by Isabelle. To this end, the PM calls the Zenon automatic theorem prover to fill in the "trivial" details omitted from proofs at the source level. Within the Isabelle framework we have an axiomatization of TLA+ (Isabelle/TLA+). Isabelle provides high assurance by checking all the proofs provided by the user or by Zenon. The PM also has an interface to CVC3, which provides a stronger automatic prover, but with lower assurance of correctness. The current version of the PM handles only the "action" part of TLA+: first-order formulas with primed and unprimed variables; where a variable is considered as unrelated to its primed version. This allows us to translate first-order formulas to first-order formulas, without the overhead associated to an encoding of temporal logic into first-order logic. This part of TLA+ is already useful for proving safety properties. Description of the activity of the post-doc The task devoted to the post-doc will be to extend the proof manager to deal with the temporal part of TLA+. To this end, he will have to define a new translation into Isabelle to handle the temporal operators, in a way that enables the re-use of non-temporal theorems proved with the simple translation. He will also have to implement this new translation and the interface between the two translations. Skills and profile of the candidate We are looking for a candidate with skills in some or all of the following subjects: parsing and compilation, logic and set theory, Isabelle, OCaml, Eclipse and Java. Moreover, the applicant must have a good command of the English language. Location The Microsoft Research-INRIA Joint Centre is located on the Campus of INRIA Futurs, in South part of Paris, near the Le-Guichet RER station. The Tools for Proofs project-team is composed of Damien Doligez, Leslie Lamport and Stephan Merz. Contact Candidates should send a resume and the name and e-mail address of one or two references to Damien Doligez <damien.doligez@inria.fr>.
Archive: http://caml.inria.fr/pub/ml-archives/caml-list/2009/06/63eca616bb3bd3e03942b12f94692dc6.en.html
Yoann Padioleau announced:I am pleased to announce the first release of distribution.ml, a poor's man MapReduce for OCaml using MPI. The code is available here: http://aryx.kicks-ass.org/~pad/ocaml/mapreduce-0.1.tgz and the documentation (distribution.ml is a literate document) here: http://aryx.kicks-ass.org/~pad/ocaml/mapreduce.pdf
Archive: http://caml.inria.fr/pub/ml-archives/caml-list/2009/06/b57ae8bf83d10e7f811345f2ee432db6.en.html
Yoann Padioleau announced:I am pleased to announce the first public release of syncweb. From the introduction in the readme.txt: syncweb is a command line tool enabling programmers to use the literate programming[1] development methodology, using the noweb[2] tool, while still being able to modify the generated files from the literate document. syncweb provides a way to "synchronize" the possibly modified original document with its possibly modified views with an interface similar to unison[3]. In addition, syncweb synchronizes data at a fine grained level by computing and storing md5sum of the different chunks. Note that literate programming is different from using javadoc, or doxygen, or ocamlweb. Noweb, and syncweb, do not provide the same kind of services. Literate programming allows programmers to explain their code in the order they think the code will be better understood, and allows among other things to explain code piece by piece with the possiblity to present a high-level view first of the code. Moreover, because noweb is essentially a macro-processing language, one can also "program" at the noweb level, which can sometimes overcome some of the limitations or the language of the documented program. For instance, for OCaml programs, using noweb frees the programmer to declare the types both in the .mli and .ml file, avoiding tedious copy-paste and maintenance problems. One can also do some forms of Aspect-oriented Programming at the noweb level. The code is available here: http://aryx.kicks-ass.org/~pad/software/project-syncweb/syncweb-0.2.tgz The documentation here: http://aryx.kicks-ass.org/~pad/software/project-syncweb/readme.txt One can also see a demo of what it looks like to edit a noweb/syncweb file and what kind of output noweb and syncweb produces: The literate document: http://aryx.kicks-ass.org/~pad/software/project-syncweb/demo/distribution.ml.nw.html The generated but "synchronizable" ml code: http://aryx.kicks-ass.org/~pad/software/project-syncweb/demo/distribution.ml.html The generated pdf: http://aryx.kicks-ass.org/~pad/software/project-syncweb/demo/distribution.pdf [1] http://en.wikipedia.org/wiki/Literate_programming [2] http://www.cs.tufts.edu/~nr/noweb/ [3] http://www.seas.upenn.edu/~bcpierce/unison/
Archive: http://caml.inria.fr/pub/ml-archives/caml-list/2009/06/479e4e5b1e9448feef2f0546b382b4fd.en.html
Damien Doligez announced:
It is our pleasure to celebrate the 30th anniversary of the first
human-powered flight over the English channel by announcing the
release of OCaml version 3.11.1. This is mainly a bug-fix release,
see the list of changes below.
It is available here: http://caml.inria.fr/download.en.html
Special thanks to Andres Varon, who tested RC1 on eight different
configurations.
Happy hacking,
-- The OCaml team.
Objective Caml 3.11.1:
----------------------
Bug fixes:
- PR#4095: ocamldebug: strange behaviour of control-C
- PR#4403: ocamldebug: improved handling of packed modules
- PR#4650: Str.regexp_case_fold mis-handling complemented character
sets [^a]
- PR#4660: Scanf.format_from_string: handling of double quote
- PR#4666: Unix.exec* failure in multithread programs under MacOS X
and FreeBSD
- PR#4667: debugger out of sync with dynlink changes
- PR#4678: random "out of memory" error with systhreads
- PR#4690: issue with dynamic loading under MacOS 10.5
- PR#4692: wrong error message with options -i and -pack passed to
ocamlc
- PR#4699: in otherlibs/dbm, fixed construction of dlldbm.so.
- PR#4704: error in caml_modify_generational_global_root()
- PR#4708: (ocamldoc) improved printing of infix identifiers such as
"lor".
- PR#4722: typo in configure script
- PR#4729: documented the fact that PF_INET6 is not available on all
platforms
- PR#4730: incorrect typing involving abbreviation "type 'a t = 'a"
- PR#4731: incorrect quoting of arguments passed to the assembler on
x86-64
- PR#4735: Unix.LargeFile.fstat cannot report size over 32bits on Win32
- PR#4740: guard against possible processor error in
{Int32,Int64,Nativeint}.{div,rem}
- PR#4745: type inference wrongly produced non-generalizable type
variables.
- PR#4749: better pipe size for win32unix
- PR#4756: printf: no error reported for wrong format '%_s'
- PR#4758: scanf: handling of \<newline> by format '%S'
- PR#4766: incorrect simplification of some type abbreviations.
- PR#4768: printf: %F does not respect width and precision
specifications
- PR#4769: Format.bprintf fails to flush
- PR#4775: fatal error Ctype.Unify during module type-checking
(temporary fix)
- PR#4776: bad interaction between exceptions and classes
- PR#4780: labltk build problem under Windows.
- PR#4790: under Windows, map ERROR_NO_DATA Win32 error to EPIPE Unix
error.
- PR#4792: bug in Big_int.big_int_of_int64 on 32-bit platforms.
- PR#4796: ocamlyacc: missing NUL termination of string
- PR#4804: bug in Big_int.int64_of_big_int on 32-bit platforms.
- PR#4805: improving compatibility with the clang C compiler
- PR#4809: issue with Unix.create_process under Win32
- PR#4814: ocamlbrowser: crash when editing comments
- PR#4816: module abbreviations remove 'private' type restrictions
- PR#4817: Object type gives error "Unbound type parameter .."
- Module Parsing: improved computation of locations when an ocamlyacc
rule
starts with an empty nonterminal
- Type-checker: fixed wrong variance computation for private types
- x86-32 code generator, MSVC port: wrong "fld" instruction generated.
- ocamlbuild: incorrectly using the compile-time value of $OCAMLLIB
- Makefile problem when configured with -no-shared-libs
- ocamldoc: use dynamic loading in native code
Other changes:
- Improved wording of various error messages
(contributed by Jonathan Davies, Citrix).
- Support for 64-bit mode in Solaris/x86 (PR#4670).
Damien Doligez later added:I forgot one important detail: the release is only available as source for the moment. Binaries will be made available shortly.
Thanks to Alp Mestan, we now include in the Caml Weekly News the links to the recent posts from the ocamlcore planet blog at http://planet.ocamlcore.org/. Simple, Efficient Trie Maps: http://alaska-kamtchatka.blogspot.com/2009/06/simple-efficient-trie-maps.html OCamlDuce 3.11.1.0: http://caml.inria.fr/cgi-bin/hump.cgi?contrib=458 Two More for the Debian New Queue.: http://www.mega-nerd.com/erikd/Blog/CodeHacking/Debian/safe_uniplate.html ocamlglobaltags 1.0: http://caml.inria.fr/cgi-bin/hump.cgi?contrib=703 Algorithm-conscious, cache-oblivious: http://alaska-kamtchatka.blogspot.com/2009/06/algorithm-conscious-cache-oblivious.html OCamlDuce 3.11.1.0: http://forge.ocamlcore.org/forum/forum.php?forum_id=383 Multi-purpose indentation parser: http://ocamlhackers.ning.com/xn/detail/2175650:BlogPost:361 OCaml 3.11.0 on Ubuntu Karmic Koala nearly complete: https://bentobako.org/david/blog/index.php?post/2009/06/11/OCaml-3.11.0-on-Ubuntu-Karmic-Koala-nearly-complete Mlpost: http://forge.ocamlcore.org/projects/mlpost/
If you happen to miss a CWN, you can send me a message and I'll mail it to you, or go take a look at the archive or the RSS feed of the archives.
If you also wish to receive it every week by mail, you may subscribe online.