Structured Propositions as Types. Hanks, P. W. 120(477):11–52.
doi  abstract   bibtex   
Powerful insights arise from linking two fields of study previ- ously thought separate. Examples include Descartes's coordinates, which links geometry to algebra, Planck's Quantum Theory, which links particles to waves, and Shannon's Information Theory, which links thermodynamics to communication. Such a synthesis is of- fered by the principle of Propositions as Types, which links logic to computation. At first sight it appears to be a simple coincidence— almost a pun—but it turns out to be remarkably robust, inspiring the design of automated proof assistants and programming languages, and continuing to influence the forefronts of computing
@article{hanksStructuredPropositionsTypes2011,
  title = {Structured Propositions as Types},
  volume = {120},
  issn = {00264423},
  doi = {10.1093/mind/fzr011},
  abstract = {Powerful insights arise from linking two fields of study previ- ously thought separate. Examples include Descartes's coordinates, which links geometry to algebra, Planck's Quantum Theory, which links particles to waves, and Shannon's Information Theory, which links thermodynamics to communication. Such a synthesis is of- fered by the principle of Propositions as Types, which links logic to computation. At first sight it appears to be a simple coincidence— almost a pun—but it turns out to be remarkably robust, inspiring the design of automated proof assistants and programming languages, and continuing to influence the forefronts of computing},
  number = {477},
  journaltitle = {Mind},
  date = {2011},
  pages = {11--52},
  author = {Hanks, Peter W.},
  file = {/home/dimitri/Nextcloud/Zotero/storage/Z6P75AZQ/Hanks - 2011 - Structured propositions as types.pdf}
}
Downloads: 0