Reverse Mathematics in Dependent Type Theory

Research output

Research output per year 2007 2007 2008 2009 2009

• 2 Conference contribution
• 1 Article

Research output per year

Research output per year

Search results

• 2009

  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)
• 2008

  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

  File
  95 Downloads (Pure)
• 2007

  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

  File
  149 Downloads (Pure)