Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

**Automatically proving equivalence by type-safe reflection.** / Slama, Franck; Brady, Edwin Charles.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Slama, F & Brady, EC 2017, Automatically proving equivalence by type-safe reflection. in H Geuvers, M England, O Hasan, F Rabe & O Teschke (eds), *Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings.* Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence), vol. 10383, Springer, Cham, pp. 40-55, 10th Conference on Intelligent Computer Mathematics (CICM 2017), Edinburgh, United Kingdom, 17/07/17. https://doi.org/10.1007/978-3-319-62075-6_4

Slama, F., & Brady, E. C. (2017). Automatically proving equivalence by type-safe reflection. In H. Geuvers, M. England, O. Hasan, F. Rabe, & O. Teschke (Eds.), *Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings *(pp. 40-55). (Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence); Vol. 10383). Cham: Springer. https://doi.org/10.1007/978-3-319-62075-6_4

Slama F, Brady EC. Automatically proving equivalence by type-safe reflection. In Geuvers H, England M, Hasan O, Rabe F, Teschke O, editors, Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings. Cham: Springer. 2017. p. 40-55. (Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)). https://doi.org/10.1007/978-3-319-62075-6_4

@inproceedings{364c78c5b4d9446589ae9cae497abb91,

title = "Automatically proving equivalence by type-safe reflection",

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.",

keywords = "Proof automation, Equivalence, Equality, Proof by reflection, Correct-by-construction software, Type-driven development",

author = "Franck Slama and Brady, {Edwin Charles}",

note = "We are also grateful for the support of the Scottish Informatics and Computer Science Alliance (SICSA) and EPSRC grant EP/N024222/1.",

year = "2017",

doi = "10.1007/978-3-319-62075-6_4",

language = "English",

isbn = "9783319620749",

series = "Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)",

publisher = "Springer",

pages = "40--55",

editor = "Herman Geuvers and Matthew England and Osman Hasan and Florian Rabe and Olaf Teschke",

booktitle = "Intelligent Computer Mathematics",

address = "Netherlands",

}

TY - GEN

T1 - Automatically proving equivalence by type-safe reflection

AU - Slama, Franck

AU - Brady, Edwin Charles

N1 - We are also grateful for the support of the Scottish Informatics and Computer Science Alliance (SICSA) and EPSRC grant EP/N024222/1.

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

KW - Proof automation

KW - Equivalence

KW - Equality

KW - Proof by reflection

KW - Correct-by-construction software

KW - Type-driven development

U2 - 10.1007/978-3-319-62075-6_4

DO - 10.1007/978-3-319-62075-6_4

M3 - Conference contribution

SN - 9783319620749

T3 - Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)

SP - 40

EP - 55

BT - Intelligent Computer Mathematics

A2 - Geuvers, Herman

A2 - England, Matthew

A2 - Hasan, Osman

A2 - Rabe, Florian

A2 - Teschke, Olaf

PB - Springer

CY - Cham

ER -

## Value-dependent session design in a dependently typed language

de Muijnck-Hughes, J., Brady, E. C. & Vanderbauwhede, W., 2 Apr 2019,*Proceedings Programming Language Approaches to Concurrency- and Communication-cEntric Software, Prague, Czech Republic, 7th April 2019.*Martins, F. & Orchard, D. (eds.). Open Publishing Association, p. 47-59 (Electronic Proceedings in Theoretical Computer Science; vol. 291).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

## Subtype polymorphism à la carte via machine learning on dependent types

Swan, J., Johnson, C. G. & Brady, E. C., 16 Jul 2018,*Companion Proceedings for the ISSTA/ECOOP 2018 Workshops.*New York, NY: Association for Computing Machinery, Inc, p. 14-16 3 p.Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

## 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 journal › Article

## 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 journal › Article

## Type-driven development with Idris

Brady, E. C., Mar 2017, Shelter Island: Manning Publications Co. 480 p.Research output: Book/Report › Book

ID: 250039705