Changing Data Structures in Type Theory: A Study of Natural Numbers
- 14 February 2002
- book chapter
- Published by Springer Nature
- p. 181-196
- https://doi.org/10.1007/3-540-45842-5_12
Abstract
No abstract availableKeywords
This publication has 9 references indexed in Scilit:
- Automating changes of data type in functional programsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A Prototype Proof Translator from HOL to CoqPublished by Springer Nature ,2000
- Equational Reasoning via Partial ReflectionPublished by Springer Nature ,2000
- Fix-Point Equations for Well-Founded Recursion in Type TheoryPublished by Springer Nature ,2000
- Analogy in Inductive Theorem ProvingJournal of Automated Reasoning, 1999
- Hybrid interactive theorem proving using nuprl and HOLPublished by Springer Nature ,1997
- A natural language explanation for formal proofsPublished by Springer Nature ,1997
- Representing proof transformations for program optimizationPublished by Springer Nature ,1994
- Views: a way for pattern matching to cohabit with data abstractionPublished by Association for Computing Machinery (ACM) ,1987