Home > lambdatheultimate > The Triumph of Types: Principia Mathematica’s Impact on Computer Science

The Triumph of Types: Principia Mathematica’s Impact on Computer Science

November 27th, 2010 11:59 admin Leave a comment Go to comments

The Triumph of Types: Principia Mathematica’s Impact on Computer Science. Robert L. Constable

The role the ideas of Principia Mathematica played in type theory in programming languages is often alluded to in our discussions, making this contribution to a meeting celebrating the hundredth anniversary of Whitehead-and-Russell’s opus provocative.

To get your juices going here is a quote from page 3:

…I will discuss later our efforts at Cornell to create one such type theory, Computational Type Theory (CTT), very closely related to two others, the Calculus of Inductive Constructions (CIC) implemented in the Coq prover and widely used, and Intuitionistic Type Theory (ITT) implemented in the Alf and Agda provers. All three of these efforts, but especially CTT and ITT, were strongly influenced by Principia and the work of Bishop presented in his book Foundations of Constructive Analysis.

Source: The Triumph of Types: Principia Mathematica’s Impact on Computer Science

Related Articles:

  1. Super Principia Mathematica
  2. Triumph of the Cyborg Composer
  3. New Computer Model Predicts Impact of Yellowstone Volcano Eruption
  4. Do High Schools Know What ‘Computer Science’ Is?
  5. Is a Computer Science Degree Worth Getting Anymore?
blog comments powered by Disqus
YOYOYOOYOYOYO