CakeML/cakeml

Export CakeML proofs in OpenTheory format

Aperta

#516 aperta il 25 ago 2018

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

(Explicitly doing work hinted at in #321). The proofs in particular to package up and export would include the compiler correctness proof (at the machine-code level) and the OpenTheory reader implementation proof. Possible assignees: @michaelsproul, @oskarabrahamsson, @IlmariReissumies -- any interest?

Guida contributor

Direzione di ricerca
Familiarizzati con la struttura delle prove di CakeML e con il formato OpenTheory. Identifica i file di prova pertinenti per la correttezza del compilatore e l'implementazione del lettore. Comprendi come esportare le prove in formato OpenTheory.
Tech stack
Nessuno
Dominio
compilers
Tipo issue
Funzionalità
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
4
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
Oltre 1 settimana
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
Git
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
30