• DocumentCode
    3294709
  • Title

    Games and definability for system F

  • Author

    Hughes, Dominic J D

  • Author_Institution
    Comput. Lab., Oxford Univ., UK
  • fYear
    1997
  • fDate
    29 Jun-2 Jul 1997
  • Firstpage
    76
  • Lastpage
    86
  • Abstract
    We develop a game-theoretic model of the polymorphic λ-calculus, system F, as a fibred category F. Our main result is that every morphism σ of the model defines a normal form sσ of system F, whose interpretation is σ. Thus the model gives a precise, non-syntactic account of the calculus
  • Keywords
    formal logic; game theory; lambda calculus; definability; fibred category; game-theoretic model; games; morphism; polymorphic λ-calculus; system F; Analog computers; Calculus; Functional programming; Laboratories; Testing; Yarn;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 1997. LICS '97. Proceedings., 12th Annual IEEE Symposium on
  • Conference_Location
    Warsaw
  • ISSN
    1043-6871
  • Print_ISBN
    0-8186-7925-5
  • Type

    conf

  • DOI
    10.1109/LICS.1997.614935
  • Filename
    614935
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3294709