A framework for developing stand-alone certifiers
From MaRDI portal
Publication:530847
DOI10.1016/J.ENTCS.2015.04.004zbMATH Open1342.68304OpenAlexW2007088604WikidataQ113317810 ScholiaQ113317810MaRDI QIDQ530847FDOQ530847
Authors: Christian Sternagel, René Thiemann 
Publication date: 1 August 2016
Full work available at URL: https://doi.org/10.1016/j.entcs.2015.04.004
Recommendations
Cites Work
- Certification of Termination Proofs Using CeTA
- Edinburgh LCF. A mechanized logic of computation
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
- Logic and Computation
- Isabelle/HOL. A proof assistant for higher-order logic
- A variant of a recursively unsolvable problem
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Sledgehammer: judgement day
- Designing programs that check their work
- Partial and nested recursive function definitions in higher-order logic
- Code generation via higher-order rewrite systems
- Automated certified proofs with CiME3
- Reachability Analysis with State-Compatible Automata
- 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
Cited In (1)
Uses Software
This page was built for publication: A framework for developing stand-alone certifiers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q530847)
