Functional interpretations

Stream: new members

[Lia Malato]

Hello! I was wondering if functional interpretations have already been formalised in Lean?

[Horatiu Cheval]

Hello, glad to see this brought up. I am not aware of any implementation, but that's precisely what I am working on, and will hopefully finish within a month.

[Horatiu Cheval]

Do you have any particular interpretation in mind? Maybe you've already seen them, but the formalizations that I am aware of in other systems are Gödel’s Dialectica in Coq by Andrej Bauer and the nonstandard Dialectica in Agda by Chuangjie Xu.

[Lia Malato]

Thank you for letting me know, I am precisely working on Shoenfield's functional interpretation. I'll take a look at those two implementations you suggested!