Proof principles for datatypes with iterated recursion
- 1 January 1997
- book chapter
- Published by Springer Nature
- p. 220-241
- https://doi.org/10.1007/bfb0026991
Abstract
No abstract availableKeywords
This publication has 20 references indexed in Scilit:
- A Coinduction Principle for Recursive Data Types Based on BisimulationInformation and Computation, 1996
- An application of co-inductive types in Coq: Verification of the alternating bit protocolPublished by Springer Nature ,1996
- A view on implementing processes: Categories of circuitsPublished by Springer Nature ,1996
- Strong categorical datatypes II: A term logic for categorical programmingTheoretical Computer Science, 1995
- An algebraic view of structural inductionPublished by Springer Nature ,1995
- Inductive familiesFormal Aspects of Computing, 1994
- The fibrational formulation of intuitionistic predicate logic ${\rm I}$: completeness according to Gödel, Kripke, and Läuchli. II.Notre Dame Journal of Formal Logic, 1993
- The fibrational formulation of intuitionistic predicate logic ${\rm I}$: completeness according to Gödel, Kripke, and Läuchli. I.Notre Dame Journal of Formal Logic, 1993
- Inductive types and type constraints in the second-order lambda calculusAnnals of Pure and Applied Logic, 1991
- Do-it-yourself type theoryFormal Aspects of Computing, 1989