Positively dependent types

11 years 10 months ago
Positively dependent types
This paper is part of a line of work on using the logical techniques of polarity and focusing to design a dependent programming language, with particular emphasis on programming with deductive systems such as programming languages and proof theories. Polarity emphasizes the distinction between positive types, which classify data, and negative types, which classify computation. In previous work, we showed how to use Zeilberger’s higher-order formulation of focusing to integrate a positive function space for representing variable binding, an essential tool for specifying logical systems, with a standard negative computational function space. However, our previous work considers only a simply-typed language. The central technical contribution of the present paper is to extend higher-order focusing with a form of dependency that we call positively dependent types: We allow dependency on positive data, but not negative computation. Additionally, we present the syntax of dependent pair an...
Daniel R. Licata, Robert Harper
Added 17 Mar 2010
Updated 17 Mar 2010
Type Conference
Year 2009
Where PLPV
Authors Daniel R. Licata, Robert Harper
Comments (0)