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

DOI10.1145/2103656.2103723zbMATH Open1321.68205OpenAlexW4243294044MaRDI QIDQ2942906FDOQ2942906

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

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

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)

Cited In (5)

• Verified characteristic formulae for CakeML
• Title not available (Why is that?)
• Dependent types and multi-monadic effects in \(\mathrm{F}^*\)
• ANF preserves dependent types up to extensional equality
• Foundations of dependent interoperability

Uses Software

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

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)