Controlling unfolding in type theory
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2022
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908592991371264 |
|---|---|
| author | Gratzer, Daniel Sterling, Jonathan Angiuli, Carlo Coquand, Thierry Birkedal, Lars |
| author_facet | Gratzer, Daniel Sterling, Jonathan Angiuli, Carlo Coquand, Thierry Birkedal, Lars |
| contents | We present a new way to control the unfolding of definitions in dependent type theory. Traditionally, proof assistants require users to fix whether each definition will or will not be unfolded in the remainder of a development; unfolding definitions is often necessary in order to reason about them, but an excess of unfolding can result in brittle proofs and intractably large proof goals. In our system, definitions are by default not unfolded, but users can selectively unfold them in a local manner. We justify our mechanism by means of elaboration to a core theory with extension types -- a connective first introduced in the context of homotopy type theory -- and by establishing a normalization theorem for our core calculus. We have implemented controlled unfolding in the cooltt proof assistant, inspiring an independent implementation in Agda. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2210_05420 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Controlling unfolding in type theory Gratzer, Daniel Sterling, Jonathan Angiuli, Carlo Coquand, Thierry Birkedal, Lars Logic in Computer Science We present a new way to control the unfolding of definitions in dependent type theory. Traditionally, proof assistants require users to fix whether each definition will or will not be unfolded in the remainder of a development; unfolding definitions is often necessary in order to reason about them, but an excess of unfolding can result in brittle proofs and intractably large proof goals. In our system, definitions are by default not unfolded, but users can selectively unfold them in a local manner. We justify our mechanism by means of elaboration to a core theory with extension types -- a connective first introduced in the context of homotopy type theory -- and by establishing a normalization theorem for our core calculus. We have implemented controlled unfolding in the cooltt proof assistant, inspiring an independent implementation in Agda. |
| title | Controlling unfolding in type theory |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2210.05420 |