• DocumentCode
    1822422
  • Title

    Type theory and recursion

  • Author

    Plotkin, G.D.

  • Author_Institution
    Dept. of Comput. Sci., Edinburgh Univ., UK
  • fYear
    1993
  • fDate
    19-23 Jun 1993
  • Firstpage
    374
  • Abstract
    Summary form only given. Type theory and recursion are analyzed in terms of intuitionistic linear type theory. This is compatible with a general recursion operator for the intuitionistic functions. The author considers second-order intuitionistic linear type theory whose primitive type constructions are linear and intuitionistic function types and second-order quantification
  • Keywords
    recursive functions; type theory; general recursion operator; intuitionistic function; intuitionistic function types; intuitionistic linear type theory; primitive type constructions; second-order quantification; second-order type theory; Algebra; Calculus; Computer languages; Computer science; Ear; Equations; Laboratories; Logic; Parametric statistics; Power system modeling;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 1993. LICS '93., Proceedings of Eighth Annual IEEE Symposium on
  • Conference_Location
    Montreal, Que.
  • Print_ISBN
    0-8186-3140-6
  • Type

    conf

  • DOI
    10.1109/LICS.1993.287571
  • Filename
    287571