Self-certification: Bootstrapping certified typecheckers in F* with Coq - Archive ouverte HAL Access content directly
Conference Papers Year : 2012

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

(1) , (2) , (3) , (2)
1
2
3
Pierre-Yves Strub
  • Function : Author
  • PersonId : 857170
Nikhil Swamy
  • Function : Author
  • PersonId : 901972
Cédric Fournet
  • Function : Author
  • PersonId : 901974
Juan Chen
  • Function : Author
  • PersonId : 901973

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.
Fichier principal
Vignette du fichier
self-cert-popl-2012.pdf (520.03 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00628775 , version 1 (09-12-2011)

Identifiers

  • HAL Id : inria-00628775 , version 1

Cite

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. ⟨inria-00628775⟩

Collections

INRIA
930 View
381 Download

Share

Gmail Facebook Twitter LinkedIn More