A semântica de um grande subconjunto de OCaml, chamado OCamllight , foi formalizada na HOL por Owens há vários anos. Mais recentemente, uma semântica teórica do tipo de um subconjunto menor de OCaml foi implementada no Nuprl por Kreitz, Hayden e Hickey .
Existe algum desenvolvimento semelhante no Coq?
coq
program-verification
ocaml
Andrea Asperti
fonte
fonte
Respostas:
Você já viu a tese de doutorado de Arthur Charguéraud, fórmulas características para verificação mecanizada de programas ?
Em vez de construir o sistema de tipos e a semântica de pequenos passos como relações indutivas, ele fornece uma técnica para converter programas Caml em fórmulas características. Isso é basicamente uma generalização da semântica do transformador de predicado para suportar um subconjunto muito grande de Ocaml - principalmente, incluindo elencos inseguros como
Obj.magic
. Para citar sua tese:É uma abordagem muito atraente se você quiser provar que um determinado programa Caml está correto (menos ainda, se você estiver interessado em sua metateoria).
fonte
Você poderia estar interessado no Uma Implementação Certificada de ML com Polimorfismo Estrutural e Tipos Recursivos de Jacques Garrigue , que estabelece a solidez da semântica estática e dinâmica e das propriedades da inferência de tipo para uma linguagem ML com polimorfismo estrutural (recursão e), formalizando assim um dos cantos mais avançados do OCaml (variantes polimórficas e tipos de objetos).
Dito isto, este trabalho tem como objetivo verificar a consistência de partes mais avançadas do sistema de tipos do que cobrir o conjunto de recursos dos programas OCaml existentes. Penso que, em termos de tentar provar a exatidão de um programa OCaml existente, a CFML seria uma escolha melhor.
fonte