Programming with binders and indexed data-types

We show how to combine a general purpose type system for an existing language with support for programming with binders and contexts by refining the type system of ML with a restricted form of dependent types where index objects are drawn from contextual LF. This allows the user to specify formal systems within the logical framework LF and index ML types with contextual LF objects. Our language design keeps the index language generic only requiring decidability of equality of the index language providing a modular design. To illustrate the elegance and effectiveness of our language, we give programs for closure conversion and normalization by evaluation. Our three key technical contribution are: 1) a bi-directional type system for our core language which is centered around refinement substitutions instead of constraint solving. As a consequence, type checking is decidable and easy to trust, although constraint solving may be undecidable. 2) a big-step environment based operational s...

• Type: Journal
• Year: 2012
• Where: POPL
• Authors: Andrew Cave, Brigitte Pientka
• Keywords: Closure Conversion, Design Languages, Operational Semantics, POPL 2012, Programming Languages