CakeML/cakeml

Update CakeML tutorial to use monadic translator

Aperta

#697 aperta il 6 nov 2019

Vedi su GitHub
 (1 commento) (0 reazioni) (0 assegnatari)Standard ML (98 fork)auto 404
help wanted

Metriche repository

Star
 (1169 stelle)
Metriche merge PR
 (Metriche PR in attesa)

Descrizione

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.

Guida contributor

Direzione di ricerca
Studia i file del tutorial esistente e confrontali con gli esempi del traduttore monadico per comprendere le differenze nello stile di dimostrazione. Quindi adatta il tutorial per utilizzare il traduttore monadico.
Tech stack
Nessuno
Dominio
documentation
Tipo issue
Documentazione
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
3
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
1-2 giorni
Stato attivitàQuanto è probabile che la issue sia ancora attiva e reviewable.
Attiva
ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.
Chiara
Prerequisiti
CakeMLStandard MLmonadic translator
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
30