Project Details
Description
language, proof checker, constructive mathematics, formal logic
| Status | Finished |
|---|---|
| Effective start/end date | 16/10/06 → 15/09/09 |
Funding
- Eng & Phys Sci Res Council EPSRC: £225,677.00
-
Coercive Subtyping in Lambda-Free Logical Frameworks
Adams, R., 2009, Proceedings of the Fourth international Workshop on Logical Frameworks and Meta-Languages. Cheney, J. & Felty, A. (eds.). New York: ACM, p. 30-39 10 p.Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
36 Downloads (Pure) -
Coercions in a polymorphic type system
Luo, Z., Aug 2008, In: Mathematical Structures in Computer Science. 18, 4, p. 729-751 23 p.Research output: Contribution to journal › Article › peer-review
File120 Downloads (Pure) -
Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory
Adams, R. & Luo, Z., 2007, Types for Proofs and Programs. Altenkirch, T. & McBride, C. (eds.). Springer, Vol. 4502. p. 1-17 17 p. (Lecture Notes in Computer Science).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
File157 Downloads (Pure)