(UL)
  • Propositions as [types] : (extended abstract)
    Awodey, Steve ; Bauer, Andrej
    Obravnavamo modalni operator ▫$[A]$▫ na tipih, s katerimi lahko izbrišemo računsko vsebino tipa in formaliziramo pojem neodvisnosti od dokaza. Podamo pravila za t.i. "oklepajne tipe" v teoriji ... odvisnih tipov in polno semantiko v regularnih kategorijah in topoloških modelih. Pokažemo tudi, kako se interpretira logika prvega reda v teoriji tipov z oklepajnimi tipi ter interpretacijo uporabimo za primerjavo teorije tipov z intuicionistično in klasično logiko prvega reda.
    Vrsta gradiva - prispevek na konferenci
    Leto - 2002
    Jezik - angleški
    COBISS.SI-ID - 11953241