Projects per year
Abstract
One difficulty with reasoning and programming with dependent types is that proof obligations arise naturally once programs become even moderately sized. For example, implementing an adder for binary numbers indexed over their natural number equivalents naturally leads to proof obligations for equalities of expressions over natural numbers. The need for these equality proofs comes, in intensional type theories, from the fact that the propositional equality enables us to prove as equal terms that are not judgementally equal, which means that the typechecker can’t always obtain equalities by reduction. As far as possible, we would like to solve such proof obligations automatically. In this paper, we show one way to automate these proofs by reflection in the dependently typed programming language Idris. We show how defining reflected terms indexed by the original Idris expression allows us to construct and manipulate proofs. We build a hierarchy of tactics for proving equivalences in semigroups, monoids, commutative monoids, groups, commutative groups, semirings and rings. We also show how each tactic reuses those from simpler structures, thus avoiding duplication of code and proofs.
Original language  English 

Title of host publication  Intelligent Computer Mathematics 
Subtitle of host publication  10th International Conference, CICM 2017, Edinburgh, UK, July 1721, 2017, Proceedings 
Editors  Herman Geuvers, Matthew England, Osman Hasan, Florian Rabe, Olaf Teschke 
Place of Publication  Cham 
Publisher  Springer 
Pages  4055 
Number of pages  16 
ISBN (Electronic)  9783319620756 
ISBN (Print)  9783319620749 
DOIs  
Publication status  Published  2017 
Event  10th Conference on Intelligent Computer Mathematics (CICM 2017)  Edinburgh, United Kingdom Duration: 17 Jul 2017 → 21 Jul 2017 Conference number: 10 http://www.cicmconference.org/2017 
Publication series
Name  Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence) 

Publisher  Springer 
Volume  10383 (LNCS) 
ISSN (Print)  03029743 
Conference
Conference  10th Conference on Intelligent Computer Mathematics (CICM 2017) 

Abbreviated title  CICM 
Country/Territory  United Kingdom 
City  Edinburgh 
Period  17/07/17 → 21/07/17 
Internet address 
Keywords
 Proof automation
 Equivalence
 Equality
 Proof by reflection
 Correctbyconstruction software
 Typedriven development
Fingerprint
Dive into the research topics of 'Automatically proving equivalence by typesafe reflection'. Together they form a unique fingerprint.Projects
 1 Finished

TypeDriven Verification of Communic: Typedriven verification of communicating systems
Brady, E. C. (PI)
1/05/16 → 30/04/17
Project: Standard