Variable Arity for LF

by John Boyland and Tian Zhao. Paper presented at LFMTP 2014 (Vienna Summer of Logic)


The dependently-typed lambda calculus (LF) supports use of meta-level binding in reasoning about bindings and hypotheticals in programming languages. That is, lambda expressions in LF can be used to model binders and hypothetical judgments depending on fixed-size contexts. However, because LF does not have a concept of variable-arity functions, a hypothetical judgment depending on a variable-size context cannot be modeled as an LF function. This paper extends LF to support variable-arity functions. As a result, one can model hypothetical judgments with variable contexts directly in the extended LF. The extended LF allows one to represent statements more transparently than previous work that uses complex meta-machinery to type the LF context. This is work in progress: we are still in the process of constructing a proof of correctness.

How to Get a Copy

The PDF is available here. The slides for the presentation are also available.

Last Modified: January 12, 2015

Variable Arity for LF