Automatically proving equivalence by type-safe reflection
- Submitting institution
-
University of St Andrews
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 252026797
- Type
- E - Conference contribution
- DOI
-
10.1007/978-3-319-62075-6_4
- Title of conference / published proceedings
- Intelligent Computer Mathematics : 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings
- First page
- 40
- Volume
- 10383 (LNCS)
- Issue
- -
- ISSN
- 0302-9743
- Open access status
- Compliant
- Month of publication
- June
- Year of publication
- 2017
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
1
- Research group(s)
-
D - Programming Languages
- Citation count
- 2
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Dependently typed programming languages such as Idris give us the ability to verify properties of programs by type checking, by expressing invariants in types. This is an extremely powerful technique, but leads to proof obligations which must be discharged by a programmer, which limits the practicality of such languages. This paper addresses the problem with a novel approach to proof automation in Idris which uses Idris itself both to automatically construct proofs of equivalence and to verify the soundness of the proof automation, using verification of the functional aspects of a hardware adder as an example.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
