Skip to content

Research at St Andrews

Automatically proving equivalence by type-safe reflection

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Author(s)

School/Research organisations

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 type checker 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,semi-rings and rings. We also show how each tactic reuses those from simpler structures, thus avoiding duplication of code and proofs.
Close

Details

Original languageEnglish
Title of host publicationIntelligent Computer Mathematics
Subtitle of host publication10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings
EditorsHerman Geuvers, Matthew England, Osman Hasan, Florian Rabe, Olaf Teschke
Place of PublicationCham
PublisherSpringer
Pages40-55
ISBN (Electronic)9783319620756
ISBN (Print)9783319620749
DOIs
StatePublished - 2017
Event10th Conference on Intelligent Computer Mathematics (CICM 2017) - Edinburgh, United Kingdom
Duration: 17 Jul 201721 Jul 2017
Conference number: 10
http://www.cicm-conference.org/2017

Publication series

NameLecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)
PublisherSpringer
Volume10383
ISSN (Print)0302-9743

Conference

Conference10th Conference on Intelligent Computer Mathematics (CICM 2017)
Abbreviated titleCICM
CountryUnited Kingdom
CityEdinburgh
Period17/07/1721/07/17
Internet address

    Research areas

  • Proof automation, Equivalence, Equality, Proof by reflection, Correct-by-construction software, Type-driven development

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Type driven development of concurrent communicating systems

    Brady, E. C. 7 Jul 2017 In : Computer Science. 18, 3, 22 p., 1413

    Research output: Contribution to journalArticle

  2. Sequential decision problems, dependent types and generic solutions

    Botta, N., Jansson, P., Ionescu, C., Christiansen, D. & Brady, E. C. 17 Mar 2017 In : Logical Methods in Computer Science. 13, 1, 23 p., 7

    Research output: Contribution to journalArticle

  3. Type-driven development with Idris

    Brady, E. C. Mar 2017 Shelter Island: Manning Publications Co.480 p.

    Research output: Book/ReportBook

  4. Elaborator reflection: extending Idris in Idris

    Christiansen, D. & Brady, E. C. 4 Sep 2016 Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. New York: ACM, p. 284-297

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  5. Automatic predicate testing in formal certification: you’ve only proven what you’ve said, not what you meant!

    Slama, F. 2016 Tests and Proofs - 10th International Conference, TAP 2016 Held as Part of STAF 2016. Aichernig, B. K. & Furia, C. A. (eds.). Springer-Verlag, p. 191-198 8 p. (Lecture Notes in Computer Science; vol. 9762)

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

ID: 250039705