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...

• Type: Conference
• Year: 2009
• Where: PLPV
• Authors: Daniel R. Licata, Robert Harper
• Keywords: Dependent Programming Language, MEANINGS OF PROGRAMS, PLPV 2009, Positive Function Space, Programming Languages