Bridging Curry and Church's typing style
- Submitting institution
-
Heriot-Watt University
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 15020190
- Type
- D - Journal article
- DOI
-
10.1016/j.jal.2016.05.008
- Title of journal
- Journal of Applied Logic
- Article number
- -
- First page
- 42
- Volume
- 18
- Issue
- -
- ISSN
- 1570-8683
- Open access status
- Compliant
- Month of publication
- June
- Year of publication
- 2016
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
2
- Research group(s)
-
-
- Citation count
- 0
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- The result of a distinguished Visiting Professorship supported by the Pacific Institute for Mathematical Sciences, Canada and led to 3 distinguished keynote speeches at 2 universities (Calgary & Lethbridge). Curry's typing is user friendly since the computer finds all types, but type checking for powerful polymorphic/dependent Pure Type Systems (PTSs) is undecidable. Church's typing is decidable because the burden of assigning types is left to humans. Due to decidability, PTSs have been worked only for Church's style. This paper provides the first time, PTSs in Curry's style while giving a faithful correct translation from one style to the other.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
