Autosubst: On Mechanising Binders in a General-Purpose Proof Assistant (Invited Talk)

Stark, Kathrin

doi:10.4230/LIPIcs.ITP.2025.40

Autosubst: On Mechanising Binders in a General-Purpose Proof Assistant

Kathrin Stark

Heriot-Watt University, Edinburgh, UK

Abstract

The question of handling binders effectively regularly comes up when mechanising results in a proof assistant. Since the beginning of proof assistants, many solutions have been suggested: these include de Bruijn syntax, locally nameless binders, nominal syntax or HOAS. But even today – 20 years after the POPLMark Challenge [2] – new tools and approaches to binding are still being published. Binders are still mentioned as being a complication of mechanised proofs over pen-and-paper proofs and the source of uninteresting technicalities and heaps of boilerplate – particularly, when working in a proof assistant without native support for binders or quotients.

Autosubst [5, 4], initially developed a decade ago as a teaching tool, addresses this problem by automating boilerplate code generation for a de Bruijn representation in the Rocq prover. Autosubst translates a specification into the corresponding pure or scoped de Bruijn algebra: It hence generates a corresponding instantiation operation for parallel substitutions, and several equational substitution lemmas. Central to its usability is a rewriting tactic that automatically decides equality up to substitutions, requiring minimal input and knowledge from the user’s side. This greatly simplifies using the otherwise notoriously difficult de Bruijn representation. Since then, Autosubst has been successfully used in several projects.

In this talk, I will give an overview of the background and history of Autosubst and give an overview on the work, tools, and formalisations around it [7, 6, 1]. Moreover, this talk will highlight some of the more recent extensions [3] as well as outline future challenges and directions.

Keywords and phrases:

Syntax, binders, Rocq

Category:

Invited Talk

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Automated reasoning ; Theory of computation

\rightarrow

Type theory ; Theory of computation

\rightarrow

Operational semantics

DOI:

10.4230/LIPIcs.ITP.2025.40

Event:

16th International Conference on Interactive Theorem Proving (ITP 2025)

Editors:

Yannick Forster and Chantal Keller

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

References

[1] Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, and Kathrin Stark. Poplmark reloaded: Mechanizing proofs by logical relations. J. Funct. Program., 29:e19, 2019. doi:10.1017/S0956796819000170.
[2] Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: The poplmark challenge. In Joe Hurd and Thomas F. Melham, editors, Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, volume 3603 of Lecture Notes in Computer Science, pages 50–65. Springer, 2005. doi:10.1007/11541868_4.
[3] Yannick Forster and Kathrin Stark. Coq à la carte: a practical approach to modular syntax with binders. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 186–200. ACM, 2020. doi:10.1145/3372885.3373817.
[4] Steven Schäfer, Gert Smolka, and Tobias Tebbi. Completeness and decidability of de bruijn substitution algebra in coq. In Xavier Leroy and Alwen Tiu, editors, Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pages 67–73. ACM, 2015. doi:10.1145/2676724.2693163.
[5] Steven Schäfer, Tobias Tebbi, and Gert Smolka. Autosubst: Reasoning with de bruijn terms and parallel substitutions. In Christian Urban and Xingyuan Zhang, editors, Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings, volume 9236 of Lecture Notes in Computer Science, pages 359–374. Springer, 2015. doi:10.1007/978-3-319-22102-1_24.
[6] Kathrin Stark. Mechanising syntax with binders in Coq. PhD thesis, Saarland University, Saarbrücken, Germany, 2020. URL: https://publikationen.sulb.uni-saarland.de/handle/20.500.11880/28822.
[7] Kathrin Stark, Steven Schäfer, and Jonas Kaiser. Autosubst 2: reasoning with multi-sorted de bruijn terms and vector substitutions. In Assia Mahboubi and Magnus O. Myreen, editors, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, pages 166–180. ACM, 2019. doi:10.1145/3293880.3294101.

[bib.bib1] [1] Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Schäfer, and Kathrin Stark. Poplmark reloaded: Mechanizing proofs by logical relations. J. Funct. Program., 29:e19, 2019. doi:10.1017/S0956796819000170.

[bib.bib2] [2] Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: The poplmark challenge. In Joe Hurd and Thomas F. Melham, editors, Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, volume 3603 of Lecture Notes in Computer Science, pages 50–65. Springer, 2005. doi:10.1007/11541868_4.

[bib.bib3] [3] Yannick Forster and Kathrin Stark. Coq à la carte: a practical approach to modular syntax with binders. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 186–200. ACM, 2020. doi:10.1145/3372885.3373817.

[bib.bib4] [4] Steven Schäfer, Gert Smolka, and Tobias Tebbi. Completeness and decidability of de bruijn substitution algebra in coq. In Xavier Leroy and Alwen Tiu, editors, Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pages 67–73. ACM, 2015. doi:10.1145/2676724.2693163.

[bib.bib5] [5] Steven Schäfer, Tobias Tebbi, and Gert Smolka. Autosubst: Reasoning with de bruijn terms and parallel substitutions. In Christian Urban and Xingyuan Zhang, editors, Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings, volume 9236 of Lecture Notes in Computer Science, pages 359–374. Springer, 2015. doi:10.1007/978-3-319-22102-1_24.

[bib.bib6] [6] Kathrin Stark. Mechanising syntax with binders in Coq. PhD thesis, Saarland University, Saarbrücken, Germany, 2020. URL: https://publikationen.sulb.uni-saarland.de/handle/20.500.11880/28822.

[bib.bib7] [7] Kathrin Stark, Steven Schäfer, and Jonas Kaiser. Autosubst 2: reasoning with multi-sorted de bruijn terms and vector substitutions. In Assia Mahboubi and Magnus O. Myreen, editors, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, pages 166–180. ACM, 2019. doi:10.1145/3293880.3294101.