A framework for developing stand-alone certifiers
type: Item
instance of: scholarly article
title: A framework for developing stand-alone certifiers
zbMATH Open document ID: 1342.68304
author: Christian Sternagel
author: René Thiemann
publication date: 2016-08-01T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 6608303
zbMATH Keywords: certification
zbMATH Keywords: Isabelle/HOL
zbMATH Keywords: proof assistants
describes a project that uses: Xml
describes a project that uses: CeTA
describes a project that uses: LCF
describes a project that uses: Archive Formal Proofs
describes a project that uses: Cambridge LCF
describes a project that uses: Certification_Monads
describes a project that uses: Haskell Show Class
describes a project that uses: PVS
describes a project that uses: Coq
describes a project that uses: Isabelle/HOL
describes a project that uses: Sledgehammer
describes a project that uses: CoLoR
MaRDI profile type: Publication
full work available at URL: j.entcs.2015.04.004
OpenAlex ID: W2007088604
Wikidata QID: Q113317810
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
cites work: Designing programs that check their work
cites work: Sledgehammer: Judgement Day
cites work: Lazy Abstraction for Size-Change Termination
cites work: Q5389068
cites work: Reachability Analysis with State-Compatible Automata
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: Code Generation via Higher-Order Rewrite Systems
cites work: Partial and nested recursive function definitions in higher-order logic
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Logic and Computation
cites work: A variant of a recursively unsolvable problem
cites work: Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
cites work: On the Formalization of Termination Techniques based on Multiset Orderings
cites work: Certification of Termination Proofs Using CeTA
DOI: 10.1016/J.ENTCS.2015.04.004
Recommended article: A framework for the verification of certifying computations
Recommended article: A unified framework for DPLL(T) + certificates
Recommended article: A Unified Framework for Certificate and Compilation for QBF
description: scientific article; zbMATH DE number 6608303