ICALP
2004
Springer
14 years 4 months ago
2004
Springer
We show that strictly positive inductive types, constructed from polynomial functors, constant exponentiation and arbitrarily nested inductive types exist in any Martin-L¨of categ...
LPAR
2007
Springer
14 years 5 months ago
2007
Springer
Abstract. This paper provides a new, decidable definition of the higherorder recursive path ordering in which type comparisons are made only when needed, therefore eliminating the...