Propositions as Types.

The article presents the Propositions as Types model, which attempts to conceptually link mathematical logic with computation. Topics addressed include an overview of several corresponding features of both systems, such as propositions proofs and simplification to types, programs and evaluation; how...

Descripción completa

Detalles Bibliográficos
Publicado en:Communications of the ACM Vol. 58; no. 12; pp. 75 - 85
Autor principal: WADLER, PHILIP
Formato: Artículo
Publicado: Association for Computing Machinery Dec2015
Materias:
Acceso en línea:Ver este registro en EBSCOhost
fields @attributes:
  recordID: 1
pdfLink:
plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=111185714&site=ehost-live
header:
  @attributes:
    shortDbName: hlh
    uiTerm: 111185714
    longDbName: Humanities International Complete
    uiTag: AN
  controlInfo:
    bkinfo:
    jinfo:
      jid:
        00010782
        ACM
      jtl: Communications of the ACM
      issn: 00010782
      maglogo: N
    pubinfo:
      dt: Dec2015
      vid: 58
      iid: 12
      pid: 68
      pub: Association for Computing Machinery
    artinfo:
      ui:
        111185714
        10.1145/2699407
      ppf: 75
      ppct: 10
      formats:
      tig:
        atl: Propositions as Types.
      aug:
        au: WADLER, PHILIP
        affil: Professor of Theoretical Computer Science, Laboratory for Foundations of Computer Science, School of Informatics, University of Edinburgh, Scotland.
      su:
        Mathematical logic
        Computer programming
        Proposition (Logic)
        Mathematical proofs
        Data types (Computer science)
        Computer software
      sug:
        subj:
          Mathematical logic
          Computer programming
          Proposition (Logic)
          Mathematical proofs
          Data types (Computer science)
          Computer software
      ab: The article presents the Propositions as Types model, which attempts to conceptually link mathematical logic with computation. Topics addressed include an overview of several corresponding features of both systems, such as propositions proofs and simplification to types, programs and evaluation; how the independent overlapping discoveries by both groups reinforce their findings, and how this model can extend to other forms of logic.
      pubtype: Periodical
      doctype: Article
      src: R
    language: English
    refInfo:
    copyright:
      @attributes:
        flag: Y
      dt:
        @attributes:
          year: 2015
    holdings:
      @attributes:
        islocal: N