Sciweavers

ICALP
2004
Springer
13 years 9 months ago
Representing Nested Inductive Types Using W-Types
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...
Michael Abbott, Thorsten Altenkirch, Neil Ghani
LPAR
2007
Springer
13 years 9 months ago
HORPO with Computability Closure: A Reconstruction
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...
Frédéric Blanqui, Jean-Pierre Jouann...