Projects per year
Abstract
In Das Kontinuum, Weyl showed how a large body of classical mathematics could be developed on a purely predicative foundation. We present a logicenriched type theory that corresponds to Weyl's foundational system. A large part of the mathematics in Weyl's book  including Weyl's definition of the cardinality of a set and several results from real analysis  has been formalised, using the proof assistant Plastic that implements a logical framework. This case study shows how type theory can be used to represent a nonconstructive foundation for mathematics.
Original language  English 

Title of host publication  Types for Proofs and Programs 
Editors  Thorsten Altenkirch, Conor McBride 
Publisher  Springer 
Pages  117 
Number of pages  17 
Volume  4502 
ISBN (Print)  9783540744634 
DOIs  
Publication status  Published  2007 
Event  TYPES 2006  Nottingham, United Kingdom Duration: 18 Apr 2006 → 21 Apr 2006 
Publication series
Name  Lecture Notes in Computer Science 

Publisher  Springer 
ISSN (Print)  03029743 
Conference
Conference  TYPES 2006 

Country/Territory  United Kingdom 
City  Nottingham 
Period  18/04/06 → 21/04/06 
Keywords
 logicenriched type theory
 predicativism
 formalisation of mathematics
Projects
 1 Finished

Reverse Mathematics in Dependent Type Theory
Adams, R. (PI)
Eng & Phys Sci Res Council EPSRC
16/10/06 → 15/09/09
Project: Research