Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
- 1 January 2006
- conference paper
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
- p. 114-129
- https://doi.org/10.1007/11737414_9
Abstract
No abstract availableThis publication has 19 references indexed in Scilit:
- Extracting a data flow analyser in constructive logicTheoretical Computer Science, 2005
- Modelling general recursion in type theoryMathematical Structures in Computer Science, 2005
- General Recursion via Coinductive TypesLogical Methods in Computer Science, 2005
- The view from the leftJournal of Functional Programming, 2004
- A general formulation of simultaneous inductive-recursive definitions in type theoryThe Journal of Symbolic Logic, 2000
- Fix-Point Equations for Well-Founded Recursion in Type TheoryLecture Notes in Computer Science, 2000
- Pipelined LMS adaptive filter using a new look-ahead transformationIEEE Transactions on Circuits and Systems II: Analog and Digital Signal Processing, 1999
- Definitions by rewriting in the Calculus of ConstructionsMathematical Structures in Computer Science, 1999
- Type-based termination of recursive definitionsMathematical Structures in Computer Science, 1999
- Terminating general recursionBIT Numerical Mathematics, 1988