Join Our Newsletter

Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Pinyin
i2Cantonese
i2Cangjie
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

CORR

2006

Springer

2006

Springer

for an informal presentation at CIE 2007 [2] is a typed -calculus that pursues the reuse of the term constructions both at the level of types and at the level of contexts, while enjoying the most common metatheoretical properties [1]. Notice that the distinction we are making here between terms and types is borrowed from the simply typed -calculus . The development of is intended as the first step towards the verification of the following conjecture: the adoption of a single set of constructions for terms, types, and contexts (i.e. the "contexts as types as terms" paradigm) is compatible with the presence of a desirable meta-theory. features the term constructions of Church plus sorts, abbreviations and type casts. Sorts are necessary to build closed terms, abbreviations (i.e. let expressions) are essential in the proofs of some meta-theoretical properties when the "types as terms" paradigm is adopted and are practically unavoidable in mathematics and computer sc...

Related Content

Added |
11 Dec 2010 |

Updated |
11 Dec 2010 |

Type |
Journal |

Year |
2006 |

Where |
CORR |

Authors |
F. Guidi |

Comments (0)