La semántica de un gran subconjunto de OCaml, llamada OCamllight , fue formalizada en HOL por Owens hace varios años. Más recientemente, Kreitz, Hayden y Hickey implementaron una semántica teórica tipo de un subconjunto más pequeño de OCaml en Nuprl .
¿Hay algún desarrollo similar en Coq?
coq
program-verification
ocaml
Andrea Asperti
fuente
fuente
Respuestas:
¿Has visto la tesis doctoral de Arthur Charguéraud, Fórmulas características para la verificación mecanizada de programas ?
En lugar de construir el sistema de tipos y la semántica de pequeños pasos como relaciones inductivas, ofrece una técnica para convertir los programas de Caml en fórmulas características. Esto es básicamente una generalización de la semántica de transformador de predicados para admitir un subconjunto muy grande de Ocaml, en particular, incluyendo lanzamientos inseguros como
Obj.magic
. Para citar de su tesis:Es un enfoque muy atractivo si desea probar que un programa de Caml en particular es correcto (menos aún si está interesado en su metateoría).
fuente
Usted podría estar interesado en la implementación certificada de ML de Jacques Garrigue de ML con polimorfismo estructural y tipos recursivos , que establece la solidez de la semántica estática y dinámica y las propiedades de inferencia de tipos para un lenguaje ML con polimorfismo estructural (recursivo y), formalizando así uno de los Esquinas más avanzadas de OCaml (variantes polimórficas y tipos de objetos).
Dicho esto, este trabajo está más dirigido a verificar la solidez de las partes más avanzadas del sistema de tipos que a cubrir el conjunto de características de los programas OCaml existentes. Creo que en términos de tratar de probar la corrección de un programa OCaml existente, CFML sería una mejor opción.
fuente