Reasoning with executable specifications

This publication has 11 references indexed in Scilit:

• Proof Of Program Transformations
  Published by Institute of Electrical and Electronics Engineers (IEEE) ,2005
• Inductive definitions in the system Coq rules and properties
  Published by Springer Nature ,2005
• Encoding natural semantics in Coq
  Published by Springer Nature ,1995
• Higher-Order Abstract Syntax with induction in Coq
  Published by Springer Nature ,1994
• Generalization and reuse of tactic proofs
  Published by Springer Nature ,1994
• Simplifying deep embedding: A formalised code generator
  Published by Springer Nature ,1994
• Symbolic animation as a proof tool
  Published by Springer Nature ,1994
• A meta-environment for generating programming environments
  ACM Transactions on Software Engineering and Methodology, 1993
• Larch: Languages and Tools for Formal Specification
  Published by Springer Nature ,1993
• Executable specification of static semantics
  Published by Springer Nature ,1984