A Modular Lean 4 Framework for Confluence and Strong Normalization of Lambda Calculi with Products and Sums
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866908703658082304 |
|---|---|
| author | Ramos, Arthur Oliveira, Anjolina de Queiroz, Ruy de Veras, Tiago |
| author_facet | Ramos, Arthur Oliveira, Anjolina de Queiroz, Ruy de Veras, Tiago |
| contents | We present Metatheory, a comprehensive library for programming language foundations in Lean 4. The library features a modular framework for proving confluence of abstract rewriting systems using three classical proof techniques: the diamond property, Newmans lemma, and the Hindley-Rosen lemma. These are instantiated across six case studies including untyped lambda calculus, combinatory logic, term rewriting, simply typed lambda calculus, and STLC with products and sums. All theorems are fully mechanized with zero axioms or sorry statements. We provide complete proofs of de Bruijn substitution infrastructure and demonstrate strong normalization via logical relations. To our knowledge, this is the first comprehensive confluence and normalization framework for Lean 4. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_09280 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Modular Lean 4 Framework for Confluence and Strong Normalization of Lambda Calculi with Products and Sums Ramos, Arthur Oliveira, Anjolina de Queiroz, Ruy de Veras, Tiago Logic in Computer Science 03B70, 03B15, 68Q42 F.3.1; F.3.2; F.4.1 We present Metatheory, a comprehensive library for programming language foundations in Lean 4. The library features a modular framework for proving confluence of abstract rewriting systems using three classical proof techniques: the diamond property, Newmans lemma, and the Hindley-Rosen lemma. These are instantiated across six case studies including untyped lambda calculus, combinatory logic, term rewriting, simply typed lambda calculus, and STLC with products and sums. All theorems are fully mechanized with zero axioms or sorry statements. We provide complete proofs of de Bruijn substitution infrastructure and demonstrate strong normalization via logical relations. To our knowledge, this is the first comprehensive confluence and normalization framework for Lean 4. |
| title | A Modular Lean 4 Framework for Confluence and Strong Normalization of Lambda Calculi with Products and Sums |
| topic | Logic in Computer Science 03B70, 03B15, 68Q42 F.3.1; F.3.2; F.4.1 |
| url | https://arxiv.org/abs/2512.09280 |