Subject: Attn: Development Editor, Latest Caml Weekly News Newsgroups: gmane.comp.lang.ocaml.weekly-news Date: Tuesday 11th June 2013 13:57:07 UTC (over 3 years ago) Hello, Here is the latest Caml Weekly News, for the week of June 04 to 11, 2013. 1) Ocamlnet-3.6.5 2) post-doc position at MSR-Inria 3) ocaml-ctypes, a library for calling C functions directly from OCaml 4) Core Suite 109.27.00 + core_kernel 5) OCaml on zLinux 6) Use-site variance in OCaml 7) New Book: OCaml from the Very Beginning 8) Deadline extension: OCaml 2013, new deadline on June 18 (anywhere on earth) 9) Findlib-1.4 10) Other Caml News ======================================================================== 1) Ocamlnet-3.6.5 Archive: <https://sympa.inria.fr/sympa/arc/caml-list/2013-06/msg00043.html> ------------------------------------------------------------------------ ** Amending the announcement from last week, Gerd Stolpmann said: Well, things go wrong... There was a build problem in 3.6.4 so that netstring-pcre did not work properly. This is fixed in the new versiopn 3.6.5 I just released. Gerd > Hi, > > I've just released Ocamlnet-3.6.4. This is a maintenance release > including: > > - New configure options for PCRE (-enable-full-pcre, -enable-pcre). > There is also documentation about the PCRE issue in Regexp.html > (remember that PCRE is no longer the default regexp engine). > - More documentation for Netmulticore: Netmcore_basics > - New Netplex module for mailboxes: Netplex_mbox. > - netcgi2-apache builds against apache-2.4 > > plus various smaller fixes and additions. > > For a full description, see the ChangeLog. > > Get Ocamlnet, read the manual etc. from > <http://projects.camlcity.org/projects/ocamlnet.html> ======================================================================== 2) post-doc position at MSR-Inria Archive: <https://sympa.inria.fr/sympa/arc/caml-list/2013-06/msg00042.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 contribute to the ADN4SE project aiming at extending the proof development environment for TLA+ developed in the Tools for Proofs project (<http://msr-inria.com/projects/tools-for-proofs>) and applying it for the verification of key components of a real-time operating system. Research Context ================ TLA+ is a language for specifying and reasoning about systems, including concurrent and distributed systems. It is based on first-order logic, set theory, temporal logic, and a module system. TLA+ and its tools have been used in industry for over a decade. More recently, we have extended TLA+ to include hierarchically structured formal proofs that are independent of any proof checker. We have released several versions of the TLAPS proof checker (<http://tla.msr-inria.inria.fr/tlaps>) and integrated it into the TLA+ Toolbox, an IDE for the TLA+ tools (<http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html>). TLAPS and the Toolbox support the top-down development of proofs and the checking of individual proof steps independently of the rest of the proof. This helps users focus on the part of the proof they are working on. Although it is still under active development, TLAPS is already a powerful tool and has been used for a few verification projects, in particular in the realm of distributed algorithms (e.g., <http://research.microsoft.com/en-us/um/people/lamport/tla/byzpaxos.html>). TLAPS consists of the Proof Manager (PM, an interpreter for the proof language that computes the proof obligations corresponding to each proof step) and an extensible list of backend provers. Current backends include the tableau prover Zenon, an encoding of TLA+ as an object logic in the Isabelle proof assistant, and a generic backend for SMT solvers. When possible, we expect backend provers to produce a detailed proof that is then checked by Isabelle. In this way, we can obtain high assurance of correctness as well as satisfactory automation. The current version of the PM handles only the "action" part of TLA+: first-order formulas with primed and unprimed variables, where a variable v is considered to be unrelated to its primed version v'. This allows us to translate non-temporal proof obligations to standard first-order logic, without the overhead associated with an encoding of temporal logic into first-order logic. An extension for handling full TLA+, including its temporal logic for verifying liveness properties, is currently being developed. Description of the activity of the post-doc =========================================== The post-doctoral position is funded by the PIA ADN4SE project (<http://www.systematic-paris-region.org/en/projets/adn4se>) that develops a real-time operating system and development tools for embedded systems based on PharOS. The system aims at providing certifiable correctness and performance guarantees, and core protocols of the operating system will be formally verified using the TLA+ notation and tools. Your research will make a key contribution to this verification effort. In particular, you will work with other members of the project, including Damien Doligez, Leslie Lamport, Tomer Libal, and Stephan Merz on extending the TLA+ Proof System and its libraries. You will also work with the project partners of ADN4SE, and in particular members of CEA List, to model the protocols subject to verification. Your contributions will be conceptual, by identifying theories and patterns that underly the verification of the operating system, and practical, by implementing formal libraries and software in order to carry out the verification task. As time permits and depending on your interests, you will have the opportunity to contribute to further improving the proof checker. This may include: - adding support for certain TLA+ features that are not yet handled by the PM, such as recursive operator definitions and elaborate patterns for variable bindings; - integrating new backends to improve the automation of proofs; - adding validation of proofs by backends whose proofs are not yet checked in the current version. Skills and profile of the candidate =================================== You should have a solid knowledge of mathematical logic as well as good implementation skills related to symbolic theorem proving. Experience with developing real-time systems are a plus. Our tools are mainly implemented in OCaml. Experience with temporal and modal logics, with interactive theorem provers or with Eclipse could be valuable. Given the geographical distribution of the members of the team, we highly value a good balance between the ability to work in a team and the capacity to propose initiatives. Location ======== The Microsoft Research-INRIA Joint Centre is located on the Campus of Ecole Polytechnique south of Paris, France. Starting date ============= The normal starting date of the contract would be November 2013, but we can arrange for an extremely well-qualified candidate to start sooner. Contact ======= Candidates should send a resume and the name and e-mail addresses of one or two references to Damien Doligez |
|||