| ||||
| ||||
![]() Title:The Essence of Type-Theoretic Elaboration Authors:Anja Petković Komel Conference:WiL2022 Tags:dependent type theory, elaboration and proof assistant Abstract: When using type theories in proof assistants the full syntax can quickly become too verbose to handle. One common solution to this problem is to design two type theories: a fully annotated type theory which has good meta-theoretic properties, is suitable for algorithmic processing and resides in the kernel of the proof assistant, and an economic one for the users’ input. The two theories are linked by elaboration, a reconstruction of missing information that happens during, or in parallel with, type-checking. We define a type-theoretic account of an elaboration map and relate its algorithmic properties to decidability of type-checking. The Essence of Type-Theoretic Elaboration ![]() The Essence of Type-Theoretic Elaboration | ||||
Copyright © 2002 – 2025 EasyChair |