A framework for developing stand-alone certifiers

DOI10.1016/j.entcs.2015.04.004zbMath1342.68304OpenAlexW2007088604WikidataQ113317810 ScholiaQ113317810MaRDI QIDQ530847

René Thiemann, Christian Sternagel

Publication date: 1 August 2016

Full work available at URL: https://doi.org/10.1016/j.entcs.2015.04.004

zbMATH Keywords

Isabelle/HOLproof assistantscertification

Mathematics Subject Classification ID

Related Items (1)

Effect polymorphism in higher-order logic (proof pearl)

Uses Software

• Coq
• Isabelle/HOL
• PVS
• CeTA
• Sledgehammer
• LCF
• CoLoR
• Archive Formal Proofs
• Xml
• Haskell Show Class
• Cambridge LCF
• Certification_Monads

Cites Work

• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Partial and nested recursive function definitions in higher-order logic
• Isabelle/HOL. A proof assistant for higher-order logic
• Edinburgh LCF. A mechanized logic of computation
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
• Certification of Termination Proofs Using CeTA
• Code Generation via Higher-Order Rewrite Systems
• Logic and Computation
• Designing programs that check their work
• Lazy Abstraction for Size-Change Termination
• On the Formalization of Termination Techniques based on Multiset Orderings
• Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
• Reachability Analysis with State-Compatible Automata
• Sledgehammer: Judgement Day
• A variant of a recursively unsolvable problem

This page was built for publication: A framework for developing stand-alone certifiers