Modal Functional Interpretation

Mircea-Dan Hernest

We extend Gödel’s Dialectica interpretation to modal formulas and prove it sound for a certain modal arithmetic based on Gödel’s system T. The range of this Modal Dialectica interpretation is the usual Heyting Arithmetic in all finite types. We illustrate the use of the new tool for optimized program extraction as part of an enhanced light Dialectica interpretation.