Paper: The Geometry of Linear Higher-Order Recursion (at LICS 2005)

Authors: Ugo Dal Lago

Abstract

Linearity and ramification constraints have been widely used to weaken higher-order (primitive) recursion in such a way that the class of representable functions equals the class of polytime functions. We show that fine-tuning these two constraints leads to different expressive strengths, some of them lying well beyond polynomial time. This is done by introducing a new semantics, called algebraic context semantics. The framework stems from Gonthier’s original work and turns out to be a versatile and powerful tool for the quantitative analysis of normalization in presence of constants and higher-order recursion.

BibTeX

  @InProceedings{DalLago-TheGeometryofLinear,
    author = 	 {Ugo Dal Lago},
    title = 	 {The Geometry of Linear Higher-Order Recursion},
    booktitle =  {Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005)},
    year =	 {2005},
    month =	 {June}, 
    pages =      {366--375},
    location =   {Chicago, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }