INTERSECTION TYPE SYSTEM AND LAMBDA CALCULUS WITH DIRECTOR STRINGS
| Autor: | Xinxin Shen, Kougen Zheng |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Property (philosophy)
Computer science Substitution (algebra) Type (model theory) Algebra TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Intersection Explicit substitution TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Subject reduction Lambda calculus computer Director string computer.programming_language |
| Zdroj: | Computer Science & Information Technology (CS & IT ). |
| DOI: | 10.5121/csit.2019.90313 |
| Popis: | The operation of substitution in ”3×6-calculus is treated as an atomic operation. It makes that substitution operation is complex to be analyzed. To overcome this drawback, explicit substitution systems are proposed. They bridge the gap between the theory of the ”3×6-calculus and its implementation in programming languages and proof assistants. ”3×6”3“4-calculus is a name-free explicit substitution. Intersection type systems for various explicit substitution calculi, not including ¦Eo-calculus, have been studied by researchers. In this paper, we put our attention to ”3×6”3“4-calculus. We present an intersection type system for ”3×6”3“4-calculus and show it satisfies the subject reduction property. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|