Automating inversion of inductive predicates in Coq

This publication has 5 references indexed in Scilit:

• An application of co-inductive types in Coq: Verification of the alternating bit protocol
  Published by Springer Nature ,1996
• Automatizing termination proofs of recursively defined functions
  Theoretical Computer Science, 1994
• Computation and Reasoning
  Published by Oxford University Press (OUP) ,1994
• The calculus of constructions
  Information and Computation, 1988
• Compiling pattern matching
  Lecture Notes in Computer Science, 1985