Combining Testing and Proving in Dependent Type Theory
- 1 January 2003
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
- p. 188-203
- https://doi.org/10.1007/10930755_12
Abstract
No abstract availableKeywords
This publication has 9 references indexed in Scilit:
- General Recursion in Type TheoryLecture Notes in Computer Science, 2003
- Towards the animation of proofs – testing proofs by examplesTheoretical Computer Science, 2002
- Indexed Induction-RecursionLecture Notes in Computer Science, 2001
- A Finite Axiomatization of Inductive-Recursive DefinitionsLecture Notes in Computer Science, 1999
- Generic ProgrammingLecture Notes in Computer Science, 1999
- Dependent types in practical programmingPublished by Association for Computing Machinery (ACM) ,1999
- Cayenne—a language with dependent typesPublished by Association for Computing Machinery (ACM) ,1998
- Inductive familiesFormal Aspects of Computing, 1994
- Constructive Mathematics and Computer ProgrammingStudies in Logic and the Foundations of Mathematics, 1982