Document Open Access Logo

Type Safety of Rewrite Rules in Dependent Types

Author Frédéric Blanqui

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.13.pdf
  • Filesize: 499 kB
  • 14 pages

Document Identifiers

Author Details

Frédéric Blanqui
  • Université Paris-Saclay, ENS Paris-Saclay, CNRS, Inria, France
  • Laboratoire Spécification et Vérification, Cachan, France

Acknowledgements

The author thanks Jui-Hsuan Wu for his prototype implementation and his comments on a preliminary version of this work.

Cite As Get BibTex

Frédéric Blanqui. Type Safety of Rewrite Rules in Dependent Types. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 13:1-13:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.FSCD.2020.13

Abstract

The expressiveness of dependent type theory can be extended by identifying types modulo some additional computation rules. But, for preserving the decidability of type-checking or the logical consistency of the system, one must make sure that those user-defined rewriting rules preserve typing. In this paper, we give a new method to check that property using Knuth-Bendix completion.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Logic and verification
Keywords
  • subject-reduction
  • rewriting
  • dependent types

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek, C. Dubois, F. Gilbert, P. Halmagrand, O. Hermant, and R. Saillard. http://lsv.fr/~dowek/Publi/expressing.pdf, 2019. Draft. URL: http://lsv.fr/~dowek/Publi/expressing.pdf.
  2. F. Baader and T. Nipkow. Term rewriting and all that. Cambridge University Press, 1998. Google Scholar
  3. F. Barbanera, M. Fernández, and H. Geuvers. http://journals.cambridge.org/article_S095679689700289X. Journal of Functional Programming, 7(6):613-660, 1997. URL: http://journals.cambridge.org/article_S095679689700289X.
  4. H. Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of logic in computer science. Volume 2. Background: computational structures, pages 117-309. Oxford University Press, 1992. Google Scholar
  5. F. Blanqui. http://tel.archives-ouvertes.fr/tel-00105522. PhD thesis, Université Paris-Sud, France, 2001. URL: http://tel.archives-ouvertes.fr/tel-00105522.
  6. F. Blanqui. http://doi.org/10.1017/S0960129504004426. Mathematical Structures in Computer Science, 15(1):37-92, 2005. URL: http://doi.org/10.1017/S0960129504004426.
  7. J. Cockx and A. Abel. https://jesper.sikanda.be/files/sprinkles-of-extensionality.pdf. Presented at TYPES'2016. URL: https://jesper.sikanda.be/files/sprinkles-of-extensionality.pdf.
  8. D. Cousineau and G. Dowek. http://doi.org/10.1007/978-3-540-73228-0_9. In Proceedings of the 8th International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 4583, 2007. URL: http://doi.org/10.1007/978-3-540-73228-0_9.
  9. Dedukti. https://deducteam.github.io/, 2018. URL: https://deducteam.github.io/.
  10. H. Doornbos and B. von Karger. http://doi.org/10.1093/jigpal/6.2.195. Logic Journal of the Interest Group in Pure and applied Logic, 6(2):195-201, 1998. URL: http://doi.org/10.1093/jigpal/6.2.195.
  11. B. Gramlich. http://doi.org/10.1016/j.tcs.2012.09.008. Theoretical Computer Science, 464:3-19, 2012. URL: http://doi.org/10.1016/j.tcs.2012.09.008.
  12. R. Harper, F. Honsell, and G. Plotkin. http://doi.org/10.1145/138027.138060. Journal of the ACM, 40(1):143-184, 1993. URL: http://doi.org/10.1145/138027.138060.
  13. J. W. Klop. http://janwillemklop.nl/Jan_Willem_Klop/Bibliography_files/9.PhDthesis-total.pdf. PhD thesis, Utrecht Universiteit, NL, 1980. Published as Mathematical Center Tract 129. URL: http://janwillemklop.nl/Jan_Willem_Klop/Bibliography_files/9.PhDthesis-total.pdf.
  14. J. W. Klop, V. van Oostrom, and F. van Raamsdonk. http://doi.org/10.1016/0304-3975(93)90091-7. Theoretical Computer Science, 121:279-308, 1993. URL: http://doi.org/10.1016/0304-3975(93)90091-7.
  15. D. Knuth and P. Bendix. http://doi.org/10.1007/978-3-642-81955-1_23. In Computational problems in abstract algebra, Proceedings of a Conference held at Oxford in 1967, pages 263-297. Pergamon Press, 1970. Reproduced in [18]. URL: http://doi.org/10.1007/978-3-642-81955-1_23.
  16. U. Norell. http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf. PhD thesis, Chalmers University of Technology, Sweden, 2007. URL: http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf.
  17. R. Saillard. https://pastel.archives-ouvertes.fr/tel-01299180. PhD thesis, Mines ParisTech, France, 2015. URL: https://pastel.archives-ouvertes.fr/tel-01299180.
  18. J. H. Siekmann and G. Wrightson, editors. http://doi.org/10.1007/978-3-642-81955-1. Symbolic computation. Springer, 1983. URL: http://doi.org/10.1007/978-3-642-81955-1.
  19. TeReSe. Term rewriting systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  20. Y. Toyama. http://doi.org/10.1016/0020-0190(87)90122-0. Information Processing Letters, 25(3):141-143, 1987. URL: http://doi.org/10.1016/0020-0190(87)90122-0.
  21. V. van Oostrom. http://www.phil.uu.nl/~oostrom/publication/ps/phdthesis.ps. PhD thesis, Vrije Universiteit Amsterdam, NL, 1994. URL: http://www.phil.uu.nl/~oostrom/publication/ps/phdthesis.ps.
  22. J.-H. Wu. Checking the type safety of rewrite rules in the λπ-calculus modulo rewriting. https://hal.inria.fr/hal-02288720, 2019. Internship report. URL: https://hal.inria.fr/hal-02288720.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact