A functional interpretation with state
- Submitting institution
-
The University of Bath
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 210610449
- Type
- E - Conference contribution
- DOI
-
10.1145/3209108.3209134
- Title of conference / published proceedings
- LICS ’18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
- First page
- 839
- Volume
- -
- Issue
- -
- ISSN
- -
- Open access status
- -
- 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
-
0
- Research group(s)
-
-
- Citation count
- 0
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper, in one of the leading conferences in theoretical computer science, concerns a fundamental technique for extracting programs from proofs: Goedel's "Dialectica" interpretation. Traditionally, extracted programs are written in a simple functional language. The paper extends the translation to incorporate stateful programs. The article includes an extended discussion outlining five new problems prompted by the paper's main result. Our underlying technique, based on the "state-monad", has been studied and classified in a more abstract setting by C. Xu. A specific instance of the translation considered in our paper has been formalised in Agda by the same author.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -