Loading...
Please wait, while we are loading the content...
Similar Documents
Type systems for dummies.
| Content Provider | CiteSeerX |
|---|---|
| Author | Asperti, Andrea Guidi, Ferruccio |
| Abstract | We extend Pure Type Systems with a function turning each term M of type A into a dummy ∣M ∣ of the same type ( ∣ ⋅ ∣ is not an identity, in that M ≠ ∣M∣). Intuitively, a dummy represents an unknown, canonical object of the given type: dummies are opaque (cannot be internally inspected), and irrelevant in the sense that dummies of a same type are convertible to each other. This latter condition makes convertibility in PTS with dummies (DPTS) stronger than usual, hence raising not trivial consistency issues. DPTS offer an alternative approach to (proof) irrelevance, tagging irrelevant information at the level of terms and not of types, and avoiding the annoying syntactical duplication of products, abstractions and applications into an explicit and an implicit version, typical of systems like ICC ∗. Categories and Subject Descriptors F.4.1 [Mathematical Logic |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | Type System Trivial Consistency Issue Pure Type System Latter Condition Subject Descriptor Alternative Approach Mathematical Logic Implicit Version Syntactical Duplication Canonical Object Irrelevant Information |
| Content Type | Text |
