propositions-as-types.pdf
homepages.inf.ed.ac.uk · 8,008 words · saved by 1 readers
N/A
Propositions as Types ∗ Philip Wadler University of Edinburgh wadler@inf.ed.ac.uk Powerful insights arise from linking two fields of study previ- cluding Agda, Automath, Coq, Epigram, F# , F? , Haskell, LF, ML, ously thought separate. Examples include Descartes’s coordinates, NuPRL, Scala, Singularity, and Trellys. which links geometry to algebra, Planck’s Quantum Theory, which…
saved by
related reading
- Curry–Howard correspondenceen.wikipedia.org
- Type theory - Wikipediaen.wikipedia.org
- Curry–Howard correspondence - Wikipediaen.wikipedia.org
- Intuitionistic logic - Wikipediaen.wikipedia.org
- Lambda calculus - Wikipediaen.wikipedia.org
- canon00-goedel.pdfhirzels.com
- "Why don't you use dependent types?"lawrencecpaulson.github.io
- Language, Proof and Logichomepages.uc.edu
- Eat. Sleep. Math.eatsleepmath.tumblr.com
- Mathematics for Computer Sciencepeople.csail.mit.edu
- Gödel's incompleteness theorems - Wikipediaen.wikipedia.org
- Philosophy of Mathematics (Stanford Encyclopedia of Philosophy)plato.stanford.edu