Undecidability of Intersection Type Inhabitation at Rank 3 and its Formalization
In: Fundamenta Informaticae
Online
serialPeriodical
Zugriff:
We revisit the undecidability result of rank 3 intersection type inhabitation (Urzyczyn 2009) in pursuit of two goals. First, we simplify the existing proof, reducing simple semi-Thue systems to intersection type inhabitation in the original Coppo-Dezani type assignment system. Additionally, we outline a direct reduction from the Turing machine halting problem to intersection type inhabitation. Second, we formalize soundness and completeness of the reduction in the Coq proof assistant under the banner of “type theory inside type theory”.
Titel: |
Undecidability of Intersection Type Inhabitation at Rank 3 and its Formalization
|
---|---|
Autor/in / Beteiligte Person: | Dudenhefner, Andrej ; Rehof, Jacob |
Link: | |
Zeitschrift: | Fundamenta Informaticae |
Medientyp: | serialPeriodical |
Schlagwort: |
|
Sonstiges: |
|