Self-certification: bootstrapping certified typecheckers in F^ with Coq

DOI10.1145/2103656.2103723MaRDI QIDQ2942906zbMATH OpenOpenAlexFDO

Authors Pierre-Yves Strub, Nikhil Swamy, Juan Chen, Cédric Fournet

Publication date 11 September 2015

Published in Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2103656.2103723

zbMATH Keywords

dependent typescertificationrefinement types

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• Dependent types and multi-monadic effects in \(\mathrm{F}^*\)
• Secure distributed programming with value-dependent types
• Secure distributed programming with value-dependent types
• Certification of a type inference tool for ML: Damas-Milner within Coq
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant

Cited in

(5)

• Verified characteristic formulae for CakeML
• scientific article; zbMATH DE number 6296049 (Why is no real title available?)
• Dependent types and multi-monadic effects in \(\mathrm{F}^*\)
• ANF preserves dependent types up to extensional equality
• Foundations of dependent interoperability

Describes a project that uses

Uses Software

• CompCert
• Agda
• Cayenne
• HOL Light
• z3
• Coq

This page was built for publication: Self-certification: bootstrapping certified typecheckers in F\(^\ast\) with Coq

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2942906)