Effectful applicative bisimilarity : monads, relators, and the Howe's method
- Submitting institution
-
The University of Birmingham
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 41883787
- Type
- E - Conference contribution
- DOI
-
10.1109/LICS.2017.8005117
- Title of conference / published proceedings
- 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
- First page
- 1
- Volume
- -
- Issue
- -
- ISSN
- -
- Open access status
- -
- Month of publication
- August
- Year of publication
- 2017
- 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
- This paper shows that a particular kind of reasoning ("Howe's method") about higher-order programs with effects, particulary probabilistic choice, can be done in a simple and general way, whereas previously ad hoc methods were used. But the paper's influence has gone beyond the specific study of Howe's method, as it was the first to use the algebraic notion of relator to reason about programming languages. These ideas were taken up, most prominently, by Simpson et al and by Maillard et al in their general logical accounts of different language features.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -