Verifiable certificates for predicate subtyping

DOI10.1007/978-3-030-17184-1_16MaRDI QIDQ6070793zbMATH OpenFDO

Authors Frédéric Gilbert

Publication date 24 November 2023

Published in Programming Languages and Systems (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-17184-1_16

zbMATH Keywords

higher-order logicpredicate subtypingproof theorytype theory

Mathematics Subject Classification ID

Higher-order logic (03B16) Type theory (03B38) Cut-elimination and normal-form theorems (03F05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Certifying circuits in type theory
• A Computational Approach to Pocklington Certificates in Type Theory
• Verification of SpecC using predicate abstraction
• A framework for the verification of certifying computations
• An expressive, scalable type theory for certified code
• Certifying compilers using higher-order theorem provers as certificate checkers
• Satisfiability certificates verifiable in subexponential time
• Predicate abstraction for program verification

Cited in

(1)

• Certificates and Separation Logic

This page was built for publication: Verifiable certificates for predicate subtyping

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