Research & Development
Industrial Research
MONEYTRACK Project [FUI]
A blockchain R&D Project to reinvent non fungible directed money systems with a smart-contract language.
In this collaborative three-year project, OCamlPro, in association with WizyPay, Fintech Entreprises, Keyrus, Inria Paris and ESILV, is helping other partners to design a platform to reinvent non fungible directed money systems. The main innovation of the platform is the application of state-of-the-art blockchain technologies such as Tezos, with formal verification technologies. OCamlPro’s work is partially funded by Region Ile-de-France.
LCHIP Project [FUI]
A blockchain R&D Project to reinvent non fungible directed money systems with a smart-contract language.
In this collaborative three-year project, OCamlPro is helping Clearsy to develop a development platform for embedded software, targeting cheap microcontrollers for the railways industry. The main innovation of the platform is that the code will be automatically proven using the SMT solver Alt-Ergo, developed and maintained by OCamlPro. OCamlPro’s work is partially funded by Region Ile-de-France.
SecurOCaml Project [FUI]
Integrate security features in the OCaml language.
In this collaborative three-year project, OCamlPro works with CEA,INRIA, Lexifi, Trust-In-Soft and Safe River to build an environment for the development of security applications in OCaml, in particular auditing tools and static analysers, such as a detector for uncaught-exceptions. OCamlPro’s work is partially funded by the Conseil Général de l’Essonne.
UCF Project [FUI]
Developing the TryOCaml platform for OCaml coding in a browser.
In this collaborative three-year project, OCamlPro works with the startups Alterway and XWiki, and the academic research laboratories of University Pierre et Marie Curie, and Denis Diderot, to develop a DSL . It is also contributing to the design of MOOC Platforms, including the OCaml MOOC. OCamlPro’s work is partially funded by BPI France.
This collaborative two-year R&D project aimed at industrializing and adapting VMKit (based on LLVM) to address the issues of scientific programming languages, particularly in terms of performance thanks to “JIT” compilation. With Scilab Entreprises, Université Pierre et Marie Curie (UPMC) LIP6 research lab, Dassault Aviation, Arcelor Mittal, CNES, Silkan and Inria Saclay as partners, OCamlPro was developing static analysis and partial typing for the Scilab language. OCamlPro’s work was partially funded by the Conseil Général de l’Essonne.
Fundamental Research
Soprano Project [ANR]
During this collaborative four years project funded by the French government, OCamlPro has added to Alt-Ergo the ability to verify floating-point computations.
Vocal Project [ANR]
During this collaborative four years project funded by the French government, OCamlPro designed and implemented an OCaml library of formally verified modules that may be used in static analyzers and theorem provers.
BWare Project [ANR]
Proof-Based Mechanized platform for the Verification of B Proof Obligations Project.
Launch of the collaborative three-year project BWare with INRIA, the LRI Lab, the Clearsy Company, MERCE (Mitsubishi Electric R&D Centre Europe), CNAM’s CEDRIC lab. OCamlPro is improving the automatic theorem provers used by Atelier B, especially the Alt-Ergo SMT solver. This project is partially funded by the French National Research Agency.
The goal of this project was to design the next generation of package managers for Java and similar languages. For OCamlPro, the main outcome was the OPAM package manager, who has become the official package manager for the OCaml.
Funders
