Pure type system
From Wikipedia, the free encyclopedia
In proof and type theory, a pure type system is a form of typed lambda calculus that obscures the distinction between types and terms and collapses the type hierarchy. It can be seen as a generalisation of Barendregt's lambda cube, and therefore serves as a uniform logical framework for studying type systems. Intuitionistic pure type systems were first described by Barendregt,[1] and the formalism was extended to classical logics via control operators by Barthe et al.[2]
[edit] References
- ^ H. Barendregt (1992). "Lambda calculi with types", in S. Abramsky, D. Gabbay and T. Maibaum: Handbook of Logic in Computer Science. Oxford Science Publications.
- ^ G. Barthe; J. Hatcliff; M. H. Sørensen (1997). "A Notion of Classical Pure Type System". Mathematical Foundations of Programming Semantics 6.
 |
This mathematical logic-related article is a stub. You can help Wikipedia by expanding it. |
