Reverse Mathematics in Dependent Type Theory

Home > Computer Science home > Research > Profile > Projects > Reverse Mathematics in Dependent Type Theory

Project: Research

language, proof checker, constructive mathematics, formal logic

Status	Finished
Effective start/end date	16/10/06 → 15/09/09

Eng & Phys Sci Res Council EPSRC: £225,677

Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
Coercive Subtyping in Lambda-Free Logical Frameworks
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
Coercions in a polymorphic type system
Research output: Contribution to journal › Article › peer-review

ID: 21685142

Research

Profile

Royal Holloway, University of London
Egham,
Surrey,
TW20 0EX

T: +44 (0)1784 434455 T: +44 (0)1784 434455

Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory