Thursday 7 November 2019, 14:00, LSV library: Maintaining a mechanized language semantics across several proof assistants: a call for solutions, Arthur Charguéraud (iCube).

Consider a programming language described by a mechanized semantics expressed in a proof assistant. For example, the verified compiler CakeML has its source semantics expressed in HOL. Assume now that users of other proof assistants, such as Isabelle or Coq, wish to prove programs correct with respect to that mechanized semantics. The question that arises is: how can we relate, with some reasonable amount of trust, a formal semantics expressed in one proof system with the same semantics expressed in another system? One important constraint is that the semantics should be expressed, for each of the proof assistants considered, in a sufficiently idiomatic fashion. Another constraint is that it should be possible, as the formal semantics evolves, to maintain all versions with reasonable effort. In this talk, I will detail the case of the CakeML semantics, and attempt to list the numerous ways in which one may attempt to tackle the problem of maintaining a set of formal definitions synchronized across several proof systems.