Sémantique formelle d'OCaml dans Coq
La sémantique d'un grand sous-ensemble d'OCaml, appelé OCamllight , a été formalisée dans HOL par Owens il y a plusieurs années. Plus récemment, une sémantique théorique de type d'un plus petit sous-ensemble d'OCaml a été implémentée dans Nuprl par Kreitz, Hayden et Hickey . Y a-t-il un...