Explicit substitution calculi with de Bruijn indices and intersection type systems
- Submitting institution
-
Heriot-Watt University
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 15020204
- Type
- D - Journal article
- DOI
-
10.1093/jigpal/jzu044
- Title of journal
- Logic Journal of the IGPL
- Article number
- jzu044
- First page
- 295
- Volume
- 23
- Issue
- 2
- ISSN
- 1367-0751
- Open access status
- Out of scope for open access requirements
- Month of publication
- December
- Year of publication
- 2014
- 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
- 1
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This work is the result of long collaborations with Brasilia University which has led to joint initiatives and events at which Professor Kamareddine lectured and gave keynote seminars. This particular work builds explicit substitutions for Intersection type systems. Both Intersection types and explicit substitution calculi help bridge theory and practice and for doing efficient computation. Working with explicit substitutions and calculi suitable for implementation require the use of forms suitable for the machine (e.g., de Bruijn indices). This is the first calculus of intersection types with de Bruijn indices and explicit subsitution. All metatheoretical properties (especially safety) are established.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
