Reflective Semantics of Constructive Type Theory: Preliminary Report Export

@inproceedings{citeulike:1576918, abstract = {It is well-known that the proof theory of many sufficiently powerful logics may be represented internally by Godelization. Here we show that for Constructive Type Theory, it is furthermore possible to define a semantics of the types in the type theory itself, and that this procedure results in new reasoning principles for type theory. Paradoxes are avoided by stratifying the definition in layers. 1 Introduction Given a sufficiently powerful logical theory L such as Peano Arithmethic, it is...}, author = {Smith, Scott F.}, booktitle = {Constructivity in Computer Science}, citeulike-article-id = {1576918}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.56.8865}, keywords = {constructive-type-theory, constructivity, topos-theory, type-theory}, pages = {33--45}, posted-at = {2007-08-20 14:52:42}, priority = {2}, title = {Reflective Semantics of Constructive Type Theory: Preliminary Report}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.56.8865}, year = {1991} }

TY - CONF ID - citeulike:1576918 L3 - citeulike-article-id:1576918 N2 - It is well-known that the proof theory of many sufficiently powerful logics may be represented internally by Godelization. Here we show that for Constructive Type Theory, it is furthermore possible to define a semantics of the types in the type theory itself, and that this procedure results in new reasoning principles for type theory. Paradoxes are avoided by stratifying the definition in layers. 1 Introduction Given a sufficiently powerful logical theory L such as Peano Arithmethic, it is... EP - 45 TI - Reflective Semantics of Constructive Type Theory: Preliminary Report T2 - Constructivity in Computer Science SP - 33 KW - constructive-type-theory KW - constructivity KW - topos-theory KW - type-theory AU - Smith, Scott PY - 1991/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.56.8865 ER -