A modal foundation for meta-variables

We report on work in progress regarding a foundation for the notion of meta-variable in logical frameworks and type theories. Our proposal is to treat meta-variables as modal variables in a modal type theory, which is logically clean and justifies several low-level implementation techniques for meta-variables. We also speculate on other logical extensions of our modal type theory, at present without clear applications.

• Type: Conference
• Year: 2003
• Where: ICFP
• Authors: Aleksandar Nanevski, Brigitte Pientka, Frank Pfenning
• Keywords: ICFP 2003, Low-level Implementation Techniques, Modal Type Theory, Modal Variables, Programming Languages