Self-certification: Bootstrapping certified typecheckers in F* with Coq

Abstract : Well-established dependently-typed languages like Coq provide a highly reliable way to build and check formal proofs. Researchers have also developed several other dependently-typed programming languages such as Agda, Aura, ATS, Cayenne, Epigram, F*, F7, Fine, Guru, PCML5, Ur, etc., and more are in the works, e.g., Trellys. All these languages shine in their own regard, but they lag behind Coq in the degree of safety provided by their implementations. This paper proposes a general technique called self-certification that allows a typechecker for a suitably expressive language to be certified for correctness. We have implemented this general technique for F*, a dependently typed language on the .NET platform. Self-certification (for F*) involves implementing a typechecker for F* in F*, while using all the conveniences F* provides for the compiler-writer (e.g., partiality, effects, implicit conversions, proof automation, libraries). This type checker is given a specification (in F*) strong enough to ensure that it computes valid typing derivations. We obtain a typing derivation for the core typechecker by running it on itself, and we export it to Coq as a type-derivation certificate. By typechecking this derivation (in Coq) and applying the F* metatheory (also mechanized in Coq), we conclude that our type checker is correct. Once certified in this manner, the F* typechecker is emancipated from Coq. Self-certification leads to an efficient certification scheme---we no longer depend on verifying certificates in Coq---as well as a more broadly applicable one. For instance, the self-certified F* checker is suitable for use in adversarial settings where Coq is not intended for use, such as run-time certification of mobile code.
Type de document :
Communication dans un congrès
39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL'12, Jan 2012, Philadelphia, United States. 2012
Liste complète des métadonnées

Littérature citée [35 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00628775
Contributeur : Pierre-Yves Strub <>
Soumis le : vendredi 9 décembre 2011 - 07:00:04
Dernière modification le : vendredi 9 décembre 2011 - 07:00:04
Document(s) archivé(s) le : dimanche 4 décembre 2016 - 11:40:44

Fichier

self-cert-popl-2012.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00628775, version 1

Collections

Citation

Pierre-Yves Strub, Nikhil Swamy, Cédric Fournet, Juan Chen. Self-certification: Bootstrapping certified typecheckers in F* with Coq. 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL'12, Jan 2012, Philadelphia, United States. 2012. 〈inria-00628775〉

Partager

Métriques

Consultations de la notice

485

Téléchargements de fichiers

234