Bindings as bounded natural functors
- Submitting institution
-
Middlesex University
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 1345
- Type
- E - Conference contribution
- DOI
-
10.1145/3290335
- Title of conference / published proceedings
- Proceedings of the ACM on Programming Languages, Volume 3 Issue POPL
- First page
- 22:1
- Volume
- 3
- Issue
- POPL
- ISSN
- 2475-1421
- Open access status
- Compliant
- Month of publication
- January
- Year of publication
- 2019
- URL
-
http://eprints.mdx.ac.uk/28146/
- 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
-
3
- Research group(s)
-
-
- Citation count
- -
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This advances the state of the art in Nominal-style datatypes, a central topic in formal reasoning. It is the culmination of a line of work on (co)datatypes and (co)recursion in Higher-Order Logic by Popescu and collaborators, which was published in CORE A*/A formal methods conferences (including ESOP, ICFP, IJCAR and LICS). This is significant because it can lead to better code generation, and proof assistance. This line of work was presented in an invited paper (FroCoS 2017) and talk (CALCO/MFPS 2019). The results are implemented in the Isabelle proof assistant, as part of its widely used datatype package.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -