CakeML/cakeml

Formalise DEFLATE and add implementation to examples

Ouverte

#806 ouverte le 16 nov. 2020

Voir sur GitHub
 (7 commentaires) (0 réaction) (0 personne assignée)Standard ML (98 forks)auto 404
enhancementgood first issuemedium effort

Métriques du dépôt

Stars
 (1 169 étoiles)
Métriques de merge PR
 (Métriques PR en attente)

Description

Deflate is a lossless data compression file format that zip and gzip are based on.

The deflate algorithm would be a nice formalisation and verification exercise in HOL. The result of the formalisation effort could be used to construct a verified gzip-like executable using CakeML.

The same compression and decompression algorithm might come in handy inside the CakeML compiler, once the compiler stores bulky constant data structures as read-only data. Such bulky constants could, for example, be the AST for the basis library or the bignum library.

This project is likely to fit the scope of an internship or MSc thesis.

Guide contributeur

Direction de recherche
Étudiez la RFC DEFLATE et les formalisations existantes dans HOL. Examinez la gestion des constantes dans le compilateur CakeML pour comprendre les points d'intégration potentiels.
Stack technique
Aucun
Domaine
compilersbackenddata
Type d'issue
Fonctionnalité
DifficultéDifficulté estimée pour un nouveau contributeur, de 1 pour un très petit changement à 5 pour un travail expert.
4
Temps estiméFourchette de temps approximative pour investiguer, implémenter, tester et préparer une pull request.
Plus d'une semaine
Statut d'activitéDisponibilité apparente de l'issue : fraîche, active, ancienne, bloquée ou en attente d'un mainteneur.
Active
ClartéClarté avec laquelle l'issue explique le changement attendu, les critères d'acceptation et la prochaine étape.
Investigation requise
Prérequis
HOLFormal verificationDEFLATE algorithm
Accessibilité débutantScore de 1 à 100 estimant l'accessibilité de cette issue pour un premier contributeur.
20