Predicative Functionals and an Interpretation of ID^_
Jeremy Avigad
10.1184/R1/6492449.v1
https://kilthub.cmu.edu/articles/journal_contribution/Predicative_Functionals_and_an_Interpretation_of_ID_/6492449
<p>In 1958 Gödel published his Dialectica interpretation, which reduces classical arithmetic to a quantifier-free theory T axiomatizing the primitive recursive functionals of finite type.</p>
1997-12-22 00:00:00
Functional interpretation
Inductive definitions
Predicative polymorphism
Dependent types