A type and scope safe universe of syntaxes with binding: their semantics and proofs
- Submitting institution
-
Heriot-Watt University
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 41355484
- Type
- D - Journal article
- DOI
-
10.1145/3236785
- Title of journal
- Proceedings of the ACM on Programming Languages
- Article number
- 90
- First page
- -
- Volume
- 2
- Issue
- ICFP
- ISSN
- 2475-1421
- Open access status
- Compliant
- Month of publication
- July
- Year of publication
- 2018
- 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
-
4
- Research group(s)
-
-
- Citation count
- 3
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper represents the culmination of more than 25 years' work on the representation of (programming and logical) languages with binding in theorem provers. An invited submission to the JFP of selected papers from the 2018 ACM ICFP conference (33% acceptance rate), it significantly extends the corresponding PACMPL/ICFP paper.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
