120(477):11–52.

doi abstract bibtex

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