Programming with binders and indexed data-types

7 years 10 months ago
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...
Andrew Cave, Brigitte Pientka
Added 25 Apr 2012
Updated 25 Apr 2012
Type Journal
Year 2012
Where POPL
Authors Andrew Cave, Brigitte Pientka
Comments (0)