Abstract
Autosubst enables automatic equality-checking up to the sigma-calculus for assumption-free equalities, allowing users to avoid cumbersome reasoning about de Bruijn indices. While effective in many cases, this approach is inapplicable when matching against typing rules, reduction relations, or lemmas, requiring users to either phrase typing rules in a way that they work with Autosubst or even stating explicitly an alternative de Bruijn term. But even without beta-reduction, solutions of matching may not be unique.
This paper presents a work-in-progress method for automatically pattern matching against assumptions, evaluated on standard case studies including the POPLMark and POPLMark Reloaded challenges.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the 21st Workshop on Logical Frameworks and Meta Languages: Theory and Practice |
| Publisher | Open Publishing Association |
| Pages | 47-57 |
| Number of pages | 11 |
| DOIs | |
| Publication status | Published - 24 Jul 2026 |
| Event | 21st Workshop on Logical Frameworks and Meta Languages 2026 - Lisbon, Portugal Duration: 24 Jul 2026 → … |
Publication series
| Name | Electronic Proceedings in Theoretical Computer Science |
|---|---|
| Volume | 448 |
| ISSN (Electronic) | 2075-2180 |
Workshop
| Workshop | 21st Workshop on Logical Frameworks and Meta Languages 2026 |
|---|---|
| Abbreviated title | LFMTP 2026 |
| Country/Territory | Portugal |
| City | Lisbon |
| Period | 24/07/26 → … |
Fingerprint
Dive into the research topics of 'Work-in-Progress: A Tactic for Pattern Matching in Autosubst'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver