Abstract Soundness

Jasmin Christian Blanchette 📧, Andrei Popescu 🌐 and Dmitriy Traytel 🌐

February 10, 2017

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

A formalized coinductive account of the abstract development of Brotherston, Gorogiannis, and Petersen [APLAS 2012], in a slightly more general form since we work with arbitrary infinite proofs, which may be acyclic. This work is described in detail in an article by the authors, published in 2017 in the Journal of Automated Reasoning. The abstract proof can be instantiated for various formalisms, including first-order logic with inductive predicates.

License

BSD License

Topics

Session Abstract_Soundness

Depends on

Used by

Cite

× 
@article{Abstract_Soundness-AFP,
  author  = {Jasmin Christian Blanchette and Andrei Popescu and Dmitriy Traytel},
  title   = {Abstract Soundness},
  journal = {Archive of Formal Proofs},
  month   = {February},
  year    = {2017},
  note    = {\url{https://isa-afp.org/entries/Abstract_Soundness.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: