Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant

This publication has 19 references indexed in Scilit:

• Extracting a data flow analyser in constructive logic
  Theoretical Computer Science, 2005
• Modelling general recursion in type theory
  Mathematical Structures in Computer Science, 2005
• General Recursion via Coinductive Types
  Logical Methods in Computer Science, 2005
• The view from the left
  Journal of Functional Programming, 2004
• A general formulation of simultaneous inductive-recursive definitions in type theory
  The Journal of Symbolic Logic, 2000
• Fix-Point Equations for Well-Founded Recursion in Type Theory
  Published by Springer Nature ,2000
• Pipelined LMS adaptive filter using a new look-ahead transformation
  IEEE Transactions on Circuits and Systems II: Analog and Digital Signal Processing, 1999
• Definitions by rewriting in the Calculus of Constructions
  Mathematical Structures in Computer Science, 1999
• Type-based termination of recursive definitions
  Mathematical Structures in Computer Science, 1999
• Terminating general recursion
  BIT Numerical Mathematics, 1988