Structured type theory Export

@inproceedings{citeulike:612077, abstract = {We present our implementation AGDA of type theory. We limit ourselves in this presentation to a rather primitive form of type theory (dependent product with a simple notion of sorts) that we extend to structure facility we find in most programming language: let expressions (local definition) and a package mechanism. We call this language Structured Type Theory.}, author = {Coquand, Catarina and Coquand, Thierry}, booktitle = {Workshop on Logical Frameworks and Meta-languages (LFM'99), Paris, France}, citeulike-article-id = {612077}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.3778}, day = {28}, keywords = {agda, dependent-types, type-theory}, month = {September}, posted-at = {2008-09-15 17:28:18}, priority = {2}, title = {Structured type theory}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.3778}, year = {1999} }

TY - CONF ID - citeulike:612077 L3 - citeulike-article-id:612077 N2 - We present our implementation AGDA of type theory. We limit ourselves in this presentation to a rather primitive form of type theory (dependent product with a simple notion of sorts) that we extend to structure facility we find in most programming language: let expressions (local definition) and a package mechanism. We call this language Structured Type Theory. TI - Structured type theory T2 - Workshop on Logical Frameworks and Meta-languages (LFM'99), Paris, France KW - agda KW - dependent-types KW - type-theory AU - Coquand, Catarina AU - Coquand, Thierry PY - 1999/09/28/ UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.3778 ER -