Proofs and types

著者

• Girard, Jean-Yves
• Taylor, Paul
• Lafont, Yves

書誌事項

Proofs and types

Jean-Yves Girard ; translated and with appendices by Paul Taylor, Yves Lafont

（Cambridge tracts in theoretical computer science, 7）

Cambridge University Press, 1989

注記

Bibliography: p. 162-165

Includes index

内容説明・目次

内容説明

This book is derived from notes prepared by J-Y.Girard for a course at the University of Paris VII. It deals with the mathematical background of the application to computer science of aspects of logic. It sheds light on traditional logic material and its prospective application to computer science.

目次

• Sense, denotation and semantics
• natural deduction
• the Curry-Howard isomorphism
• the normalisation theorem
• Godel's system T
• coherence spaces
• denotational semantics of T
• sums in natural deduction
• system F
• coherence semantics of the sum
• cut elimination (Hauptsatz)
• strong normalisation for F
• representation theorem
• semantics of System F
• what is linear logic?

「Nielsen BookData」 より

詳細情報

• NII書誌ID(NCID): BA06868186
• ISBN:
  • 0521371813
• 出版国コード: us
• タイトル言語コード: eng
• 本文言語コード: eng
• 出版地: Cambridge
• ページ数/冊数: xi, 176 p.
• 大きさ: 26 cm
• 分類:
  • LCC : QA9
• 件名:
  • LCSH : Logic, Symbolic and mathematics
• 親書誌ID:
  • BA01121831