Skip to content
  • HOME
  • Contact
  • Admin
The ANTIQUE Research Team
The ANTIQUE Research Team
Skip to content
  • PRESENTATION
  • TEAM MEMBERS
  • Publications
  • PROJECTS
  • JOB OFFERS
  • SEMINAR
Home Posts tagged "Remy Seassau (Cambium – Inria Paris)"

Tag: Remy Seassau (Cambium – Inria Paris)

Osiris: towards formal semantics and reasoning for OCaml

2025/01/24 - 2:00 PM 2025/02/10Seminars 2024-2025 Remy Seassau (Cambium - Inria Paris)

I will describe work in progress on Osiris, an attempt to equip a nontrivial fragment of OCaml with a formal semantics and with an interactive program verification environment, hosted inside the Rocq proof assistant. Our semantics is hybrid: it takes the form of a monadic interpreter, defined on top of…

Continue reading

Powered by Nirvana & WordPress. Mentions légales & CGU & Politique de confidentialité & Cookies

We are using cookies to give you the best experience on our website.

You can find out more about which cookies we are using or switch them off in .

The ANTIQUE Research Team
Powered by  GDPR Cookie Compliance
Privacy Overview

This website uses cookies so that we can provide you with the best user experience possible. Cookie information is stored in your browser and performs functions such as recognising you when you return to our website and helping our team to understand which sections of the website you find most interesting and useful.

Strictly Necessary Cookies

Strictly Necessary Cookie should be enabled at all times so that we can save your preferences for cookie settings.

If you disable this cookie, we will not be able to save your preferences. This means that every time you visit this website you will need to enable or disable cookies again.