CakeML/cakeml

Update CakeML tutorial to use monadic translator

Aberta

#697 aberto em 6 de nov. de 2019

Ver no GitHub
 (1 comentário) (0 reação) (0 responsável)Standard ML (98 forks)auto 404
help wanted

Métricas do repositório

Stars
 (1.169 estrelas)
Métricas de merge de PR
 (Métricas PR pendentes)

Description

Currently the CakeML tutorial, i.e. the files under tutorial/solutions and particularly wordfreqProgScript.sml, is based on CF proofs.

Since the monadic translator, which is described in Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions, could produce the same program in a nicer way, I think the tutorial should be ported to use the monadic translator.

One can take inspiration from existing examples that use the monadic translator.

Guia do colaborador

Direção de pesquisa
Estude os arquivos do tutorial existente e compare com os exemplos do tradutor monádico para entender as diferenças no estilo de prova. Em seguida, adapte o tutorial para usar o tradutor monádico.
Pilha de tecnologia
None
Domain
documentation
Tipo Issue
Documentação
DifficultyDificuldade de implementação estimada para um novo contribuidor, de 1 para alterações muito pequenas a 5 para trabalho de nível especializado.
3
Tempo estimadoUm intervalo de tempo aproximado para um colaborador experiente investigar, implementar, testar e preparar um pull request.
1-2 dias
Status da atividadeQuão disponível o issue aparece agora: novo, ativo, obsoleto, bloqueado ou aguardando entrada do mantenedor.
Ativo
ClarityCom que clareza o issue explica a mudança esperada, os critérios de aceitação e a próxima etapa.
Claro
Prerequisites
CakeMLStandard MLmonadic translator
Simpatia para novatosUma pontuação de 1 a 100 que estima o quão acessível este issue é para colaboradores iniciantes.
30